A BRICS Mini-Course
December 18, 1996
The main concern of this Mini-course is to give an introduction to Linear Logic. For pedagogical purposes we shall also have a look at Classical Logic as well as Intuitionistic Logic. Linear Logic was introduced by J.-Y. Girard in 1987 and it has attracted much attention from computer scientists, as it is a logical way of coping with resources and resource control. Several hundred papers have been written on the topic. Applications of Linear Logic include linear functional programming, linear logic programming, planning and AI, and general theories of concurrency. The focus of this Mini-course will be on proof-theory and computational interpretation of proofs, that is, we will focus on the question of how to interpret proofs as programs and reduction (cut-elimination) as evaluation. No proofs will be given, rather, the emphasis will be on basic ideas.
The course is based on a technical report introducing Linear Logic. A draft version of the report will be handed out at the course, and a final version will be worked out later.