Dagstuhl Seminar on Linear Logic and Applications
22-27 August 1999.
Organised by Valeria de Paiva, Josef van Genabith and Eike Ritter

[ Aim of the Seminar ] [ Overview ] [ Programme ] [ Abstracts ]

Aim of the Seminar

Linear Logic was introduced by J.-Y. Girard in 1987, and has attracted much attention from computer scientists as a logical way of coping with resources and resource control. The basic idea of Linear Logic is to consider formulae in a derivation as resources, which can be consumed or produced. To realize this basic idea we consider a logical system where the duplication and/or erasing of formulae must be explicitly marked using a unary operator, called an exponential or a modality. Rather than an alternative to Classical Logic, Linear Logic is a refinement of it: using Girard's well-known translation we can investigate the usage of resources in proofs of the traditional theorems. Linear Logic shares with Intuitionistic Logic a well-developed proof-theory and shares with Classical Logic the involutive behavior of negation, which makes its model theory particularly pleasant.

More importantly, because resource control is a central issue for Computer Science, Linear Logic has been applied to several areas within it, including functional programming, logic programming, general theories of concurrency, syntactic and semantic theories of natural language, artificial intelligence and planning. Several sessions in prestigious conferences like LiCS (Logic in Computer Science) as well as whole conferences (Cornell 1993, Tokyo 1995, Luminy-Marseille 1998) have been devoted to Linear Logic, a measure of the penetration of these ideas in the community.

We would like to survey the computational applications of Linear Logic, and bring together researchers working in different application areas. Towards this end, we are organizing this Dagstuhl Seminar.


Overview of the Workshop

The seminar contained talks concerning a number of different application areas of linear logic, as well as talks on more foundational issues.

Abstracts of the talks, sorted alphabetically by author, can be found
here.

Programme


Monday, 23 August

9.30h-10.30h

Mark Hepple

Implicational Linear Logic, Tree Descriptions
and Early Deduction. Slides.

10.30h-11.00h

Coffee

11.00h-12.00h

Alessandra Carbone

On the Geometry of Proofs

12.00h-14.00h

Lunch

14.00h-15.00h

David Pym

Bunched Logic/Dependent Type Theory and Their Semantics

15.00h-15.30h

Luiz Carlos Pereira

Translations, Normalization and Multiple-Conclusion Linear Logic

15.30h-16.00h

Coffee

16.00h-16.30h

Gianluigi Bellin

Programtic Interpretation of Substructural Logic

16.30h-17.30h

Dick Crouch

Linear Logic and Natural Semantics:
An Introduction to the Glue Approach.

Slides.

Tuesday, 24 August

9.00h-10.00h

Uday Reddy

Linear Logic in Modelling State

10.00h-10.30h

Coffee

10.30h-11.30h

Eike Ritter

Linear Abstract Machines with Single Pointer Property. Slides.

11.30h-14.00h

Lunch

14.00h-15.00h

Peter O'Hearn

Bunched Implications

15.00h-15.30h

Martin Hofmann

In place update with linear types or how to compile functional programs into malloc()-free C

15.30h-16.00h

Coffee

16.00h-16.30h

Geert-Jan Kruijff

Resource Logics, Formal Grammar and Processing

16.30h-17.00h

Coffee

17.00h-18.00h

David Sinclair

Using Linear Logic to Specify and Verify Protocols

Wednesday, 25 August

9.00h-10.00h

Andrea Schalk

Games and Linear Logic. Paper.

10.00h-10.30h

Coffee

10.30h-11.30h

Glyn Morrill

Proof Nets as Syntactic Structure of Language. dagstuhlslides1, dagstuhlslides2, dagstuhlslides3, dagstuhlslides4.

11.30h-14.00h

Lunch

Thursday, 26 August

9.00h-10.00h

Hermann Haeusler

Multiplicatively Quantified Linear Logic

10.00h-10.30h

Coffee

10.30h-11.30h

Francois Lamarche

Spaces for the Semantics of Linear Logic
and Linguistic Representation

11.30h-14.00h

Lunch

14.00h-14.45h

Philippe de Groote

Linear Logic and Categorial Grammars

14.45h-15.30h

Christian Retore

Linear Logic and Chomsky's Minimalist programme for Linguisitics

15.30h-16.00h

Coffee

16.00h-16.30h

Sara Kalvala

Linear Logic for Formal Verification

16.30h-17.00h

Coffee

17.00h-18.00h

Bertram Fronhoefer

Proof Search in Multiplicative Linear Logic Slides.

Friday, 27 August

9.00h-9.30h

Tsutomu Fujinami

A Decidable Linear Logic for Speech Translation

9.30h-10.00h

Akim Demaille

Mixed Logics

10.00h-10.30h

Coffee

10.30h-11.30h

Luke Ong

A Linear-Time Algorithm for Verifying MLL Proof Nets via Lamarche's Essential Nets. Paper.

11.30h-14.00h

Lunch


Back to top of page
+++++++++++++++++++++++++++

Page maintained by E.Ritter@cs.bham.ac.uk Last modified: Thu Oct 7 21:16:58 BST 1999