Logic-ml

9 participants
1782 discussions

=?ISO-2022-JP?B?UmU6IEVMQxskQjgmNWY9ODJxIScbKEIzGyRCN24bKEI=?=14( 木） ), 13(水), 17(日)午後午後
by Jun Tarui 06 Feb '13

06 Feb '13

みなさま，１月３０日のメール（このメールの最後にあるもの）でお伝えしましたスケジュールの最新版をみなさまの参考のためお伝えします。主な変更点は、TBAとなっていたいくつかの講演タイトルが決定したことです。参加ご検討くださるようお願いします。垂井 -------------------------------- Mar13(Wed) Satellite Mini-Workshop, Shinagawa venue: Kyoto Univ Shinagawa Office, Shinagawa (in: Intercity Shinagawa Building A, 27th floor) http://www.kyoto-u.ac.jp/ja/tokyo-office http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Yoshio Okamoto (UEC), Suguru Tamaki (Kyoto U), Jun Tarui (UEC) each talk will have a 15-min break in the middle 10:30--12:15 David Zuckerman: Randomness Extraction: A Survey 12:15--13:40 lunch (on your own) 13:40--15:25 Ran Raz: Parallel Repetition of Two Prover Games: A Survey 15:25--15:45 break 15:45--17:30 Noam Nisan: Algorithmic Mechanism Design: Multi-unit Auctions 18:00-- impromptu dinner party at Shinagawa ------------------------------- Tokyo Complexity Workshop (Main Workshop): venue: Shinagawa Prince Hotel, Main Tower 8th floor, Room: "Turquoise 8" http://www.al.ics.saitama-u.ac.jp/elc/ws/ http://goo.gl/aCgSE fee for reception/banquet; no fee otherwise; please register in all cases Mar14(Thu) 13:20--13:30 opening 13:30--14:20 Umesh Varirani: Quantum Hamiltonian Complexity: through the computational lens 14:20--14:35 break 14:35--15:25 Rahul Jain: TBA 15:25--15:40 break 15:40--16:30 Pavel Pudlak: Polynomial Hierarchy and Bounded Arithmetic Hierarchy. 16:30--16:45 break 16:45--17:35 Ryan O'Donnell: Approximability and Proof Complexity 18:00--20:00 reception Mar15(Fri) 09:00--09:50 Noam Nisan: Selling Two Objects (in Three Models) 09:50--10:15 break 10:15--11:05 Ketan Mulmuley: The GCT Chasm 11:05--11:30 break 11:30--12:20 Joshua Grochow: Geometric Complexity Theory unifies and generalizes many known lower bounds (an introduction to GCT) 12:20--14:00 lunch (on your own) 14:00--14:50 Shachar Lovett: The probabilistic method - new frontiers 14:50--15:15 break 15:15--16:05 Zeev Dvir: Locally Decodable Codes: recent progress and open problems 16:05--16:30 break 16:30--17:20 Luca Trevisan: Spectral Graph Theory Mar16(Sat) 09:00--09:50 Raghu Meka: Recent Progress in Unconditional Derandomization 09:50--10:15 break 10:15--11:05 David Zuckerman: Pseudorandomness from Shrinkage 11:05--11:30 break 11:30--12:20 Irit Dinur: TBA 12:20--14:00 lunch (lunch on your own) 14:00--14:50 Rocco Servedio: TBA 14:50--15:15 break 15:15--16:05 Pinyan Lu: Complexity Dichotomies of Counting Problems 16:05--16:30 break 16:30--17:20 Ran Raz: Interactive Channel Capacity 18:00--20:00 banquet Mar17(Sun) 09:00--09:50 Valentine Kabanets: Yin and Yang of computing: From circuit lower bounds to compression and SAT algorithms, and back 09:50--10:05 break 10:05--10:55 Eric Allender: Strengthening the Link between Complexity Classes and Kolmogorov Complexity 10:55--11:10 break 11:10--12:00 Yuichi Yoshida: Robust approximation of CSPs: Universal algebra meets optimization -------------------------------- Mar17(Sun) Satellite Mini-Workshop on Geometric Complexity Theory(GCT) venue: 2nd floor meeting room, Campus Innovation Center, Tamachi http://www.cictokyo.jp/access.html http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Takeshi Tokuyama (Tohoku U), Susumu Ariki (Osaka U), Jun Tarui (UEC) speakers: Ketan Mulmuley and Joshua Grochow 14:00--18:15 (with 3 breaks) 18:30-- impromptu dinner party at Tamachi ------------------------------- Mar19(Tue) Satellite Mini-Workshp, Kyoto venue: Room 111, RIMS, Kyoto Univ, Kyoto http://www.kurims.kyoto-u.ac.jp/en/access-01.html http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Shin-ichi Tanigawa (RIMS), Suguru Tamaki (Kyoto U), Jun Tarui (UEC) 13:15--14:15 Raghu Meka: Beating the Union Bound via Gaussian Geometry 14:15--14:30 break 14:30--15:30 Zeev Dvir: Locally Decodable Codes: recent progress and open problems 15:30--15:45 break 15:45--17:15 Ketan Mulmuley: talk on geometric complexity theory 18:00-- impropmtu dinner party around Sanjo/Shijo-Kawara-machi -------------------------------- Speakers: Eric Allender (Rutgers) www.cs.rutgers.edu/~allender/ Irit Dinur (Weizmann) www.wisdom.weizmann.ac.il/~dinuri/ Zeev Dvir (Princeton) www.cs.princeton.edu/~zdvir/ Josh Grochow (U Toronto) www.cs.toronto.edu/~jgrochow/ Rahul Jain (Nat Univ Singapore) www.comp.nus.edu.sg/~rahul/ Valentine Kabanets (Simon Fraser) www.cs.sfu.ca/~kabanets/ Shachar Lovett (UCSD) https://sites.google.com/site/shacharlovetthomepage/ Pinyan Lu (Microsoft Research Asia and Shanghai Jiao Tong Univ) http://research.microsoft.com/en-us/people/pinyanl/ Raghu Meka (Princeton, IAS) www.math.ias.edu/~raghu/ Ketan Mulmuley (Chicago) www.cs.uchicago.edu/people/mulmuley Noam Nisan (Hebrew U) www.cs.huji.ac.il/~noam/ Ryan O'Donnell (CMU) www.cs.cmu.edu/~odonnell/ Pavel Pudlak (Math Institute of Czech Republic) www.math.cas.cz/~pudlak/ Ran Raz (Weizmann) www.wisdom.weizmann.ac.il/~ranraz/ Rocco Servedio (Columbia) www.cs.columbia.edu/~rocco/ Luca Trevisan (Stanford) http://theory.stanford.edu/~trevisan/ Umesh Vazirani (UC Berkeley) http://www.cs.berkeley.edu/~vazirani/ Yuichi Yoshida (National Institute of Informatics, Tokyo) http://research.nii.ac.jp/~yyoshida/ David Zuckerman (U Texas, Austin) www.cs.utexas.edu/~diz/ At 10:08 13/01/30, Jun Tarui wrote: >みなさま， > >電通大の垂井です． > >計算限界解明プロジェクト http://www.al.ics.saitama-u.ac.jp/elc/ >のキックオフメイン集会とサテライト集会に関して >プログラム作成と企画の主担当をしています． > >まだ調整中の部分もあるのですが，みなさまの参考のために >現時点での予定をお伝えします．ぜひ参加ご検討ください． > > >サテライト集会：参加費なしで登録不要です． >当日夕方に参加希望を現地で尋ねる形の懇親食事会を予定しています． > >メイン集会：参加費はなしですが，一部講演のみ聴講の場合でも >登録をお願いしています．登録締め切りは２月２８日です． > >よろしくお願いします． > >垂井淳 >-------------------------------------------- >Exploring the Limits of Computation (ELC) >Tokyo Complexity Workshop and Satellite Mini-Workshops: >http://www.al.ics.saitama-u.ac.jp/elc/ws/ > > >Mar13(Wed) Satellite Mini-Workshop, Shinagawa > >venue: Kyoto Univ Shinagawa Office, Shinagawa >http://www.kyoto-u.ac.jp/ja/tokyo-office http://goo.gl/aCgSE >registration not necessary; no participation fee; everybody is welcome >organizers: Yoshio Okamoto(UEC), Suguru Tamaki(Kyoto U), Jun Tarui(UEC) > >each talk will have a 15-min break in the middle >10:30--12:15 TBA >12:15--13:40 lunch (on your own) >13:40--15:25 Ran Raz: Parallel Repetition of Two Prover Games: A Survey >15:25--15:45 break >15:45--17:30 Noam Nisan: Algorithmic Mechanism Design: Multi-unit Auctions >18:00-- impromptu dinner party at Shinagawa > > >Mar17(Sun) Satellite Mini-Workshop on Geometric Complexity Theory(GCT) > >venue: 2nd floor meeting room, Campus Innovation Center, Tamachi >http://www.cictokyo.jp/access.html http://goo.gl/aCgSE >registration not necessary; no participation fee; everybody is welcome >organizers: Takeshi Tokuyama(Tohoku U), Susume Ariki(Osaka U), Jun Tarui(UEC) > >speakers: Ketan Mulmuley and Joshua Grochow > >14:00--18:15 (with 3 breaks) >18:30-- impromptu dinner party at Tamachi > > >Mar19(Tue) Satellite Mini-Workshp, Kyoto >venue: Room 111, RIMS, Kyoto Univ, Kyoto >http://www.kurims.kyoto-u.ac.jp/en/access-01.html http://goo.gl/aCgSE >registration not necessary; no participation fee; everybody is welcome >organizers: Shin-ichi Tanigawa(RIMS), Suguru Tamaki(Kyoto U), Jun Tarui(UEC) > >13:15--14:15 Raghu Meka: Beating the Union Bound via Gaussian Geometry >14:15--14:30 break >14:30--15:30 Zeev Dvir: Locally Decodable Codes: recent progress and open problems >15:30--15:45 break >15:45--17:15 Ketan Mulmuley: talk on geometric complexity theory >18:00-- impropmtu dinner party around Sanjo/Shijo-Kawara-machi > > >Tokyo Complexity Workshop (Main Workshop): tentative schedule as of Jan 30th >venue: Shinagawa Prince Hotel, Main Tower 8th floor, Room: "Turquoise 8" >http://www.al.ics.saitama-u.ac.jp/elc/ws/ http://goo.gl/aCgSE >fee for reception/banquet; no fee otherwise; please register in all cases > >Mar14(Thu) >13:20--13:30 opening >13:30--14:20 Umesh Varirani: Quantum Hamiltonian Complexity: > through the computational lens >14:20--14:35 break >14:35--15:25 Rahul Jain: TBA >15:25--15:40 break >15:40--16:30 Pavel Pudlak: Polynomial Hierarchy and Bounded Arithmetic Hierarchy. >16:30--16:45 break >16:45--17:35 Ryan O'Donnell: Approximability and Proof Complexity >18:00--20:00 reception > >Mar15(Fri) >09:00--09:50 Noam Nisan: Selling Two Objects (in Three Models) >09:50--10:15 break >10:15--11:05 Ketan Mulmuley: The GCT Chasm >11:05--11:30 break >11:30--12:20 Joshua Grochow: Geometric Complexity Theory unifies and generalizes > many known lower bounds (an introduction to GCT) >12:20--14:00 lunch >14:00--14:50 Shachar Lovett: The probabilistic method - new frontiers >14:50--15:15 break >15:15--16:05 Zeev Dvir: Locally Decodable Codes: recent progress and open problems >16:05--16:30 break >16:30--17:20 Luca Trevisan: TBA > >Mar16(Sat) >09:00--09:50 Raghu Meka: Recent Progress in Unconditional Derandomization >09:50--10:15 break >10:15--11:05 David Zuckerman: Pseudorandomness from Shrinkage >11:05--11:30 break >11:30--12:20 Irit Dinur: TBA >12:20--14:00 lunch >14:00--14:50 Rocco Servedio: TBA >14:50--15:15 break >15:15--16:05 Pinyan Lu: TBA >16:05--16:30 break >16:30--17:20 Ran Raz: Interactive Channel Capacity >18:00--20:00 banquet > >Mar17(Sun) >09:00--09:50 Valentine Kabanets: Yin and Yang of computing: From circuit lower bounds > to compression and SAT algorithms, and back >09:50--10:05 break >10:05--10:55 Eric Allender: Strengthening the Link between Complexity Classes > and Kolmogorov Complexity >10:55--11:10 break >11:10--12:00 Yuichi Yoshida: Robust approximation of CSPs: > Universal algebra meets optimization > >Speakers: > >Eric Allender (Rutgers) www.cs.rutgers.edu/~allender/ >Irit Dinur (Weizmann) www.wisdom.weizmann.ac.il/~dinuri/ >Zeev Dvir (Princeton) www.cs.princeton.edu/~zdvir/ >Josh Grochow (U Toronto) www.cs.toronto.edu/~jgrochow/ >Rahul Jain (Nat Univ Singapore) www.comp.nus.edu.sg/~rahul/ >Valentine Kabanets (Simon Fraser) www.cs.sfu.ca/~kabanets/ >Shachar Lovett (Princeton, IAS) > https://sites.google.com/site/shacharlovetthomepage/ >Pinyan Lu (Microsoft Research Asia and Shanghai Jiao Tong Univ) > http://research.microsoft.com/en-us/people/pinyanl/ >Raghu Meka (Princeton, IAS) www.math.ias.edu/~raghu/ >Ketan Mulmuley (Chicago) www.cs.uchicago.edu/people/mulmuley >Noam Nisan (Hebrew U) www.cs.huji.ac.il/~noam/ >Ryan O'Donnell (CMU) www.cs.cmu.edu/~odonnell/ >Pavel Pudlak (Math Institute of Czech Republic) > www.math.cas.cz/~pudlak/ >Ran Raz (Weizmann) www.wisdom.weizmann.ac.il/~ranraz/ >Rocco Servedio (Columbia) www.cs.columbia.edu/~rocco/ >Luca Trevisan (Stanford) > http://theory.stanford.edu/~trevisan/ >Umesh Vazirani (UC Berkeley) > http://www.cs.berkeley.edu/~vazirani/ >Yuichi Yoshida (National Institute of Informatics, Tokyo) > http://research.nii.ac.jp/~yyoshida/ >David Zuckerman (U Texas, Austin) www.cs.utexas.edu/~diz/

1 0

仙台ロジックスクール
by Tanaka Kazuyuki 05 Feb '13

05 Feb '13

仙台ロジックスクール SLS2013 （日本ベルギー合同勉強会）すでにご案内申し上げておりますCTFM研究集会(２月１８日〜２１日，東工大) http://sendailogic.math.tohoku.ac.jp/CTFM/ のサテライトとして，仙台にて学生・若手のための勉強会を下記の通り行います。【日程】　２月２２日（金）・２３日（土）9:00 開場【場所】　仙台国際センター　小会議室８【講師】　S. Simpson，Yang Yue，Wu Guohua 　　　　　照井一成，宮部賢志，秋吉亮太（敬称略） ※詳細は，下記ウェブ・ページをご覧ください。 http://sendailogic.math.tohoku.ac.jp/SLS/ 　――――――――――――――――――――――― 参加費は無料ですが，会場準備の都合上，参加される方は事前申し込みをお願いします。【申し込み期限】　2月11日（祝）【申し込み・問い合わせ先】　sendailogic(a)gmail.com 　(担当：朴) 下の申込書をカット＆ペーストして必要事項を記入のうえ，上のアドレス（朴）までお送りください。２２日の夜に懇親会（参加費３千円程度）を予定しておりますので、出欠を併せてお知らせください。 ※　宿泊については，近くのホテルの部屋をいくつかおさえてありますので，必要な方はお問い合わせください。幹事：田中一之，山崎武（東北大学・理学研究科）　――――――――――――――――――――――― 仙台ロジックスクール SLS2013　申込書　お名前　所属・身分　ご連絡先　講演会参加　　22日（　）　23日（　）　懇親会参加　　22日（　）　―――――――――――――――――――――――

1 0

Kobe Colloquium (Feb 6, 2013, Pelupessy)
by Makoto Kikuchi 04 Feb '13

04 Feb '13

Kobe Colloquium on Logic, Statistics and Informatics 以下の要領でコロキウムを開催します。日時：2013年2月6日（水）15:10-16:40 場所：神戸大学自然科学総合研究棟3号館4階421室（プレゼンテーション室）講演者：Florian Pelupessy (Ghent) ======================================================================== 題目：Connecting the provable with the unprovable アブストラクト： Since Gödels famous incompleteness theorems it is well known that there exist theorems which are not provable in Peano Arithmetic. In the last decades of the last century many mathematically interesting examples of such unprovable statements emerged, for example: the Paris-Harrington theorem, the Kanamori-McAloon theorem, Kruskal's tree theorem, Hydra battles and Goodstein sequences. In these theorems it is possible to insert a parameter function, where the resulting theorem variant with constant parameter is provable, but the variant with as parameter the identity function is unprovable. An obvious question in these cases is at which threshold between those functions (ordered by eventual domination) the resulting theorem changes from provable to unprovable: the phase transition for provability of the theorem. We study these phase transitions with the goal of better understanding unprovability. We will be examining the transition results for three Ramsey theorem variants: Friedman's adjacent Ramsey theorem, the Paris-Harrington theorem and the Kanamori-McAloon theorem. For these theorems it is possible to show a deep connection between lower/upper bound estimates for the variants with constant parameter values and the threshold values for the parametrised theorems. This shows an influence of mathematics which is provable at a level slightly stronger than exponential function arithmetic on provabiltiy at the level of Peano Arithmetic. ======================================================================== 交通：阪急六甲駅またはJR六甲道駅から神戸市バス36系統「鶴甲団地」行きに乗車，「神大本部工学部前」停留所下車，徒歩すぐ． http://www.kobe-u.ac.jp/info/access/rokko/rokkodai-dai2.htm 連絡先：菊池誠　mkikuchi(a)kobe-u.ac.jp

1 0

重要なご連絡ーアブストラクトの公開について（訂正）
by Masahiro Kumabe 02 Feb '13

02 Feb '13

皆様複数受け取られた場合はご容赦ください。こんにちは。日本数学会の数学基礎論及び歴史分科会の連絡評議委員の隈部です。先日、学会発表におけるアブストラクトの公開についてのご連絡を、メールにてお知らせしましたが、訂正があります。重要な内容ですので、是非ご一読お願い致します。＊学会における一般講演のアブストラクトについて２０１３年度年会から、数学会として、一般講演のアブストラクトをPDFファイルとして、学会開催前に、数学会のホームペジにて公開することをご連絡しましたが、これは、数学基礎論及び歴史分科会においては、学会会員内だけの公開です。昨年９月の分科会総会でそのように決まっていました。ここにお詫びして訂正致します。申し訳ありませんでした。従いまして、学会会員でない方は、アブストラクトの冊子を学会会場で購入してご覧になれます。以上の件、お間違いのないようにご理解ください。隈部

1 0

【参加申込締切2013年2月4日(月)】CTFM 2013, Tokyo, 18-20, Feb 2013
by Naohi Eguchi 01 Feb '13

01 Feb '13

Logic-ml の皆様，以下の研究会の参加申込締切が迫ってまいりましたのでご案内させていただきます． Computability Theory and Foundations of Mathematics (CTFM 2013) (2013年2月18日(月)～2月20日(水)，東京工業大学大岡山キャンパス) 参加ご希望の方は参加登録ページよりお申込ください． http://sendailogic.math.tohoku.ac.jp/CTFM/registration.html 参加申込締切：2013年2月4日(月) 多くの方々の参加申込をお待ちいたしております．江口直日，Sam Sanders, 田中一之 CTFM(a)math.tohoku.ac.jp ============================================================ Computability Theory and Foundations of Mathematics (Tokyo Institute of Technology, Tokyo, Japan, February 18 - 20, 2013) http://sendailogic.math.tohoku.ac.jp/CTFM/ ============================================================ Computability Theory and Foundations of Mathematics (CTFM) aims to develop computability theory and logical foundations of Mathematics. The scope involves the topics Computability Theory, Reverse Mathematics, Nonstandard Analysis, Proof Theory, Constructive Mathematics, Theory of Randomness and Computational Complexity Theory. This is a successor workshop to Workshop on Proof Theory and Computability Theory 2012 - Philosophical Frontiers in Reverse Mathematics (February 20 - 23, 2012, Tokyo, Japan). -------------------------------------------- Deadline of Registration: February 4th, 2013 -------------------------------------------- Invited Speakers: Chi Tat Chong (National University of Singapore) Erik Palmgren (Stockholm University) Michael Rathjen (University of Leeds) Helmut Schwichtenberg (LMU Munich) Stephen G. Simpson (Pennsylvania State University) Yang Yue (National University of Singapore) Wu Guohua (Nanyang Technological University) -------------------------------------------- Programme Committee: Toshiyasu Arai (Chiba) Naohi Eguchi (Tohoku) Hajime Ishihara (JAIST) Ryo Kashima (Tokyo Institute of Technology) Sam Sanders (Ghent) Kazuyuki Tanaka (Tohoku, Co-chair) Andreas Weiermann (Ghent, Co-chair) Takeshi Yamazaki (Tohoku) Keita Yokoyama (Tokyo Institute of Technology) --------------------------------------------

1 0

Eighth NII Type Theory Workshop
by Makoto Tatsuta 01 Feb '13

01 Feb '13

Eighth NII Type Theory Workshop Date: February 6, 2013, 10:40--16:50 Place: National Institute of Informatics, Room 1904 (19th floor) 場所: 国立情報学研究所 19階 1904室 (半蔵門線,都営地下鉄三田線・新宿線神保町駅または東西線竹橋駅より徒歩5分) (地図 http://www.nii.ac.jp/about/access/) Program: 10:40--11:20 Toshihiko Uchida (The Graduate University for Advanced Studies) Title: A Partial Translation from lambda U to lambda 2 11:20--12:00 Daisuke Kimura (National Institute of Informatics) Title: Linear Pure Type Systems 12:00--14:00 Lunch Break 14:00--14:40 Kazuyuki ASADA (National Institute of Informatics) Title: Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation 14:40--15:20 Makoto Tatsuta (National Institute of Informatics) Title: Dual Calculus with Inductive and Coinductive Types 15:20--15:50 Tea Break 15:50--16:50 Stefano Berardi (Torino University) Title: A Curry-Howard result for various subclassical logics Abstracts: ---------------------------------------------------------------------- Toshihiko Uchida (The Graduate University for Advanced Studies) Title: A Partial Translation from lambda U to lambda 2 Abstract: Girard showed that every type of sort * (i.e., proposition) is inhabited in lambda U. Barendregt state without proof that every type of sort Box (i.e., domain) is also inhabited in the system. In this talk, we show that the second statement is not the case by giving a partial translation from lambda U to lambda 2. ---------------------------------------------------------------------- Daisuke Kimura (National Institute of Informatics) Title: Linear Pure Type Systems Abstract: This talk proposes a linear variant of Pure Type Systems (PTSs), called linear pure type systems (LPTSs). It is a general framework, which provides a uniform way to treat various linear type systems that have the features of linear logic. We first introduce a subframework of LPTSs, called multiplicative linear pure type systems (MLPTSs), in which only variables that linearly occur are abstracted. All MLPTSs are consistent and satisfy strong normalization. However their expressive power is rather weak. We then give LPTSs by extending MLPTSs with exponentials. Each PTS can be embedded into a LPTS. We also show the equivalence of strong normalizability of PTSs and LPTSs by giving mutual translations between them. ---------------------------------------------------------------------- Kazuyuki ASADA (National Institute of Informatics) Title: Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation Abstract: We give Curry-Howard style correspondence between (propositional logic part of) Dialectica interpretation and bidirectional transformation. Dialectica interpretation was introduced by Godel to show relative consistency of Heyting Arithmetic to System T. Independently, bidirectional transformation arose in database community for automatic view-update problem, and recently have been studied in programming language community to formulate languages for bidirectional transformations. A bidirectional transformation consists of a pair of forward ("usual") transformation and a backward ("inverse") transformation, and we usually assume that they satisfy some standard axioms called GetPut law and PutGet law. We show GetPut law naturally fits the above correspondence to Dialectica interpretation, and this gives a way of extending a language for bidirectional transformations with GetPut law. Then we modify the above scheme for PutGet law and the combination of GetPut and PutGet laws. We also show that Paiva's variant of Dialectica model, GC, corresponds to the category for inverse computation. Then for the result by Paiva that the original Dialectica category is the coKleisli category of some comonad on GC, we give similar result for PutGet law, and we utilize this to investigate further categorical structures of these models. Also we see that a kind of Diller-Nahm variant of Dialectica interpretation corresponds to backward-partial bidirectional transformation. ---------------------------------------------------------------------- Makoto Tatsuta (National Institute of Informatics) Title: Dual Calculus with Inductive and Coinductive Types Abstract: This talk gives an extension of Dual Calculus by introducing inductive types and coinductive types. The same duality as Dual Calculus is shown to hold in the new system, that is, this talk presents its involution for the new system and proves that it preserves both typing and reduction. The duality between inductive types and coinductive types is shown by the existence of the involution that maps an inductive type and a coinductive type to each other. The strong normalization in this system is also proved. First, strong normalization in second-order Dual Calculus is shown by translating it into second-order symmetric lambda calculus. Next, strong normalization in Dual Calculus with inductive and coinductive types is proved by translating it into second-order Dual Calculus. This is a joint work with Daisuke Kimura. ---------------------------------------------------------------------- Stefano Berardi (Torino University) Title: A Curry-Howard result for various subclassical logics Abstract: We introduce games with Sequential Backtracking as a model for various sub-classical logic that have implication as a primitive connective. We define a one-sided version of the logical systems, whose proofs have a tree isomorphism (a kind of ``Curry Howard'' isomorphism) with respect to the winning strategies of the game semantics. We use this correspondence to interpret various classical proofs as learning algorithms. ---------------------------------------------------------------------- 問合せ先　龍田 (tatsuta(a)nii.ac.jp)

1 0

数学基礎論及び歴史分科会からの重要なお知らせ
by Masahiro Kumabe 31 Jan '13

31 Jan '13

皆様複数受け取られた場合はご容赦ください。こんにちは。日本数学会の数学基礎論及び歴史分科会の連絡評議委員の隈部です。学会に関して、以下の通りお知らせします。重要な内容ですので、是非ご一読お願い致します。（１）学会における一般講演のアブストラクトについて２０１３年度年会から、数学会として、一般講演のアブストラクトをPDFファイルとして、学会開催前に、数学会のホームペジにて公開することになりました。公開する時期は、学会が開催される２週間前までには公開する予定でいますが、詳しい内容については、学会のホームページにアクセスして、その都度ご確認ください。なおアブストラクトは、学会の会員外の方もダウンロードできるようにする予定です。これにより、アブストラクトを事前に各個人がプリントアウトし、それを持参して、学会に臨むことができるようになります。（２）（１）の対応に関連して、学会会場にて販売されていたアブストラクトの冊子の販売については、分科会として、以下の通りとすることになりました。アブストラクトの冊子での販売は、上記変更による混乱を避けるため、２０１３年度年会においては、続けます。ただし販売部数が減少することが予想されるため、用意する部数を減らします。アブストラクトの冊子の購入を希望される方は、この点ご了解ください。また出来る限り、事前にアブストラクトをプリントアウトあるいはダンロードして、学会に臨まれることをお願いします。当分科会のアブストラクトは、会員外の方もダウンロードできますので、できるだけそのようにお願いします。アブストラクトの冊子での販売は、赤字が予想されますので、なるべく早い時期に廃止する方向で考えています。そのためにもスムーズな移行ができるよう、ご協力お願いします。（３）２０１３年度年会は京都で行われますが、開催期間の京都のホテルが既に混み合っていると数学会から連絡を受けました。ですから、至急ホテルの予約をしていただきますようお願いいたします。以上です。連絡評議委員隈部正博

1 0

CAPE Truth theory and Logic Workshopのお知らせ
by Shunsuke Yatabe 31 Jan '13

31 Jan '13

みなさま複数受け取られた場合はご容赦ください。 2月13日に京都大学で行われる CAPE Truth theory and Logic Workshop のご案内をご転送させて頂きます。矢田部俊介 ---------- Forwarded message ---------- CAPE Truth theory and Logic Workshopのお知らせ皆様京都大学大学院文学研究科附属応用哲学・倫理学教育研究センター（CAPE）の主催にて、 CAPE Truth theory and Logic Workshopが下記のように開催されます。今回は特別講演として、ブリストル大学のPhilip Welch先生に、チューリングの数学の業績に関する一般向け講演（元々は6'th European Cogress of Mathematics で行われたもの）をお願いしました（1600-1745の最終枠です）。専門家以外の方も、ぜひお越し下さい。京都大学大学院文学研究科附属応用哲学・倫理学教育研究センター http://www.bun.kyoto-u.ac.jp/cape/cape-top_page/ 事務補佐　　竹中利彦〒606-0085 京都市左京区吉田本町　京都大学文学部内 CAPE(a)bun.kyoto-u.ac.jp **************************************************************************************** CAPE Truth theory and Logic Workshop Date: February 13 (Wed) 9:00-17:00, Place: The 8th lecture room, "Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)" of Kyoto University, No34 of the map in http://www.kyoto-u.ac.jp/en/access/campus/main.htm （京都大学総合研究2号館第8講義室） CAPE Website: http://www.bun.kyoto-u.ac.jp/cape/cape-top_page/ Timetable: 9:00-10:15 Shunsuke Yatabe "Yablo paradox and semantics of coinductive language" 10:30-11:45 Graham E. Leigh "Global reflection and theories of truth" 13:15-14:30 Katsuhiko Sano "What is the corresponding first-order logic to coalgebraic modal logic?" 14:30-15:45 Leon Horsten " One hundred years of semantic paradox" 16:00-17:15 Philip Welch "Alan Turing's Mathematical work" Abstracts: Shunsuke Yatabe (Kyoto University) title: Yablo paradox and semantics of coinductive language Abstract: We generalize the framework of Barwise and Etchmendy's "the liar" to that of coinductive language, and focus on a diﬃculty of constructing semantics. We deﬁne a game theoretic semantics, which can be regarded as a version of Austin semantics. Graham E. Leigh (University of Oxford) title: Global reflection and theories of truth Abstract: This talk explores the relationship between the global reflection principle ("If A is provable, A is true") and its arithmetic cousins ("If A is provable then A"). I will provide a proof-theoretic analysis of a number of axiomatic theories of truth expanded by transfinite hierarchies of reflection principles. Katsuhiko Sano (School of Information Science, Japan Advanced Institute of Science and Technology) title: What is the corresponding first-order logic to coalgebraic modal logic? Abstract: It is well-known that modal logic over Kripke models can be regarded as the bisimulation-invariant fragment of first-order logic, where the notion of bisimulation tells us when given two Kripke models are `similar' with each other. This is called Van Benthem's characterization theorem. The main aim of this talk is to propose a corresponding first-order syntax with Van Benthem-style characterization to coalgebraic modal logic, a uniform framework to cover modal logic over Kripke models, modal logic over neighborhood models, graded modal logic, probabilistic modal logic, etc. This talk focuses on a conceptual background to explain our strategy of finding a corresponding FO syntax for coalgebraic modal logic. A key idea consists in Arthur Prior's early idea of hybrid logic (esp. modal operators for pointed truth) and C. C. Chang's FO syntax for neighborhood models. This talk is based on a joint work with Dirk Pattinson (ANU), Tadeusz Litak (Friedrich-Alexander University of Erlangen and Nuremberg (FAU)), and Lutz Schroeder (FAU). Leon Horsten (University of Bristol) title: One hundred years of semantic paradox Abstract: This article contains an overview of the main problems, themes and theories relating to the semantic paradoxes in the twentieth century. From this historical overview I tentatively draw some lessons about the way in which the field may evolve in the next decade. Philip Welch (University of Bristol) title: Alan Turing's Mathematical work -- このメールは Google グループのグループ「京都現代哲学コロキアム」の登録者に送られています。このグループから退会し、メールの受信を停止するには、kyoto_colloquium+unsubscribe(a)googlegroups.com にメールを送信します。その他のオプションについては、https://groups.google.com/groups/opt_out にアクセスしてください。

1 0

ELC研究集会：3月14(木） ), 13(水), 17(日)午後午後
by Jun Tarui 30 Jan '13

30 Jan '13

みなさま，電通大の垂井です．計算限界解明プロジェクト http://www.al.ics.saitama-u.ac.jp/elc/ のキックオフメイン集会とサテライト集会に関してプログラム作成と企画の主担当をしています．まだ調整中の部分もあるのですが，みなさまの参考のために現時点での予定をお伝えします．ぜひ参加ご検討ください．サテライト集会：参加費なしで登録不要です．当日夕方に参加希望を現地で尋ねる形の懇親食事会を予定しています．メイン集会：参加費はなしですが，一部講演のみ聴講の場合でも登録をお願いしています．登録締め切りは２月２８日です．よろしくお願いします．垂井淳 -------------------------------------------- Exploring the Limits of Computation (ELC) Tokyo Complexity Workshop and Satellite Mini-Workshops: http://www.al.ics.saitama-u.ac.jp/elc/ws/ Mar13(Wed) Satellite Mini-Workshop, Shinagawa venue: Kyoto Univ Shinagawa Office, Shinagawa http://www.kyoto-u.ac.jp/ja/tokyo-office http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Yoshio Okamoto(UEC), Suguru Tamaki(Kyoto U), Jun Tarui(UEC) each talk will have a 15-min break in the middle 10:30--12:15 TBA 12:15--13:40 lunch (on your own) 13:40--15:25 Ran Raz: Parallel Repetition of Two Prover Games: A Survey 15:25--15:45 break 15:45--17:30 Noam Nisan: Algorithmic Mechanism Design: Multi-unit Auctions 18:00-- impromptu dinner party at Shinagawa Mar17(Sun) Satellite Mini-Workshop on Geometric Complexity Theory(GCT) venue: 2nd floor meeting room, Campus Innovation Center, Tamachi http://www.cictokyo.jp/access.html http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Takeshi Tokuyama(Tohoku U), Susume Ariki(Osaka U), Jun Tarui(UEC) speakers: Ketan Mulmuley and Joshua Grochow 14:00--18:15 (with 3 breaks) 18:30-- impromptu dinner party at Tamachi Mar19(Tue) Satellite Mini-Workshp, Kyoto venue: Room 111, RIMS, Kyoto Univ, Kyoto http://www.kurims.kyoto-u.ac.jp/en/access-01.html http://goo.gl/aCgSE registration not necessary; no participation fee; everybody is welcome organizers: Shin-ichi Tanigawa(RIMS), Suguru Tamaki(Kyoto U), Jun Tarui(UEC) 13:15--14:15 Raghu Meka: Beating the Union Bound via Gaussian Geometry 14:15--14:30 break 14:30--15:30 Zeev Dvir: Locally Decodable Codes: recent progress and open problems 15:30--15:45 break 15:45--17:15 Ketan Mulmuley: talk on geometric complexity theory 18:00-- impropmtu dinner party around Sanjo/Shijo-Kawara-machi Tokyo Complexity Workshop (Main Workshop): tentative schedule as of Jan 30th venue: Shinagawa Prince Hotel, Main Tower 8th floor, Room: "Turquoise 8" http://www.al.ics.saitama-u.ac.jp/elc/ws/ http://goo.gl/aCgSE fee for reception/banquet; no fee otherwise; please register in all cases Mar14(Thu) 13:20--13:30 opening 13:30--14:20 Umesh Varirani: Quantum Hamiltonian Complexity: through the computational lens 14:20--14:35 break 14:35--15:25 Rahul Jain: TBA 15:25--15:40 break 15:40--16:30 Pavel Pudlak: Polynomial Hierarchy and Bounded Arithmetic Hierarchy. 16:30--16:45 break 16:45--17:35 Ryan O'Donnell: Approximability and Proof Complexity 18:00--20:00 reception Mar15(Fri) 09:00--09:50 Noam Nisan: Selling Two Objects (in Three Models) 09:50--10:15 break 10:15--11:05 Ketan Mulmuley: The GCT Chasm 11:05--11:30 break 11:30--12:20 Joshua Grochow: Geometric Complexity Theory unifies and generalizes many known lower bounds (an introduction to GCT) 12:20--14:00 lunch 14:00--14:50 Shachar Lovett: The probabilistic method - new frontiers 14:50--15:15 break 15:15--16:05 Zeev Dvir: Locally Decodable Codes: recent progress and open problems 16:05--16:30 break 16:30--17:20 Luca Trevisan: TBA Mar16(Sat) 09:00--09:50 Raghu Meka: Recent Progress in Unconditional Derandomization 09:50--10:15 break 10:15--11:05 David Zuckerman: Pseudorandomness from Shrinkage 11:05--11:30 break 11:30--12:20 Irit Dinur: TBA 12:20--14:00 lunch 14:00--14:50 Rocco Servedio: TBA 14:50--15:15 break 15:15--16:05 Pinyan Lu: TBA 16:05--16:30 break 16:30--17:20 Ran Raz: Interactive Channel Capacity 18:00--20:00 banquet Mar17(Sun) 09:00--09:50 Valentine Kabanets: Yin and Yang of computing: From circuit lower bounds to compression and SAT algorithms, and back 09:50--10:05 break 10:05--10:55 Eric Allender: Strengthening the Link between Complexity Classes and Kolmogorov Complexity 10:55--11:10 break 11:10--12:00 Yuichi Yoshida: Robust approximation of CSPs: Universal algebra meets optimization Speakers: Eric Allender (Rutgers) www.cs.rutgers.edu/~allender/ Irit Dinur (Weizmann) www.wisdom.weizmann.ac.il/~dinuri/ Zeev Dvir (Princeton) www.cs.princeton.edu/~zdvir/ Josh Grochow (U Toronto) www.cs.toronto.edu/~jgrochow/ Rahul Jain (Nat Univ Singapore) www.comp.nus.edu.sg/~rahul/ Valentine Kabanets (Simon Fraser) www.cs.sfu.ca/~kabanets/ Shachar Lovett (Princeton, IAS) https://sites.google.com/site/shacharlovetthomepage/ Pinyan Lu (Microsoft Research Asia and Shanghai Jiao Tong Univ) http://research.microsoft.com/en-us/people/pinyanl/ Raghu Meka (Princeton, IAS) www.math.ias.edu/~raghu/ Ketan Mulmuley (Chicago) www.cs.uchicago.edu/people/mulmuley Noam Nisan (Hebrew U) www.cs.huji.ac.il/~noam/ Ryan O'Donnell (CMU) www.cs.cmu.edu/~odonnell/ Pavel Pudlak (Math Institute of Czech Republic) www.math.cas.cz/~pudlak/ Ran Raz (Weizmann) www.wisdom.weizmann.ac.il/~ranraz/ Rocco Servedio (Columbia) www.cs.columbia.edu/~rocco/ Luca Trevisan (Stanford) http://theory.stanford.edu/~trevisan/ Umesh Vazirani (UC Berkeley) http://www.cs.berkeley.edu/~vazirani/ Yuichi Yoshida (National Institute of Informatics, Tokyo) http://research.nii.ac.jp/~yyoshida/ David Zuckerman (U Texas, Austin) www.cs.utexas.edu/~diz/

1 0

Logic Zoo Workshop 2013 プログラム (1月31日東京)
by Yoichi Hirai 25 Jan '13

25 Jan '13

みなさま東京大学萩谷研の平井洋一です。先般ご案内のLogic Zooワークショップのプログラムを流します。ご参加お待ちしております。平井洋一 ◆日時と場所 2013年1月31日(木) 10:00〜17:00 東京大学本郷キャンパス化学東館236室(理学部7号館より入る) ◆プログラム 10:00〜11:30 (TBA) ・Kazuyuki Asada (NII) 　Curry-Howard Correspondence between Dialectica Interpretation and Bidirectional Transformation ・Yoshihiko Kakutani (Univ. Tokyo) and/or Daisuke Kimura (NII) 　What is natural numbers in call-by-name lambda-mu? ・Ichiro Hasuo (Univ. Tokyo) 　Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications 12:00〜13:00 (TBA) ・Mamoru Kaneko (Univ. Tsukuba) 　Infinite Regresses arising from Prediction/Decision Making in Games (with Tai-Wei Hu) ・Yoichi Hirai (Univ. Tokyo) 　Complexity of Conditinal XPath Containment 14:00〜15:00 (TBA) ・Andrzej Murawski (Univ. Warwick) 　TBA ・Kensuke Kojima (Kyoto University) 　A Hoare logic for SIMT programs 15:30〜17:00 (Yoichi Hirai) ・Shunsuke Yatabe (Kyoto University (AIST)) 　Naive Set Theory and Coinduction ・Masaki Hara (Univ. Tokyo) 　Coqで直観主義命題論理の決定性を証明する (On proving decidability of Intuitionistic Propositional Calculus on Coq) ・Toshiki Takahashi (Free Scientist) 　Botanical Shapes Generated by 3rd Data Structure, "Poker" ◆その他情報 http://logiczoo13.pira.jp/

1 0

Jump to page:

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml