Categorical models of linear logic.

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


  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 


in the directory