headers
wadler | 5 Jul 1994 20:51
Picon
Picon
Favicon

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
	programming, Addison-Wesley, 1992.]

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
Hajime Ishihara | 8 Jul 1994 16:42
Picon

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 ),
(Continue reading)

Permalink | Reply | 0 comments |
headers
J Roger Hindley | 8 Jul 1994 11:05

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.
Permalink | Reply | 0 comments |
headers
wadler | 5 Jul 1994 21:07
Picon
Picon
Favicon

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)

Permalink | Reply | 0 comments |
headers
Dieter Spreen | 3 Jul 1994 23:33
Picon

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)

Permalink | Reply | 0 comments |
headers
Ruy de Queiroz | 4 Jul 1994 20:50
Picon

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)

Permalink | Reply | 0 comments |
headers
David Rydeheard | 11 Jul 1994 13:44
Picon

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)

Permalink | Reply | 0 comments |
headers
Alexandre Zamulin | 15 Jul 1994 03:53
Picon

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)

Permalink | Reply | 0 comments |
headers
Richard Blute | 14 Jul 1994 20:49
Picon

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
(Continue reading)

Permalink | Reply | 0 comments |
headers
bellin | 20 Jul 1994 23:26
Picon
Favicon

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.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane