Logic-ml February 2013

logic-ml@fos.kuis.kyoto-u.ac.jp

15 participants
25 discussions

仙台ロジックスクール
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

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

Logic-ml February 2013