ESSLLI'98 Workshop on Logical Abstract Machines

ESSLLI'98 Workshop on Logical Abstract Machines
Supported by the EU-Working Group "Applications of Semantics"

Organisers: Eike Ritter and Valeria de Paiva

School of Computer Science, University of Birmingham.

The aim of this workshop was to bring together recent work on the design of abstract machines for functional programming languages, based on logical foundations.
The following speakers made papers available.
  • Francisco Alberti and Eike Ritter. An efficient linear abstract machine with single-pointer property.
  • Neil Ghani, Valeria de Paiva and Eike Ritter. Categorical Models of Explicit Substitutions.
  • Neil Ghani, Valeria de Paiva and Eike Ritter. Linear Explicit Substitutions.
  • Hugo Herbelin. Using Types to Control Reduction in System F.
  • Ian Mackie and Jorge Pinto. Compiling the Lambda Calculus into Interaction Combinators.
  • Prahladavaradan Sampath. On Abstract Machines and Games.

  • The abstract of the following talks is also available.
  • Andrea Asperti. The optimal implementation of functional programming languages.
  • Kristoffer Rose. Explicit Substitution, Abstract Machines, and Memory.

  • Aim of the Workshop

    Abstract machines describe implementations of functional languages at a level of abstraction high enough to make it possible to reason mathematically about the implementation, but low enough to allow a direct coding of it. We call the machines we work with `logical' since we use the extended Curry-Howard Correspondence to link the type theory of the functional language to various kinds of logic. The categorical semantics of the type theory is also used as a guide for devising the `correct' reduction rules or transformations of the machines.

    Much recent work on abstract machines has been based around ideas from Linear Logic which, being a resource-sensitive logic, is well suited to modelling resource control in functional languages. We tried to represent as many strands of work along these lines as we could in the workshop.

    First, there is the adaptation to a linear setting of the traditional approach to abstract machines for functional languages. This traditional approach is not easy, but it is more feasible if based on integrating explicit substitutions and linearity constraints. These form the basis of the xSLAM -- The eXplicit Substitutions Linear Abstract Machine project, being developed by the organisers of the worskshop.

    Second, there are less traditional approaches to the design of linear abstract machines, based on proof nets and on game semantics. The key point ofxhos the approach based on proof nets is that reduction strategies in the lambda-calculus can be seen as following certain paths in the proof net. Because the paths make it explicit where sharing occurs in a computation, linear logic has also been applied to study optimal reductions in the lambda-calculus. The approach to abstract machines using game semantics is based on the idea that the sequence of moves in the game corresponds to execution of abstract machines. Because many game models for the simply-typed lambda-calculus work via linear logic as an intermediate language, the resulting abstract machines are related to the ones obtained from linear logic.

    We had talks from the all the strands of work mentioned above. Since the workshop itself was very informal, these are again very informal proceedings. We asked all participants to provide some written record of their contribution, but some chose not to do so. Kris Rose started the workshop explaining the basics of the traditional approach and clarified many of the differences between machines in the literature. His slides are part of the proceedings, but not available electronically. Andrea Asperti described optimal reductions and its problems, as well as his proposed solutions. Eike Ritter presented the xSLAM solution, that is traditional, but heavily based on the use of the categorical semantics as a guide for designing the syntax of the calculus. Pralahd Sampath presented his personal view of game semantics, that is a synthesis of previous work by Abramsky, Ong and Hyland, McCusker, etc. Jorge Pinto presented his work with Ian Mackie on interactions nets and Francisco Alberti presented his suggestions for a more relevant calculus, following the lines of xSLAM. Hugo Harbelin spoke about a machine for system F, based on game semantics. Keith Wansbrough talked about a related problem: how to infer a number of uses for a program expression in Haskell.

    We would like to thanks all our participants for a very enjoyable meeting and we hope to have another sucessful workshop on Logical Abstract Machines in 1999.