The main concern of this report 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. The focus of this technical
report 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. We rst introduce Classical
Logic. This is the fundamental idea of the proofs-as-programs paradigm.
Cut-elimination for Classical Logic is highly non-deterministic; it is shown
how this can be remedied either by moving to Intuitionistic Logic or to Linear
Logic. In the case on Linear Logic we consider Intuitionistic Linear Logic as
well as Classical Linear Logic. Furthermore, we take a look at the Girard
Translation translating Intuitionistic Logic into Intuitionistic Linear Logic.
Also, we give a brief introduction to some concrete models of Intuitionistic
Linear Logic. No proofs will be given except that a proof of cut-elimination
for the multiplicative fragment of Classical Linear Logic is included in an
appendix.