Categorical models of linear logic.

To: linear@cs.stanford.edu
Subject: Categorical models of linear logic.
From: Torben Brauner <tor@daimi.aau.dk>
Date: Wed, 22 Feb 1995 13:03:23 +0100
Approved: types@dcs.gla.ac.uk



A remark to the discussion about categorical models of linear logic:

It has often been said that the embedding of intuitionistic logic into 
linear logic given by the Girard Translation corresponds to the 
coKleisli category induced by a categorical model of linear logic. 
This verbal statement can be given a precise mathematical meaning by 
using the categorical model proposed by Benton, Bierman, de Paiva, and 
Hyland, that is, one can show a categorical generalisation of the 
result that the Girard Translation is sound with respect to the 
coherence space semantics (shown in Girard's TCS 50 paper). The 
categorical generalisation of Girard's soundness result can be found 
in the technical report mentioned below (whose main topic actually is 
recursion in a linear context).

Torben Bra{\"u}ner

BRICS, University of Aarhus

.........................................................

  @techreport{BRICS-RS-95-13,
  author = {T. Bra{\"u}ner},
  title = {The Girard Translation Extended with Recursion},
  institution = {BRICS, Department of Computer Science, University of Aarhus},
  year = {1995},
  number = {RS-95-13},
  note = {Full version of paper to appear in Proceedings of CSL '94, LNCS}}

which will be available by anonymous FTP in a couple of weeks from 

  ftp.daimi.aau.dk

in the directory
        
  pub/BRICS/RS/95/13