[Prev][Next][Index][Thread]
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
.........................................................
@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