LL 2002

Linear Logic
Copenhagen, Denmark, July 25-26, 2002
Affiliated with LICS 2002

Linear logic was invented by Girard in 1986, and first appeared as a finer analysis of his denotational semantics of system F. It provides a decomposition of the connectives of intuitionistic logic (more recently also have appeared some interpretations of classical logic into linear logic). It is important to note that linear logic is not yet another exotic logic, but a canonical mathematical object, with a well structured proof-theory, even simpler than that of classical and intuitionistic logics. It is only in 1986 that linear logic was clearly formulated as a logic and armed with its, by now common, tools; but it had appeared in 1979, in categorical guise, as Barr's `star-autonomous categories'; the `exponential' construction was already present in Blass' dialog-games as early as 1972; and even as early as 1958, a non- commutative fragment of linear logic was defined by Lambek. Since its invention it has spontaneously shown up in various fields and notably in the denotational semantics of programming languages.

Linear logic, by the decomposition of intuitionistic connectives it provides, but also by the new concepts it carries (geometrization of computations, management of resources at the logical level) opens a new dimension, already intensely exploited, in applications of logic to computer science, and at the same time is the locus of a mathematical theory within which mathematics is comfortably done. It is both a theory and a tool.

New possibilities show up at two levels, which we might call the language level and the operational level. Let us say that linear logic acts as a kind of a looking-glass through which phenomena of the field are better understood.

Though only fifteen years old, linear logic has spread in the computer science and logic communities, so that it can now be considered as a mature topic. The success of various international initiatives, such as the linear logic workshops at Cornell in 1993, in Tokyo in 1996, in Marseille in 1998; the linear logic bibliography web page at Carnegie Mellon University in the U.S. and also the various European projects where linear logic played or currently plays an important role, such as the Esprit projects CLiCS and CONFER, the HCM Network "Typed Lambda-Calculus" and the current LINEAR TMR network are concrete signs of vitality of the subject. In 2002 four years will have passed since the most recent international workshop on linear logic held in 1998 in Marseille, and the time will be ripe for a successful meeting.


Authors are invited to submit an extended abstract explaining recent research results or work in progress, in 5 pages or less, by April 29, 2002. The first page should include the title, the names, affiliations, and email addresses of the authors, and an abstract.

Papers should be submitted electronically as an email attachment to Andre Scedrov <> in an email message with the title "LL at FLoC'02" in order to distinguish it from everyday email. Paper formats are limited to portable postscript and PDF. Submissions that do not follow these instructions cannot be accepted. All accounted submissions will be confirmed by email. Submissions will be reviewed by the organizers and the authors will be informed of the decision by May 25, 2002.


LL 2002 is sponsored by LICS and the Association for Symbolic Logic.

Invited speakers

  • Richard Blute, U Ottawa, Canada
    Linear logic, relations and vector spaces
  • Stefano Guerrini, U Rome I (La Sapienza), Italy
    From proof nets to sharing graphs: From logic to implementations
  • Olivier Laurent, U Paris VII, France
    Polarities in linear logic
  • Kazushige Terui, IML Marseille, France
    On the complexity of cut elimination in linear logic