August 22 – 27, 1999, Dagstuhl Seminar 99341
Linear Logic and Applications
V. de Paiva (Birmingham), J. van Genabith (Dublin), E. Ritter (Birmingham)
For support, please contact
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.
In order to put together a program for the seminar reflecting the interests and activities of its participants, we are soliciting volunteers to give presentations on topics including, but not limited to:
- Linear Logic, its Syntax and Semantics
- Linear Logic for programming
- Implementations of Linear Logic
- Linear Logic in linguistics
- Linear Logic in artificial intelligence
We have invited participants to give short commentaries on other participants' presentations as a spur to more extended discussion.