[Prev][Next][Index][Thread]
Linear Logic 96
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
[Apologies to those who see this twice. Mailer difficulties
mean the first circulation may not have reached everyone.
-- Philip Wadler, moderator, Types Forum]
Linear Logic 96 Tokyo Meeting Program
(Co-sponsored by Keio University,
Japan Society for Scientific Promotion,
Centre National de Recherche Scientifique(France),
and Office of Naval Research(USA))
WWW page: http://abelard.flet.mita.keio.ac.jp/Linear96.html
---------------------------------------------------------------------------
Linear Logic 96 Tokyo Meeting (March 28 -- April 2)
(the Main Hall of the "Kitashinkan" Building, the Mita Campus, Keio Univ.)
Special Tutorials
Jean-Yves Girard Tutorial I: Recent Advances in Linear Logic
P.Lincoln-J.Mitchell Tutorial II: Decision and Optimization Problems
-A.Scedrov in Linear Logic
28 March (Thursday)
6:00pm-8:30pm Pre-Registration and Welcome Reception
(the Faculty Club of the "Kitashinkan" Building)
29 March (Friday)
8:50-9:20 Registration/Coffee and muffins (light breakfast)
9:20-10:20
J-Y.Girard Tutorial I: Recent Advances in Linear Logic
10:20-10:40 Coffee Break
10:40-12:10 Morning Session
Peter O'Hearn From Algol to Polymorphic Linear Lambda-Calculus,I
John Reynolds From Algol to Polymorphic Linear Lambda-Calculus,II
12:10-1:30 Lunch Break
1:30-3:00 Afternoon Session I
Samson Abramsky Linearity, Sharing and State
Kohei Honda Relating Proof Nets and Pi-Calculus
3:00-3:15 Coffee Break
3:15-5:30 Afternoon Session II
Andre Joyal Free Bicompletion of Categories and Linear Logic
Dale Miller Linear Logic as a Logical Framework
Kobayashi-Yonezawa Linear Concurrent Logic Programming (tentative)
5:30-5:45 Break
5:45-6:45
Lincoln-Mitchell- Tutorial II: Decision and Optimization Problems
Scedrov in Linear Logic
30 March (Saturday)
8:50-9:20 Coffee and muffins (light breakfast)
9:20-10:20
J-Y. Girard Tutorial I: Recent Advances in Linear Logic
10:20-10:40 Coffee Break
10:40-12:10 Morning Session
Vincent Danos Abstract Machines and Games Semantics I
Laurent Regnier Abstract Machines and Games Semantics II
12:10-1:40 Lunch Break
1:40-3:35 Afternoon Session I
Francois Lamarche From Proof Nets to Games.
C-H L Ong A semantic view of classical proofs: type-theoretic,
categorical and denotational characterizations
Thomas Ehrhard A characterization of strongly stable functions
in terms of sequential algorithms
3:35-3:50 Coffee Break
3:50-5:20 Afternoon Session II
V. Michele Abrusci Semantics of proofs for noncommutative linear logic
Mitsu Okada From Phase Semantics to Higher Order Normalization
5:20-5:30 Break
5:30-6:30
Lincoln-Mitchell- Tutorial II: Decision and Optimization Problems
Scedrov in Linear Logic
6:30-8:30 Panel Discussion and Conference Reception
(Panelists: S. Abramski, J-Y Girard, J. Mitchell)
31 March (Sunday)
8:50-9:20 Coffee and muffins (light breakfast)
9:20-10:20
J-Y. Girard Tutorial I: Recent Advances in Linear Logic
10:20-10:40 Coffee Break
10:40-12:10 Morning Session
Andrea Asperti Paths and optimal reductions in the
lambda-calculus: an introduction.
Susumu Hayashi Two extensions of PX system
12:10-1:20 Lunch Break
1:20-3:35 Afternoon Session I
Hiroakira Ono Algebraic semantics for substructural logics
Peter Freyd Paracategaries, paramathematics
Vaughan Pratt Linear logic complements classical logic
3:35-3:50 Coffee Break
3:50-6:50pm Special Session on the Related Fields
Gaisi Takeuti Logical Approach to Computational Complexity Theory
Dag Prawitz Proof Theory, its Past and Future
Dirk van Dalen What is Constructivity?-the Intuitionist Approach-
in Linear Logic
7:30-10:00 Conference Banquet
1st April (Monday)
8:50-9:20 Coffee and muffins (light breakfast)
9:20-10:20
J-Y. Girard Tutorial I: Recent Advances in Linear Logic
10:20-10:40 Coffee Break
10:40-12:10 Morning Session
Phil J.Scott Representations of Groups and Hopf Algebras
in Linear Proof Theory I
Rick Blute Representations of Groups and Hopf Algebras
in Linear Proof Theory II
12:10-1:20 Lunch Break
1:20-3:35 Afternoon Session I
Max Kanovitch Enriching LL by temporal-like operators "next"
and "afterwards"
Natarajan Shankar The Mechanics of Proof Search in Linear Logic
Jacqueline Vauzeilles Linear Logic for Taxonomical Networks and
Database Updates
Presentation by Title:
Christian Retore Proof structures and perfect matchings.
3:35-3:45 Coffee Break
3:45-6:00 Afternoon Session II
Misao Nagayama Graph-Theoretic Characterization of Proof Nets
of Non-Commutative MLL
Francois Metayer Some remarks on cyclic linear logic
Makoto Kanazawa Lambek calculus: recognizing power and complexity.
6:00-6:05 Break
6:05-7:05
Lincoln-Mitchell- Tutorial II: Decision and Optimization Problems
Scedrov in Linear Logic
2nd April
9:30-12:00 Contributed Papers Session
Joshua S. Hodas Forum as a Logica Programming Language
-Jeffrey Polakow (Preliminary Results and Observations)
Marco Pedicini Remarks on Elementary Linear Logic
Vincent Danos, Computational isomorphisms in classical logic
-Jean-Baptiste Joinet,
-Harold Schellinx
Lorenzo Tortora Generalized standardization lemma for the additives
de Falco
End of the Formal Program of Linear 96.
---------------------------------------------------------------------------
---------------------------------------------------------------------------
Linear Logic Mini-Courses (March 25 -- 27)
(the AV-Hall of the Main Library, the Mita Campus, Keio Univ)
[I] Introduction to Linear Logic, by Girard-Lafont-Okada-Scedrov(10:30--12:30)
[P] Proof Nets and Interaction Nets, by Y. Lafont (2:00--3:30)
[D] Decision Problems in Linear Logic, by A. Scedrov (4:00--5:30)
25 26 27
10:30 [I] [I] [I]
12:30 Break Break Break
2:00 [P] [P] [P]
4:00 [D] [D] [D]
-----------------------------------------------------------------------
Linear Logic 96 Tokyo Meeting (March 28 -- April 2)
(the Main Hall of the "Kitashinkan" Building, the Mita Campus, Keio Univ.)
Invited speakers:
>From Europe:
M. Abrusci, Univ Roma
S. Abramsky, Edinburgh Univ
A. Asperti, Bologna Univ
D. van Dalen, Univ Utrecht
V. Danos, Paris VII
T. Ehrhard, LMD-Marseille
J-Y. Girard, LMD-Marseille
M. Kanovitch, Moscow Humanity Univ
Y. Lafont, LMD-Marseille
F. Lamarche, Univ Nancy
F. Metayer, Paris VII
L. Ong, Oxford Univ and National Univ Singapore
P. O'Hearn, Syracuse Univ/Queen Mary and Westfield College,Univ London
D. Prawitz, Univ Stockholm
L. Regnier, LMD-Marseille
J. Vauzeille, Univ Paris XIII
>From North America:
R. Blute, Ottawa
P. Freyd, Univ Penn
A. Joyal, Univ Quebec-Montreal
P. Lincoln, SRI/Stanford Univ
J. Mitchell, Stanford Univ
D. Miller, Univ Penn
V. Pratt, Stanford Univ
J. Reynolds, Carnegie Mellon Univ
A. Scedrov, Univ Penn
P. Scott, Univ Ottawa
N. Shankar, SRI
G. Takeuti, Univ Illinois-Urbana
>From Japan:
S.Hayashi, Univ Kobe
N.Kobayashi, Univ Tokyo
M.Kanazawa, Univ Chiba
K.Honda, Univ Manchester/Keio Univ
M.Nagayama, TWCU
M.Okada, Keio Univ
H.Ono, JAIST
A.Yonezawa, Univ Tokyo
Scientific Program Comittee:
Jean-Yves Girard (LMD-CNRS, Marseille, France)
Mitsu Okada (Keio Univ, Japan)
Andre Scedrov (Univ. of Pennsylvania, USA).
Local Organizing Comittee:
Y. Fujiwara (Toshiba Lab)
K. Mukai (Keio Univ)
M. Nagayama (TWCU)
M. Okada (Keio Univ)
M. Takahashi-Horai (Titech)
---------------------------------------------------------------------------
Post-Conference Activities
Apr 2, 1:00pm -- 6:00pm "Philosophy of Mathematics" Symposium,
(the International Meeting Room of the fourth
floor of the "Kitashinkan" building)
organizers: H. Ishiguro(Keio Univ)
and M. Okada(Keio Univ)
speakers: J-Y. Girard(CNRS, France),
T. Iida(Chiba Univ),
M. Okada(Keio Univ),
C. Parsons(Harvard Univ, USA),
D. Prawitz(Stockholm Univ, Sweden),
G. Takeuti(Illinois Univ, USA),
D. van Dalen(Utrecht Univ, Netherlands)
6:00pm -- 8:00pm Reception (Faculty Club)
Apr 3, 10:00am-- 3:00pm "History of Logic" Symposium,
(the International Meeting Room of the fourth
floor of the "Kitashinkan" building)
organizers: H. Ishiguro(Keio Univ)
and M. Okada(Keio Univ)
speakers: J.J. Katz(New York Univ, USA),
H. Sinaceur(CNRS, France),
D. van Dalen(Utrecht Univ, Netherlands)
Apr 3, 3:30pm -- ALGI96 Seminar (the AV-Hall of the Mail Library)
organizer: Y. Akama(Univ. Tokyo)
Apr 4, 10:00am-- ALGI96 Seminar (the AV-Hall of the Mail Library)
organizer: Y. Akama(Univ. Tokyo)
Apr 5, 10:00am-- ALGI96 Seminar (the AV-Hall of the Mail Library)
organizer: Y. Akama(Univ. Tokyo)
Apr 4, 9:30am -- 4:00pm Protcol Verification System Workshop
(room 102, building 1)
(organized by SRI-International,
organizer: N. Shankar,
lecturer: P. Lincoln
------------------------------------------------------------------------
------------------------------------------------------------------------
A Tutorial/Workshop on Formal Specification and Verification Using PVS
Patrick Lincoln, SRI International
April 4, 1996 at Kieo University (Mita Campus),
Room 102, Buliding 1
9.30am to 4pm (with a break for lunch)
PVS (Prototype Verification System) is a mechanized tool for formal
specification and verification of safety critical systems that has been
developed by researchers at the SRI International computer science
laboratory. The PVS system integrates a number of advanced capabilities
for specification and verification such as induction, rewriting, linear
arithmetic, Boolean simplification, and symbolic model checking within
a highly interactive framework. It has been applied to several hard
problems in fault-tolerant and real-time algorithms, hardware
verification, and computing. Formally verified examples include various
fault-tolerant agreement and diagnosis algorithms, the correctness of
commercial-scale processor designs, and more recently, the design of an
SRT divider. PVS is available from SRI and various mirror sites in
England, France, and Germany by anonymous FTP. See the web site:
http://www.csl.sri.com/pvs.html for details.
The tutorial is open to any interested participant. This tutorial will
review the basic capabilities of PVS and provide glimpses of several of
its more advanced features. The purpose of the tutorial is give
attendees an appreciation for the scope and power of modern mechanizations
of formal methods, and for the opportunities these create for efficient
and effective use of formal methods in a variety of application areas.
The tutorial will be conducted as a live demonstration using a workstation
with projection capabilities. The tutorial will be conducted by Patrick
Lincoln, who is a member of the PVS development team at SRI and an expert
PVS user.
There will be time for short presentations on any topic of relevance to
mechanized formal methods in general, or PVS in particular. Please
send email to shankar@csl.sri.com if you would like to make such a
presentation.
The topics covered in the tutorial include:
* Some introductory tutorial examples
* The PVS Language: Type System, Definitions, the prelude library,
Parametric theories, Recursive datatypes, Tables,
Inductive relations, Libraries.
* The PVS Prover: Propositional Logic, Quantification,
Decision Procedures, Rewriting, Proof Strategies,
Induction, BDD-based symbolic model checking.
* Advanced Applications
There is no registration for this tutorial. For more details,
please send email to shankar@csl.sri.com or phone Mr. Eiji Kitahara (SRI,
Tokyo) at +(81) 03-3505-8914; Fax +(81) 03-3505-8920.