[Prev][Next][Index][Thread]
Workshop on Theories of Types and Proofs
Final Program
Workshop on Theories of Types and Proofs (TTP-Tokyo)
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 two-week 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 TTP-Kyoto at Kyoto,
Japan (September 19 - 20) and the TACS'97 conference at Sendai, Japan
(September 23 - 27).
You can also get information about TTP-Kyoto and TACS at the following URLs:
http://wwwfun.kurims.kyoto-u.ac.jp/ttp-kyoto/ 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:00-12.30
|Stefano Berardi (University of Torino):
| Yet Another Constructivization of Classical Logic (part I)
|Chairman: Stefano Berardi
|
|14.30-16:00
|Susumu Hayashi (Kobe University)
| Comparing constructive programming with practical formal methods
| - Constructive programming is possible but not indispensable -
|
|16.30-17.30
|Ken-etsu Fujita (Kyushu Institute of Technology)
| A simple system of classical propositional logic
============
September 9
|Chairman: Masahiko Sato
|
|9:00-10.30
|Stefano Berardi (University of Torino):
| Yet Another Constructivization of Classical Logic (part II)
|
|11:00-12.30
|Susumu Hayashi (Kobe University)
| Towards Proof Animation from Constructive Programming
|Chairman: Susumu Hayashi
|
|14.30-16:00
|Henk Barendregt (Catholic University Nijmegen):
| The methodology of proof-checking.
|
|16.30-17.30
|Ichiro Ogata (Electrotechnical Lab. Japan)
| A proof theoretical approach to "classical proofs as programs"
===============
September 10
|Chairman: Susumu Hayashi
|
|9:00-10.30
|Henk Barendregt (Catholic University Nijmegen):
| Systems for formalizing proofs.
|
|11:00-12.30
|Masahiko Sato (Kyoto University)
| Classical Brouwer-Heyting-Kolmogorov interpretation
|Chairman: Masahiko Sato
|
|14.30-16:00
|Sachio Hirokawa (Kyushu University)
| What is a lambda-calculus for classical logic?
|
============
September 11
|Chairman: Stefano Berardi
|
|9:00-10.30
|
|Sachio Hirokawa (Kyushu University)
| Principal types of lambda-terms and their application to the
| analysis of proofs
|
|11:00-12.30
|Henk Barendregt (Catholic University Nijmegen):
| The technology of proof-checking.
|Chairman: Henk Barendregt
|
|14.30-15.30
|Martijn Oostdijk, Herman Geuvers (Eindhoven University of Technology)
| Proof by Computation in the Coq system
|
|16:00-17:00
|Tarmo Uustalu (Royal Institute of Technology)
|Vermo Vene (University of Tarku)
| A cube of natural-deduction calculi for intuitionistic mu-,nu-logic
=============
|September 12
|
|Chairman: Henk Barendregt
|
|9:00-10.30
|Masako Takahashi (Tokyo Institute of Technology)
| Lambda-representable functions over free structures revisited
|
|11:00-12.30
|Mariangiola Dezani (University of Torino, Tokyo Inst. of Technology)
| Trees and Types
|Chairman: Sachio Hirokawa
|
|14.30-16:00
|Hiroakira Ono (Jaist)
| An introductory course of proof-theoretic methods
| in nonclassical logic (Part I)
|
|16.30-17.30
|Malgorzata Moczurad, Marek Zaionc (Jagiellonian University)
| Lambda-representability by Linear Terms. The case study of type
| (N -> N) -> N.
==============
September 13
|Chairman: Mariangiola Dezani
|
|9:00-10.30
|Hiroakira Ono (Jaist)
| An introductory course of proof-theoretic methods
| in nonclassical logic (Part II)
|
|11:00-12:30
|Hirofumi Yokouchi (Gunma University)
| Syntax and semantics of type assignment systems
==============
September 15
|Chairman: Hirofumi Yokouchi
|
|9:00-10.30
|Ryu Hasegawa (University of Tokyo)
| Applications of analytic functors to theoretical computer science
| (part I)
|
|11:00-12.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.30-15.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 beta-rule
|
|16:00-17:00
|Yoko Motohama (JAIST)
| The call-by-vale type discipline over the minimal relevant logic B+
===============
September 16
|Chairman: Luke Ong
|
|9:00-10.30
|Mitsu Okada (Keio University)
| Inductive type theory + algebraic rewriting
|
|11:00-12.30
|Ryu Hasegawa (University of Tokyo)
| Applications of analytic functors to theoretical computer science
| (part II)
|Chairman: Ryu Hasegawa
|
|14.30-16:00
|Luke Ong (Oxford University)
| Game semantics for lambda calculus (part I)
|
|16.30-17.30
|Izumi Takeuti (Kyoto University)
| A type theory for cyclic structure
================
September 17
|Chairman: Mitsu Okada
|
|9:00-10.30
|Mario Coppo (University of Torino)
| A type inference approach to program analysis.
|
|11:00-12.30
|Luke Ong (Oxford University)
| Game semantics for lambda calculus (part II)
|Chairman: Luke Ong
|
|14.30-16:00
|Ryu Hasegawa (University of Tokyo)
| Applications of analytic functors to theoretical computer science
| (part III)
|
|16.30-17.30
|Satoshi Matsuoka (Nagoya Institute of Technology)
| Nondeterministic Linear Logic
============
September 18
|Chairman: Ryu Hasegawa
|
|9:00-10.30
|Luke Ong (Oxford University)
| Game semantics for lambda calculus (part II)
|
|11:00-12.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
.........................................................................
TTP-Tokyo Registration form
Name:
E-mail:
Affiliation:
Do you participate the whole period?
If not, specify the dates of your stay.
.........................................................................