5 Jul 20:51 1994

A tale of two translations


There are at least two translations that have been discussed of
intuitionistic logic into intuitionistic linear logic.

(i)   Standard.  This takes A -> B into (!A) -o B.
(ii)  Less standard.  This takes A -> B into !(A -o B).

Regarding the second translation, Girard wrote the following
(to the linear mailing list on 14 Sep 92).

however it might be of interest to try other translations and
to study them in the spirit of denotational semantics. The
translation by means of !(A -o B) is far from preserving the
usual CCC isos, but it has its own virtues. Let us just mention
one : models of lambda-calculus can be indifferently described
as fixpoints of !X -o X or of !(Y -o Y)... the second choice is
in the spirit of lazy lambda-calculi and is reminiscent of the
modelisation by means of strictness/lifting proposed by
Abramsky (i remember a talk, not a paper, sorry).

[The paper he refers to is S. Abramsky, The lazy lambda
calculus, in D. Turner, editor, Research topics in functional

The second translation takes formulae and proofs (equivalently,
types and terms) of intuitionistic logic into those of linear logic.
However, the properties under proof reduction seem less desirable.  The
beta rule is not preserved by the translation.  Furthermore, if we
take the usual (degenerate) semantics of linear logic where !
corresponds to lifting, then the semantics induced by the translation


8 Jul 16:42 1994

NSL'94


[Since it is clearly relevant, I am distributing this conference
announcement to types.  General conference announcements should go to
the Theory-A list: send announcements or requests to subscribe to
THEORY-A@...  -- Philip Wadler, moderator, Types Forum.]

WORKSHOP ON NON-STANDARD LOGICS AND
LOGICAL ASPECTS OF COMPUTER SCIENCE

Kanazawa, Japan, December 5 - 8, 1994

( First announcement )

The WORKSHOP ( NSL'94 ) will be held at Kanazawa City Cultural Hall,
Kanazawa, Japan from December 5th(Mon) to 8th(Thu), 1994.  Kanazawa
is known as one of Japan's foremost castle towns and is a central
city in the Hokuriku region.
This is organized as an activity of the joint project on the study of
non-standard logics between logicians in Japan and Siberia, and is
supported by JAIST ( Japan Advanced Institute of Science and
Technology, Hokuriku ). The workshop will be held also as an annual
meeting of MLG ( Research Group of Mathematical Logic in Japan ).

ORGANIZING COMMITTEE:

L. Maksimova ( Novosibirsk ), H. Ono ( JAIST ) ( co-chair ),


8 Jul 11:05 1994

Krivine's book in Engl.


Details of the English translation of Krivine's types-
book are:

"Lambda-Calculus, Types and Models", by J. L. Krivine,
trans. by Rene Cori,
publ. 1993 by Ellis-Horwood (now amalgamated with Prentice-Hall),
price U.S.$67.95 or U.K.pounds 39.95, ISBN 0-13-062407-1.  5 Jul 21:07 1994 Linear lambda calculi  Following is the list of references I know of that deal with lambda calculi based on linear logic. If you know of updates or additions to the list, I'd be grateful if you pass them on to me. I do not know of a reference that shows that any of these calculi possess the Church-Rosser property. Again, I'd be grateful for enlightenment (or confirmation). Cheers, -- P S. Abramsky, Computational interpretations of linear logic. {\em Theoretical Computer Science\/} 111:3--57, 1993. N. Benton, G. Bierman, V. de Paiva, and M. Hyland, Type assignment for intuitionistic linear logic. Draft paper, August 1992. J. Chirimar, C. A. Gunter, and J. G. Riecke. Linear ML. In {\em Symposium on Lisp and Functional Programming}, ACM Press, San Francisco, June 1992. S. Holmstr\"om, A linear functional language. Draft paper, Chalmers University of Technology, 1988. Y. Lafont, The linear abstract machine. {\em Theoretical Computer Science}, 59:157--180, 1988.  (Continue reading) 3 Jul 23:33 1994 new model for second order lambda calculus and other type theories  This note is to announce a new model construction for the Girard-Reynolds second order lambda calculus. The interpretation of the ForAll-type in this model is different from the usual one. Types are interpreted as inverse limits TT of co-chains T_0 <--p_0-- T_1 <--p_1-- ... of finite topological T_0-spaces such that the mappings p_i are continuous and onto. The morphisms from TT to TT' are sequences (f_i) of maps f_i \in [T_i --> T'_i]. Here [T_0 --> T'_0] is the set of all continuous maps from T_0 into T'_0 and for i > 0, [T_i --> T'_i] is the set of those continuous maps f: T_i --> T'_i such that f~f and [f]~ \in [T_{i-1} --> T'_{i-1}] where f~g iff (forall y, z \in T_i) [if p_i(y) = p_i(z) then p'_i(f(y)) = p'_i(g(z))] and [f]~ is the equivalence class of f under this relation. The space of all morphisms from TT to TT' is thus again an inverse limit of a co-chain of finite T_0-spaces. Moreover, its i-th approximation depends only on the first i+1 approximations of TT and TT', which means that it is rank preserving. For each such constructor F a space \Pi F can be constructed such that its i-th approximation contains i-tuples of elements of the first i+1 approximations of F(TT) for certain spaces TT. Moreover, a mapping Apply is defined such that for t \in \Pi F Apply(t,TT) \in F(TT). This is used to give meaning to the ForAll-type of second order lambda calculus.  (Continue reading) 4 Jul 20:50 1994 WoLLIC '94 - Final Programme [Since it is clearly relevant, I am distributing this conference announcement to types. General conference announcements should go to the Theory-A list: send announcements or requests to subscribe to THEORY-A@... -- Philip Wadler, moderator, Types Forum.] Re: Workshop on Logic, Language, Information and Computation (WoLLIC '94) Recife, July 28-30 1994 (An event part of the IX School of Computing, Recife, July 24-31 1994) Here is the final programme of the Workshop, together with general information and registration form. The Workshop will be part of a bigger event being held in Recife during the last week of July 1994: the (Brazilian) IXth School of Computing, a large biennial event in computer science in the context of Latin America. As some of the invited speakers for the Workshop will be giving advanced seminars (in the form of short courses) on logic and computation in the School, the Workshop will benefit from the fact that the School will attract a fair number of young researchers and students in computer science from all over Latin America. (The School is expected to have an audience of approx. 600 participants.) ******************************************************************************** Workshop on Logic, Language, Information and Computation (WoLLIC '94) Recife, July 28-30 1994 ******************************************************************************** Final Programme *********  (Continue reading) 11 Jul 13:44 1994 Conference: Category Theory and Computer Science (CTCS)  [Since it is clearly relevant, I am distributing this conference announcement to types. General conference announcements should go to the Theory-A list: send announcements or requests to subscribe to THEORY-A@... -- Philip Wadler, moderator, Types Forum.] Preliminary Announcement and Call for Papers ------------------------------------------------------------------------ CATEGORY THEORY AND COMPUTER SCIENCE CTCS-6 7th-11th August 1995 University of Cambridge, UK. ------------------------------------------------------------------------ The sixth of the biennial conferences on Category Theory and Computer Science is to be held in Cambridge in 1995, in conjunction with the third Cambridge Summer Meeting in Category Theory. The purpose of the conference series is the advancement of the foundations of computing using the tools of category theory, algebra, geometry and logic. Whilst the emphasis is upon applications of category theory, it is recognised that the area is highly interdisciplinary and the organising committee welcomes submissions in related areas. Topics central to the conference include: Models of computation Program logics and specification  (Continue reading) 15 Jul 03:53 1994 technical reports (re)  Dear Coleagues, I would like to announce the description of a new database specification language, which is available both electronically and in hard copy and should be of interest to the data type community. Abstract. The database specification language Ruslan is designed for writing specifications of databases of various models and application programs manipulating them. The language is based on the concept of an entity-structured specification, which is a collection of specifications of data types, kinds, type and kind classes, and detached operations and is a special case of a many-sorted algebraic specification. This technique permits the specification of both object-dependent and generic (polymorphic) data types. The language definition is distributed over two documents. The first one (Preprint 28) gives an algebraic background for entity-structured specifications and introduces syntactic constructions of the language. Two sorts of entities are distinguished, data types, and type kinds. A data type is a tool for constructing data units represented in programs by data terms and a kind is a tool for constructing type units represented in programs by type terms. The language of type terms is intermixed with the language of data terms. When a data term is used for constructing a type term, an object-dependent type term is created. Type terms are mapped into type specifications. Depending on the kind of a type term, a concrete, generic, or object-dependent type is specified in this way. Both types and kinds can belong to definite type or kind classes.  (Continue reading) 14 Jul 20:49 1994 Fock Space  The following paper is available by anonymous ftp from triples.math.mcgill.ca, in the directory pub/blute. Anyone without ftp access can of course write to me at the above address. Cheers, Rick Blute Fock Space: A Model of Linear Exponential Types R. Blute P. Panangaden R. Seely ABSTRACT It has been observed by several people that, in certain contexts, the free symmetric algebra construction can provide a model of the linear modality !. This construction arose independently in quantum physics, where it is considered as a canonical construction in quantum field theory. In this context, it is known as (bosonic) Fock space. Fock space is used to analyze such quantum phenomena as the annihilation and creation of particles. There is a strong intuitive connection to the principle of renewable resource, which is the philosophical interpretation of the linear modalities. In this paper, we examine Fock space in several categories of vector spaces. We first consider vector spaces, where the Fock construction induces a model of the$\tensor, \with, !\$ fragment in the category
of symmetric algebras. When considering Banach spaces, the Fock construction
provides a model of a weakening cotriple in the sense of Jacobs.
While the models so obtained have weaker properties, it is closer


20 Jul 23:26 1994

paper announcement


The following paper is available as  LC-pnets.ps  or LC-pnets.dvi
by anonymous ftp from
theory.doc.ic.ac.uk    in the directory    /theory/papers/Bellin

================================================================

Proof-nets for LC, with an appendix on GL.

Gianluigi Bellin
Equipe de Logique, Universite' de Paris VII

Abstract

In the paper [1991] J-Y.Girard proposed the new system LC
for classical logic. Well-known features of LC are:
a new sequent calculus, with a mixed (classical and linear)
consequence relation, a translation into linear logic,
a denotational semantics and a refinement of Goedel's double negation
interpretation into intuitionistic logic. The flow of information
in the process of cut-elimination is controlled by a system of
*polarities* assigned to formulas; strong normalization and confluence
are transferred from LJ to LC in a natural way.

In section 1.5. of Girard [1991] the following open problem was indicated:
to find a system which is to LC what typed Lambda-calculus is to LJ;
... a kind of proof-net'' was indicated as a possible solution.
Given the sequent calculus LC and its interpretation in the sequent calculus
LL for linear logic, it is not too difficult to transfer the formalism of
proof-nets *with additive and exponential boxes* from LL to LC.