headers
danos | 2 Dec 1992 13:00
Picon
Favicon

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.
Permalink | Reply | 0 comments |
headers
Jean-Yves Girard | 4 Dec 1992 15:37
Picon
Picon
Favicon

Answer to Carolyn

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

Permalink | Reply | 0 comments |
headers
Jacqueline Vauzeille | 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".
(Continue reading)

Permalink | Reply | 0 comments |
headers
Samson Abramsky | 10 Dec 1992 15:11
Picon

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
Permalink | Reply | 0 comments |
headers
Samson Abramsky | 10 Dec 1992 17:03
Picon

New Foundations for the Geometry of Interaction (full version)


The full version of ``New Foundations for the Geometry of Interaction''
by myself and Radha Jagadeesan is now available by anonymous-ftp from
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
Permalink | Reply | 0 comments |
headers
Jan Friso Groote | 11 Dec 1992 15:17
Picon

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

Permalink | Reply | 0 comments |
headers
pierce | 15 Dec 1992 19:03
Picon
Picon

Typing and Subtyping for the Mobile Processes


The following paper is now available for anonymous FTP.  Retrieval
instructions follow the abstract.

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

Permalink | Reply | 0 comments |
headers
John "C." Mitchell | 17 Dec 1992 00:49
Picon

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

Permalink | Reply | 0 comments |
headers
Kim Bruce | 17 Dec 1992 20:45
Picon

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
address is 137.165.5.2).

Login as anonymous and type your id as password when requested.  To get to 
the proper directory, type:
	cd pub/kim
To receive the papers, type
	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.
(Continue reading)

Permalink | Reply | 0 comments |
headers
John "C." Mitchell | 22 Dec 1992 21:17
Picon

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,
        author = "Mads Tofte",
(Continue reading)

Permalink | Reply | 0 comments |

Gmane