Constructive Logics. Part I: A Tutorial on Proof Systems and Typed λ-Calculi

The purpose of this paper is to give an exposition of material dealing with constructive logic, typed -calculi, and linear logic. The emergence in the past ten years of a coherent eld of research often named \logic and computation" has had two major (and related) eects: rstly, it has rocked vigorously the world of mathematical logic; secondly, it has created a new computer science discipline, which spans from what is traditionally called theory of computation, to programming language design. Remarkably, this new body of work relies heavily on some \old" concepts found in mathematical logic, like natural deduction, sequent calculus, and -calculus (but often viewed in a dierent light), and also on some newer concepts. Thus, it may be quite a challenge to become initiated to this new body of work (but the situation is improving, there are now some excellent texts on this subject matter). This paper attempts to provide a coherent and hopefully \gentle" initiation to this new body of work. We have attempted to cover the basic material on natural deduction, sequent calculus, and typed -calculus, but also to provide an introduction to Girard's linear logic, one of the most exciting developments in logic these past six years. The rst part of these notes gives an exposition of background material (with some exceptions, such as \contractionfree " systems for intuitionistic propositional logic and the Girard-translation of classical logic into intuitionistic logic, which is new). The second part is devoted to more current topics such as linear logic, proof nets, the geometry of interaction, and uni ed systems of logic (LU )