2 Dec 1992 13:00

### local and asynchronous beta-reduction

We build a confluent, local, asynchronous reduction on lambda-terms, using
infinite objects (partial one-to-one transformations in Girard's algebra
Lambda*), which is simple (only one move), intelligible (semantic setting of
the reduction), general (based on a large-scale decomposition of beta
reduction), and may be mechanized.

A paper virtred.dvi.Z describing this construction is
ftp-able at frege.logique.jussieu.fr in /pub/scratch/

Vincent Danos & Laurent Regnier.


4 Dec 1992 15:37

[This message is an answer by Jean-Yves Girard to questions posed by
Carolyn Brown in an earlier message.  As a reminder, the message from
Brown appears first.  -- Phil Wadler, moderator, Types Forum]

-----------------------------------------------------------------------------

>Date: Fri, 30 Oct 92 16:13:15 +0100
>From: Carolyn Brown <cbrown@...>
>Subject: question about rules for !

I have a simple question about the two common presentations of the
rules for !. I've discussed this with several linear-logicians, without
reaching a conclusion.

Two presentations commonly used (for single-conclusion calculi) are

(I)  !Gamma |- A        Gamma, !A, !A |- B      Gamma, A |- B      Gamma |- B
-----------        ------------------      --------------     ------------
!Gamma |- !A       Gamma, !A  |- B         Gamma, !A |- B    Gamma, !A |-B

and

(II) The last three rules above with the first rule replaced by:

B |- I    B |- A    B |- B \otimes B   (where I is the unit of \otimes)
------------------------------------
B |- !A

System (II)  is the categorical combinator version of the rules, characterising
!A as a greatest fixed point (coinductive type).


8 Dec 1992 04:33

### Generating plans im linear logic


The increasing interest for applications of linear logic
motivates the present announcement of our own works on
"Planification  and Linear Logic".
These works - performed before the beginning of the current
mailing list - have been largely diffused (in Europ and in the
world) since 1990, especially at the German Congress on Artificial
Intelligence (GWAI'91), workshop Logic and Change.

Up to 1989, several attempts in the relation between logic
and the changes involved in reasoning and specifically in
plan generation, have been made, either by embedding actions
into a classical framework or by using non-standard formalisms.
We have thought that these attempts, though promising, missed
their objectives, for a want of a suitable logic.
We have shown how to obtain a strong and clean correspondence
between proofs and sequences of actions only by using linear
logic. A theorem is presented which expresses the new adequacy
between proofs and actions.
After the proof theoretical study, M. Masseron has proposed
a new characterization of actions, in the spirit of proof-nets
in the conjunctive case. The work on the disjunctive case
has also be treated : a preliminary version has been diffused
since 1991 ; an achieved version will be presented at the
ESPRIT workshop "Logic and Change" at Lisboa (january 1993).

M. Masseron, C. Tollu, J. Vauzeilles

References
1. Masseron M. Tollu C. Vauzeilles J. : "Plan Generation and Linear LogicJ".


10 Dec 1992 15:11

### Introduction to Bellin-Scott paper


At the suggestion of the authors, I have written a short introductory
note to On the pi-calculus and Linear Logic'' by Gianluigi Bellin and
Phil Scott. This is now available by anonymous-ftp from
theory.doc.ic.ac.uk, in papers/Abramsky/picalcintro.dvi.

Samson Abramsky


10 Dec 1992 17:03

### New Foundations for the Geometry of Interaction (full version)


The full version of New Foundations for the Geometry of Interaction''
theory.doc.ic.ac.uk in compressed form as
papers/Abramsky/nfgi.{dvi,ps}.Z.
(An extended abstract was published in the Proceedings of LICS 92).

Samson Abramsky


11 Dec 1992 15:17

### Program of TLCA'93


Summary: The final program of TLCA93 and some general
information on how to participate.

-----------------------------------------------------------------------

International Conference on Typed Lambda Calculi and Applications

TLCA

TLCA, the international conference on Typed Lambda Calculi and Applications
will be held March 16-18, 1993 in Utrecht The Netherlands.
The conference location will be:

Koninklijke Jaarbeurs
Jaarbeursplein
Utrecht

The conference aims at providing a forum for the presentation and discus-
sion of recent research in the following areas:

* Proof theory of type systems
* Logic and type systems
* Typed lambda calculi as models of (higher order) computation
* Semantics of type systems
* Proof verification via type systems
* Type systems of programming languages
* Typed term rewriting systems



15 Dec 1992 19:03

### Typing and Subtyping for the Mobile Processes


The following paper is now available for anonymous FTP.  Retrieval

Cheers,

Benjamin Pierce
Davide Sangiorgi

----------------------------------------------------------------------

TYPING AND SUBTYPING FOR MOBILE PROCESSES
Benjamin Pierce and Davide Sangiorgi

The pi-calculus is a process algebra that supports process mobility by
focusing on the communication of channels.

Milner's presentation of the pi-calculus includes a type system
assigning arities to channels and enforcing a corresponding discipline
in their use.  We extend Milner's language of types by distinguishing
between the ability to read from a channel, the ability to write to a
channel, and the ability both to read and to write.  This refinement
gives rise to a natural subtype relation similar to those studied in
typed lambda-calculi.

The greater precision of our type discipline yields stronger versions
of some standard theorems about the pi-calculus.  These can be used,
for example, to obtain the validity of beta-reduction for the more
efficient of Milner's encodings of the call-by-value lambda-calculus,
for which beta-reduction does not hold in the ordinary pi-calculus.


17 Dec 1992 00:49

### two preliminary papers by anon ftp


Preliminary versions of two papers are available by anonymous ftp.
The titles and abstracts are given below. The files are

ftp/pub/jcm/objects-paper.dvi
ftp/pub/jcm/weak-poly.dvi

on theory.stanford.edu. Any comments, criticism, or corrections to
these papers will be appreciated.

John Mitchell

-----------------------------------------------------------------------------------

A lambda calculus of objects and method specialization

John C. Mitchell           Furio Honsell               Kathleen Fisher
Computer Science Dept.  Dipartimento di Informatica   Computer Science Dept.
Stanford University        Universit\'{a} di Udine      Stanford University
jcm@...       honsell <at> uduniv.cineca.it    kfisher <at> cs.stanford.edu

Abstract

This paper presents an untyped lambda calculus, extended with
object primitives that reflect the capabilities of so-called
delegation-based object-oriented languages.
A type inference system allows static detection of errors,
preventing {\it message not understood,}
while at the same time allowing the type of an inherited
method to be specialized to the type of the inheriting object.


17 Dec 1992 20:45

### OOL design and semantics papers


The following papers on the design, type-checking, and semantics of a
functional, statically-typed, object-oriented language, TOOPLE, are now
available for anonymous ftp:

1. Safe Type Checking in a Statically-Typed Object-Oriented Programming Language
by Kim B. Bruce.  To Appear in Proc ACM Symp. Principles of Programming
Languages, 1993.

2. An operational semantics for TOOPLE:  A statically-typed object-oriented
programming language, by Kim B. Bruce, Jonathan Crabtree, and Gerald Kanapathy.

3. Type checking in TOOPLE is decidable, by Kim B. Bruce, Jon Crabtree,
Allyn Dimock, Robert Muller, Thomas P. Murtagh, Robert van Gent.

They may be obtained by anonymous ftp from bull.cs.williams.edu, (for those
whose name servers have difficulty finding the machine, its numeric

the proper directory, type:
cd pub/kim
get TCPOPL.dvi
get TPLNatSem.dvi
get TpCkAlgo.dvi

The second and third papers are preliminary versions for conference submission,
so I would be grateful for any comments or suggestions for clarification on
them.  Full versions will be available later.


22 Dec 1992 21:17

### clarification of recently-posted abstract


Standard ML weak polymorphism and imperative constructs

My Hoang   John Mitchell  Ramesh Viswanathan
Department of Computer Science
Stanford University, Stanford, CA 94305
{hoang, mitchell, vramesh} <at> cs.stanford.edu

The recently-posted abstract may be somewhat misleading regarding the
difference between Standard ML, as specified in the formal definition,
and Standard ML of New Jersey, a popular implementation of the language.
The typing of imperative constructs in Standard ML is fully specified in
the formal definition [1], and proved correct in [2,3]. It is the SML-NJ
implementation, which differs from the formal definition, that uses weak
type variables and has not been analyzed previously. The main differences
between the two approaches are explained in the paper.

Sorry for any confusion on this point.

John Mitchell

[1]      <at> book{MTH90,
author = "Robin Milner and Mads Tofte and Robert Harper",
title = "The Definition of {Standard ML}",
publisher = "MIT Press",
year =  "1990"
}

[2]      <at> PhdThesis{tofte,
`