[Prev][Next][Index][Thread]
Workshop on Theories of Types and Proofs
Final Program
Workshop on Theories of Types and Proofs (TTPTokyo)
Satellite Workshop of TACS'97
September 8  18, 1997
Tokyo Institute of Technology
Tokyo, Japan
<ttp@is.titech.ac.jp>
http://www.is.titech.ac.jp/ttp/
Partially sponsored by the Mathematical Society of Japan and
Tokyo Institute of Technology
The aim of this twoweek workshop is to exchange ideas and research results
in the area of Theories of Types and Proofs. Researchers interested in this
area are welcome to participate in the workshop. The workshop will consist
of a series of lectures and contributed talks, both of which contain enough
discussion hours.
The workshop period is just before the sister workshop TTPKyoto at Kyoto,
Japan (September 19  20) and the TACS'97 conference at Sendai, Japan
(September 23  27).
You can also get information about TTPKyoto and TACS at the following URLs:
http://wwwfun.kurims.kyotou.ac.jp/ttpkyoto/ for the
http://tacs97.ito.ecei.tohoku.ac.jp/tacs97.html
Our Web page is at http://www.is.titech.ac.jp/ttp.
==============
September 8
Chairman: Masako Takahashi

11:0012.30
Stefano Berardi (University of Torino):
 Yet Another Constructivization of Classical Logic (part I)
Chairman: Stefano Berardi

14.3016:00
Susumu Hayashi (Kobe University)
 Comparing constructive programming with practical formal methods
  Constructive programming is possible but not indispensable 

16.3017.30
Kenetsu Fujita (Kyushu Institute of Technology)
 A simple system of classical propositional logic
============
September 9
Chairman: Masahiko Sato

9:0010.30
Stefano Berardi (University of Torino):
 Yet Another Constructivization of Classical Logic (part II)

11:0012.30
Susumu Hayashi (Kobe University)
 Towards Proof Animation from Constructive Programming
Chairman: Susumu Hayashi

14.3016:00
Henk Barendregt (Catholic University Nijmegen):
 The methodology of proofchecking.

16.3017.30
Ichiro Ogata (Electrotechnical Lab. Japan)
 A proof theoretical approach to "classical proofs as programs"
===============
September 10
Chairman: Susumu Hayashi

9:0010.30
Henk Barendregt (Catholic University Nijmegen):
 Systems for formalizing proofs.

11:0012.30
Masahiko Sato (Kyoto University)
 Classical BrouwerHeytingKolmogorov interpretation
Chairman: Masahiko Sato

14.3016:00
Sachio Hirokawa (Kyushu University)
 What is a lambdacalculus for classical logic?

============
September 11
Chairman: Stefano Berardi

9:0010.30

Sachio Hirokawa (Kyushu University)
 Principal types of lambdaterms and their application to the
 analysis of proofs

11:0012.30
Henk Barendregt (Catholic University Nijmegen):
 The technology of proofchecking.
Chairman: Henk Barendregt

14.3015.30
Martijn Oostdijk, Herman Geuvers (Eindhoven University of Technology)
 Proof by Computation in the Coq system

16:0017:00
Tarmo Uustalu (Royal Institute of Technology)
Vermo Vene (University of Tarku)
 A cube of naturaldeduction calculi for intuitionistic mu,nulogic
=============
September 12

Chairman: Henk Barendregt

9:0010.30
Masako Takahashi (Tokyo Institute of Technology)
 Lambdarepresentable functions over free structures revisited

11:0012.30
Mariangiola Dezani (University of Torino, Tokyo Inst. of Technology)
 Trees and Types
Chairman: Sachio Hirokawa

14.3016:00
Hiroakira Ono (Jaist)
 An introductory course of prooftheoretic methods
 in nonclassical logic (Part I)

16.3017.30
Malgorzata Moczurad, Marek Zaionc (Jagiellonian University)
 Lambdarepresentability by Linear Terms. The case study of type
 (N > N) > N.
==============
September 13
Chairman: Mariangiola Dezani

9:0010.30
Hiroakira Ono (Jaist)
 An introductory course of prooftheoretic methods
 in nonclassical logic (Part II)

11:0012:30
Hirofumi Yokouchi (Gunma University)
 Syntax and semantics of type assignment systems
==============
September 15
Chairman: Hirofumi Yokouchi

9:0010.30
Ryu Hasegawa (University of Tokyo)
 Applications of analytic functors to theoretical computer science
 (part I)

11:0012.30
Mitsu Okada (Keio University)
 A semantic framework for computation models based on classical
 linear logic and classical linear type theory.
Chairman: Mitsu Okada

14.3015.30
Franco Barbanera (University of Torino), Maribel Fernandez (ENS),
Steffen van Bakel (Imperial College)
 A type assignment system with polymorphic and intersection types
 for term rewriting systems with betarule

16:0017:00
Yoko Motohama (JAIST)
 The callbyvale type discipline over the minimal relevant logic B+
===============
September 16
Chairman: Luke Ong

9:0010.30
Mitsu Okada (Keio University)
 Inductive type theory + algebraic rewriting

11:0012.30
Ryu Hasegawa (University of Tokyo)
 Applications of analytic functors to theoretical computer science
 (part II)
Chairman: Ryu Hasegawa

14.3016:00
Luke Ong (Oxford University)
 Game semantics for lambda calculus (part I)

16.3017.30
Izumi Takeuti (Kyoto University)
 A type theory for cyclic structure
================
September 17
Chairman: Mitsu Okada

9:0010.30
Mario Coppo (University of Torino)
 A type inference approach to program analysis.

11:0012.30
Luke Ong (Oxford University)
 Game semantics for lambda calculus (part II)
Chairman: Luke Ong

14.3016:00
Ryu Hasegawa (University of Tokyo)
 Applications of analytic functors to theoretical computer science
 (part III)

16.3017.30
Satoshi Matsuoka (Nagoya Institute of Technology)
 Nondeterministic Linear Logic
============
September 18
Chairman: Ryu Hasegawa

9:0010.30
Luke Ong (Oxford University)
 Game semantics for lambda calculus (part II)

11:0012.30
Henk Barendregt
 Open Problem Session
The workshop is sponsored by the Mathematical Society of Japan as a part
of the regional workshop program of the society. A lecture note (including
lectures and original papers selected from contributed talks) will be published
as a volume in a new lecture note series of the Mathematical Society of Japan.
Workshop Organizers:
Mariangiola Dezani (University of Torino, Tokyo Inst. of Technology)
Mitsu Okada (Keio University)
Masako Takahashi (Tokyo Institute of Technology, chair)
Program committee:
Henk Barendregt (Catholic University Nijmegen)
Mariangiola Dezani (University of Torino, Tokyo Inst. of Technology)
Ryu Hasegawa (University of Tokyo)
Mitsu Okada (Keio University)
Masako Takahashi (Tokyo Institute of Technology, chair)
Hirofumi Yokouchi (Gunma University)
Local Arrangement:
Yohji Akama (University of Tokyo)
Toshihiko Kurata (Tokyo Institute of Technology)
Important dates:
registration for participants August 15, 1997
workshop September 8  18, 1997
.........................................................................
TTPTokyo Registration form
Name:
Email:
Affiliation:
Do you participate the whole period?
If not, specify the dates of your stay.
.........................................................................