[Prev][Next][Index][Thread]

paper announcement





*****************************************************************

			Interaction Systems II
                 The Practice of Optimal Reductions


          Andrea Asperti                   Cosimo Laneve

      Department of Mathematics,       INRIA - Sophia Antipolis,
      University of Bologna,           2004, Route des Lucioles,
      Piazza Porta S. Donato 5,        B.P.93 - 06902,
      40127 Bologna, Italy.            Sophia Antipolis, France.
      asperti@cs.unibo.it	       cosimo@garfield.cma.fr


                              Abstract:

Lamping's optimal graph reduction technique for the lambda-calculus 
is generalized to a new class of higher order rewriting systems,
called Interaction Systems. Interaction Systems provide a nice 
integration of the functional paradigm with a rich class of data 
structures (all inductive types), and some basic control flow 
constructs such as conditionals and (primitive or general) recursion.
We describe a uniform and optimal implementation, in Lamping's style,
for all these features.
This work is the natural continuation of our previous paper 
"Interaction systems I, the theory of optimal reductions", where 
we focused on the theoretical aspects of optimal reductions in IS's 
(family relation, labeling, extraction, an so on).

******************************************************************

Comments: 

The paper is related to Linear Logic in two ways:

1. At the syntactical level: Interaction Systems are the intuitionistic
generalization of Lafont's Interaction Nets, which in turn generalize
Proof Nets of Linear Logic. 

2. At the operational level: the optimal reduction technique has been
inspired by Gontheir's and al. systematization of Lamping's work,
based on a tight relation with Linear Logic and the Geometry of
Interaction.

****************************************************************


The paper is available by anonymous FTP from the area 
		ftp.cs.unibo.it
in the directory
		/pub/TR/UBLCS. 
The file, in postscript compressed form, is named 
		93-12.ps.Z 
(technical report 93-12 of the University of Bologna, Laboratory for
Computer Science).