Technical reports

What is a categorical model of intuitionistic linear logic?

G.M. Bierman

April 1994, 15 pages

DOI: 10.48456/tr-333

Abstract

This paper re-addresses the old problem of providing a categorical model for Intuitionistic Linear Logic (ILL). In particular we compare the new standard model proposed by Seely to the lesser known one proposed by Benton, Bierman, Hyland and de Paiva. Surprisingly we find that Seely’s model is unsound in that it does not preserve equality of proofs — we shall give some examples of equal proofs which do not seem to be modelled as equal morphisms in the category. We shall propose how to adapt Seely’s definition so as to correct these problems and consider how this compares with the model due to Benton et al.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-333,
  author =	 {Bierman, G.M.},
  title = 	 {{What is a categorical model of intuitionistic linear
         	   logic?}},
  year = 	 1994,
  month = 	 apr,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-333.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-333},
  number = 	 {UCAM-CL-TR-333}
}