Return-Path: <@Sunburn.Stanford.EDU:gtall@ogre.cica.indiana.edu> Date: Wed, 28 Jul 1993 06:59:14 -0500 From: Gerry Allwein To: linear@cs.stanford.edu Subject: Banach Spaces & Linear Logic Sender: lincoln@cs.stanford.edu --text follows this line-- Folks, does anyone know of a paper(s) relating linear logic and banach spaces? Gerry Return-Path: <@Sunburn.Stanford.EDU:RBLUTE@acadvm1.uottawa.ca> Date: Fri, 30 Jul 93 13:00:42 EDT From: Richard Blute Subject: Linear Logic and Banach Spaces To: linear@cs.stanford.edu Sender: lincoln@cs.stanford.edu --text follows this line-- Gerry Allwein asks for a reference on the relation between linear logic and Banach spaces. At this year's MFPS conference, Prakash Panangaden, Robert Seely and I presented a paper entitled "Holomorphic Models of Exponential Types in Linear Logic". In this paper, we build a model of the tensor-! fragment in the category of commutative Banach algebras. Hopefully, we will be announcing the completed paper soon. One of the main distinctions between Banach spaces (and Hilbert spaces) is that the existence of a norm allows one to discuss convergent sequences, power series (hence holomorphic functions), etc. The specific construction we use to model ! is called Fock space. Fock space was introduced in quantum field theory as a framework for modelling the annihilation and creation of particles. There is a pleasing analogy here between such ideas and that of infinitely renewable resource. Finally, the Fock space associated to a Banach space or Hilbert space has a concrete representaton as a space of holomorphic functions, suitably defined.Thus, the Kleisli category can reasonably be thought of as a category of generalized holomorphic functions. Rick Blute Return-Path: <@Sunburn.Stanford.EDU:RBLUTE@acadvm1.uottawa.ca> Date: Fri, 30 Jul 93 18:16:33 EDT From: Richard Blute Subject: Linear Logic and Banach Spaces II To: linear@cs.stanford.edu Sender: lincoln@cs.stanford.edu --text follows this line-- Half of a sentence of my last note somehow vanished so please let me clarify one issue. The point of the second paragraph is that Banach spaces and Hilbert spaces have a notion of norm, whereas ordinary vector spaces do not. Thus, the notions of convergent sequence, power series, etc. make sense in either a Banach Space or Hilbert space. Rick Blute Return-Path: Date: Wed, 4 Aug 93 10:23:28 EDT From: andre@saul.cis.upenn.edu (Andre Scedrov) Posted-Date: Wed, 4 Aug 93 10:23:28 EDT To: linear@cs.stanford.edu Subject: Brief Guide to LL Sender: lincoln@cs.stanford.edu --text follows this line-- A BRIEF GUIDE TO LINEAR LOGIC Andre Scedrov In: "Current Trends in Theoretical Computer Science", ed. by G. Rozenberg and A. Salomaa, World Scientific Publishing Co., 1993. ABSTRACT. An overview of linear logic is given, including an extensive bibliography and a simple example of the close relationship between linear logic and computation. This is an expanded and updated version of the article that has originally appeared in Bull. EATCS vol. 41, June, 1990, pp. 154-165, in the column "Logic in Computer Science" edited by Y. Gurevich. Return-Path: <@Sunburn.Stanford.EDU:gtall@ogre.cica.indiana.edu> Date: Wed, 25 Aug 1993 08:50:40 -0500 From: Gerry Allwein To: linear@cs.stanford.edu Subject: Duality for Bounded Lattices Sender: lincoln@cs.stanford.edu --text follows this line-- Folks, there is a paper available via ftp to cs.indiana.edu in the pub/logic directory called duality.ps (.dvi). The abstract follows below. Lattices are in used in the algebraic semantics of linear logics. The duality was extended to the full Kripke models in my thesis and a paper on that should also appear shortly...real soon...really... Gerry Duality for Bounded Lattices Gerard T. Allwein Chrysafis Hartonas Visual Inference Laboratory Dept of Math and Philosophy Indiana University Indiana University We present a duality theorem for bounded lattices that improves and strengthens Urquhart's topological representation for lattices. Rather than using maximal, disjoint filter-ideal pairs, as Urquhart does, we use all disjoint filter-ideal pairs. This allows not only for establishing a bijective correspondance between lattices and a certain kind of doubly ordered Stone Spaces (Urquhart), but for a full duality result. We provide, in the sequel, a treatment of congruences and epimorphisms, as well as of sublattices, proving relevant duality theorems. The paper is concluded with a sectional representation of lattices, imbedding a general lattice in a sheaf space of lattices. Return-Path: <@Sunburn.Stanford.EDU:sa@doc.ic.ac.uk> Date: Wed, 8 Sep 1993 19:51:24 +0100 (BST) From: Samson Abramsky Mime-Version: 1.0 Content-Type: text/plain; charset=US-ASCII To: linear@cs.stanford.edu Subject: Games and Full Abstraction for PCF: second announcement Sender: lincoln@cs.stanford.edu --text follows this line-- A document is now available by anonymous ftp from theory.doc.ic.ac.uk in papers/Abramsky/gfapcf2.{dvi,ps}. The gist is conveyed by the final sentence: ``In the light of the preliminary discussion, we feel that these results provide a clear-cut solution to the Full Abstraction Problem for PCF.'' Return-Path: <@Sunburn.Stanford.EDU:asperti@cs.unibo.it> Date: Fri, 10 Sep 1993 10:57:46 +0200 From: asperti@cs.unibo.it (Andrea Asperti) To: linear@cs.stanford.edu Subject: paper announcement Sender: lincoln@cs.stanford.edu --text follows this line-- The following paper is available by anonymous ftp at ftp.dm.unibo.it (Dipartimento di Matematica of the University of Bologna, Italy). The paper, in compressed postscript form, is in the directory pub/asperti, and it is called acta.ps.Z. It is going to appear in a special issue of ACTA INFORMATICAE, devoted to Categories in Computer Science. In you like to play with an optimal (?!) compiler of lambda terms, in the same directory you will find a prototype, very preliminary (but running) version, in the file opt_impl.tar.Z (compressed, tar form). Cheers. -- andrea ______________________________________________________________________ Andrea Asperti Dipartimento di Matematica, Universit\'a di Bologna, P.za di Porta S.Donato, 40126 Bologna, ITALY. asperti@cs.unibo.it ABSTRACT The paper discusses, in a categorical perspective, some recent works on optimal graph reduction techniques for the lambda-calculus. In particular, we relate the two "brackets" of Gonthier-Abadi-Levy (POPL 92, LICS 92) to the two operations associated with the comonad "!" of Linear Logic. The rewriting rules can be then understood as a "local implementation" of naturality laws, that is as the broadcasting of some information from the output to the inputs of a term, following its connected structure. Return-Path: <@Sunburn.Stanford.EDU:asperti@cs.unibo.it> Date: Thu, 16 Sep 1993 19:02:08 +0200 From: asperti@cs.unibo.it (Andrea Asperti) To: linear@cs.stanford.edu Subject: errata corrige Sender: lincoln@cs.stanford.edu --text follows this line-- In my last message about a paper available by ftp, I made a mistake about the name of the journal which is going to publish it. It is not "Acta informatica" but "FUNDAMENTA INFORMATICAE". I am really sorry. I also forgot to give the title of the paper. Here it is: Linear Logic, Comonads, and Optimal Reductions. Cheers. -- andrea Return-Path: <@Sunburn.Stanford.EDU,@sophia.inria.fr:retore@espace.cma.fr> Date: Wed, 6 Oct 93 11:17:05 +0100 From: Christian Retore To: linear@cs.stanford.edu Subject: non-commutative tensor Sender: lincoln@cs.stanford.edu --text follows this line-- During the summer there was a discussion on calculi involving both commutative and non-commutative connectives. I mentionned the work I did on this topic, but there was nothing available by ftp. I partly fixed this trouble by putting the english introduction of my thesis called: intro.dvi on the ftp site: cma.cma.fr under the directory pub/papers/retore The paper on this ordered calculus will soon be available on the same ftp directory, with the name pomset.dvi Return-Path: <@Sunburn.Stanford.EDU:pavlovic@triples.math.mcgill.ca> From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic) Subject: Chu is cofree To: linear@cs.stanford.edu Date: Wed, 13 Oct 93 12:47:26 EDT X-Mailer: ELM [version 2.3 PL11] Sender: lincoln@cs.stanford.edu --text follows this line-- 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.