Workshop on Linear Logic, Proof Theory
and Computer Science
(with Lecture Series by Jean-Yves Girard)
March 16-17, 2006

Mita Logic Seminarの企画でLinear Logicの進化 及び関連するProof Theoryの発展とその哲学的側面や 計算機科学的側面への応用に関する次のようなワークショップを 開催します．参加は自由です． Jean-Yves Girard教授の連続講義も予定されています．

Place:

慶應義塾大学三田キャンパス東館6階G-secホール
Keio University, Mita-Campus (downtown Tokyo, 5 minutes walk from JR-Tamachi St or Subway-Mita St), 6F Hall of the East Building (G-SEC laboratory)
http://www.keio.ac.jp/access.html

March 16, Thursday

10:40-12:00

Invited lecture series:
Jean-Yves Girard (Marseille, IML), ``Evolutions of Proof Theory Part I"

12:00-13:30

Lunch Break

13:30-14:30

Special Lecture:
Naoki Kobayashi (Tohoku University), ``Linearity and Order in Type Systems for Programming Languages"

14:30-14:40

Discussion and Coffee Break

14:40-16:00

Session I:

Martin Berger

(Queen Mary, Univ of London), ``Process Calculi and Interaction Types"

Sylvain Salvati

(NII), ``Type systems for syntax"

16:00-16:20

Discussion and Coffee Break

16:20-18:00

Session II:

Makoto Tatsuta

(NII), ``Different Substitution Theorem" (joint work with Mariangiola Dezani-Ciancaglini)

Hiroshi Unno

(University of Tokyo), Naoki Kobayashi (Tohoku University), Akinori Yonezawa (University of Tokyo), ``Combining Type-Based Analysis and Model Checking for Static Detection of Information Leakage"

Koji Hasebe

(Keio University), Mitsuhiro Okada (Keio University), ``Correctness Proofs and Counter-Example Generations with Basic Protocol Logic"

March 17, Friday

10:30-12:00

Invited lecture series:
Jean-Yves Girard (Marseille, IML), ``Evolutions of Proof Theory Part II"

12:00-13:30

Lunch Break

13:30-15:20

Session III:

Olivier Laurent

(PPS CNRS-Université Paris VII), ``Predicate calculus, game semantics and Krivine's realisability"

Patrick Baillot

(LIPN, CNRS-University Paris 13), ``Inferring Light types for guaranteeing polynomial time bounds in system F" (joint work with Vincent Atassi, Kazushige Terui)

Kazushige Terui

(NII), ``Linear intersection types for computational complexity (tentative)"

15:20-15:50

Discussion and Coffee Break

15:50-17:30

Session IV:

Shoji Yuen

(Nagoya University), ``Process Languages with discrete time"

Masahiro Hamano

(Keio University), ``Characters of Group Representations and Compact Closed Full Completeness''

Ryo Takemura

(Keio University）, Mitsuhiro Okada (Keio University), ``Lorenzen Style Traditional Games Revisited from a Sequent Calculus View (Report of an on-going work)"

主催:

本研究会は科学研究費（基盤研究「充実期を迎えた線形論理の進化と その応用に関する研究」国際共同研究グループ）により 支援されています。

協力:

慶應義塾大学CIRM（人文科学COE）及び 文学研究科魅力ある大学院教育イニシアティヴ論理学グループ

Okada Laboratory, Dept. of Philosophy, Keio University
address: 2-15-45 Mita, Minato-ku, Tokyo
phone: 03-5427-1156 (ext. 23864)
e-mail: philosophy at abelard.flet.keio.ac.jp