Subject: Banach Spaces & Linear Logic
From: Gerry Allwein <[email-masked]>
To: [email-masked]
Date: Wed, 28 Jul 1993 06:59:14 -0500

--text follows this line--

Folks, does anyone know of a paper(s) relating linear logic and banach spaces?

Gerry

Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date:         Fri, 30 Jul 93 13:00:42 EDT
From: Richard Blute <[email-masked]>
Subject:      Linear Logic and Banach Spaces
To: [email-masked]
Sender: [email-masked]
--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:[email-masked]>
Date:         Fri, 30 Jul 93 18:16:33 EDT
From: Richard Blute <[email-masked]>
Subject:      Linear Logic and Banach Spaces II
To: [email-masked]
Sender: [email-masked]
--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: <[email-masked]>
Date: Wed, 4 Aug 93 10:23:28 EDT
From: [email-masked] (Andre Scedrov)
Posted-Date: Wed, 4 Aug 93 10:23:28 EDT
To: [email-masked]
Subject: Brief Guide to LL 
Sender: [email-masked]
--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:[email-masked]>
Date: Wed, 25 Aug 1993 08:50:40 -0500
From: Gerry Allwein <[email-masked]>
To: [email-masked]
Subject: Duality for Bounded Lattices
Sender: [email-masked]
--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.

Date: Wed,  8 Sep 1993 19:51:24 +0100 (BST)
From: Samson Abramsky <[email-masked]>
To: [email-masked]
Subject: Games and Full Abstraction for PCF: second announcement
Sender: [email-masked]
--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:[email-masked]>
Date: Fri, 10 Sep 1993 10:57:46 +0200
From: [email-masked] (Andrea Asperti)
To: [email-masked]
Subject: paper announcement
Sender: [email-masked]
--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.
		      [email-masked]

			   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:[email-masked]>
Date: Thu, 16 Sep 1993 19:02:08 +0200
From: [email-masked] (Andrea Asperti)
To: [email-masked]
Subject: errata corrige
Sender: [email-masked]
--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:[email-masked]>
Date: Wed, 6 Oct 93 11:17:05 +0100
From: Christian Retore <[email-masked]>
To: [email-masked]
Subject: non-commutative tensor
Sender: [email-masked]
--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:[email-masked]>
From: [email-masked] (Dusko Pavlovic)
Subject: Chu is cofree
To: [email-masked]
Date: Wed, 13 Oct 93 12:47:26 EDT
X-Mailer: ELM [version 2.3 PL11]
Sender: [email-masked]
--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.