Dagstuhl Seminar on Linear Logic and Applications

22-27 August 1999.

Organised by Valeria de Paiva, Josef van Genabith and Eike Ritter

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.

• Applications to verification and specification: There were two presentations on using linear logic for formal specification and verification. Both stated that linear logic appeared to provide a compact and intuitive representation for a variety of problems, as compared to many other logical specification languages. However, the need for a combined linear and temporal logic was clearly felt.
• There was a large representation of linguistic applications. A repreated theme was a need for proof search methods that could efficiently uncover all distinct proofs of a given formula from a set of premises; distinct proofs either corresponding to distinct parses of a sentence, or distinct semantic interpretations of a parse. Many of the linguistic applications employed some version of categorial grammar, which through the Lambek calculus bear close connections to linear logic. However, the applications were not limited to this one style of linguistic theory: there were presentations on how linear logic could account for the resource sensitive nature of minimalism, how it could be used for rewrite rules in machine translation, and how categorial semantics could be combined with other grammatical theories. There was additionally discussion of how proof nets could account for observed processing costs in different types of linguistic construction. There was also discussion of how LL could be used to encode pragmatic distinctions (in natural language meanings), e.g. between assertions of fact, obligations.
• There were also presentations on the application of linear logic to functional programming. There has been a longstanding hope that the resource/usage counting aspects of linear logic could be used to allow efficient memory management / garbage collection in functional languages. Presentations showed how this goal could be met in a number of useful special cases, but higher-order functions continue to raise problems for the more general goal.
• Proof theory, search and syntax: Talks on proof search and checking included a discussion of potentially incremental connection methods, and the presentation of a linear time algorithm for multiplicative linear logic. There were also presentations on the treatment of quantifiers as infinite tensors and pars, as well as the significance for various translations / embeddings between logics.