Technical reports

On intuitionistic linear logic

G.M. Bierman

August 1994, 191 pages

This technical report is based on a dissertation submitted December 1993 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Wolfson College.

DOI: 10.48456/tr-346

Abstract

In this thesis we carry out a detailed study of the (propositional) intuitionistic fragment of Girard’s linear logic (ILL). Firstly we give sequent calculus, natural deduction and axiomatic formulations of ILL. In particular our natural deduction is different from others and has important properties, such as closure under substitution, which others lack. We also study the process of reduction in all three local formulations, including a detailed proof of cut elimination. Finally, we consider translations between Instuitionistic Logic (IL) and ILL.

We then consider the linear term calculus, which arises from applying the Curry-Howard correspondence to the natural deduction formulation. We show how the various proof theoretic formulations suggest reductions at the level of terms. The properties of strong normalization and confluence are proved for these reduction rules. We also consider mappings between the extended λ-calculus and the linear term calculus.

Next we consider a categorical model for ILL. We show how by considering the linear term calculus as an equational logic, we can derive a model: a linear category. We consider two alternative models: firstly, one due to Seely and then one due to Lafont. Surprisingly, we find that Seely’s model is not sound, in that equal terms are not modelled with equal morphisms. We show how after adapting Seely’s model (by viewing it in a more abstract setting) it becomes a particular instance of a linear category. We show how Lafont’s model can also be seen as another particular instance of a linear category. Finally we consider various categories of coalgebras, whose construction can be seen as a categorical equivalent of the translation of IL into ILL.

Full text

PDF (12.6 MB)

BibTeX record

@TechReport{UCAM-CL-TR-346,
  author =	 {Bierman, G.M.},
  title = 	 {{On intuitionistic linear logic}},
  year = 	 1994,
  month = 	 aug,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-346.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-346},
  number = 	 {UCAM-CL-TR-346}
}