Chu is cofree

• To: linear@cs.stanford.edu
• Subject: Chu is cofree
• From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic)
• Date: Wed, 13 Oct 93 12:47:26 EDT
• Approved: types@dcs.gla.ac.uk

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.

• Prev: proof terms for classical logic in natural deduction formulation
• Next: erratum: Undecidabilty of System F
• Index(es):
  • Main
  • Thread