[Prev][Next][Index][Thread]
Chu is cofree
A paper on
THE CHU CONSTRUCTION AND
COFREE MODELS OF CLASSICAL LINEAR LOGIC
by Dusko Pavlovic
is available by anonymous FTP from triples.math.mcgill.ca. The files
chu-{A4,US}.{dvi,ps}.Z are the directory pub/pavlovic. Each of them
contains the whole paper, but in various formats.
Abstract
We describe a couniversal property of the Chu construction. It induces
a comonad on a category of autonomous categories. *-Autonomous
categories are exactly the coalgebras for this comonad. The models of
full classical linear logic (with the exponentials) are then obtained
as the coalgebras on the models of intuitionistic linear logic ---
this time for a comonad derived from the Chu construction. In view of
the computational interpretations of linear logic, these results
suggest an interesting connection of the functional and the concurrent
programming. For this reason, some effort has been spent to make all
the constructions effective.