[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).