Workshop on Logical Abstract Machines

(WoLAM'99)

14-16 July 1999, Birmingham, UK

Supported by the EU Working Group "Applications of Semantics"
and the British Logic Colloquium and the School of Computer Science, University of Birmingham

This workshop brings together recent work on the design of abstract machines for functional programming languages, based on logical foundations.

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 relatively direct coding of the abstract machine. 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.

One of the main goals of the workshop is to improve understanding of the connections between the novel abstract machines based on game semantics (or the geometry of interaction) and their more traditional counterparts. A second goal of the workshop is to explore how a semantically-based view of explicit substitutions can lead to good implementation techniques.

The programme comprised the following talks, here listed alphabetically by author.

Nick Benton, Microsoft Research, Cambridge.
Monads, Effects and Transformations. Abstract.

Viviana Bono, University of Birmingham.
Subtyping Relations as Sequents. Abstract.

Valeria de Paiva, University of Birmingham, visiting Xerox Parc.
xSLAM project: the story so far. Slides

Neil Ghani, University of Leicester.
Categorical Models of Explicit Substitutions. Paper.

Stefano Guerrini , Queen Mary and Westfield College, London.
An Overview of lambda-calculus Sharing Graph Reduction. Chapter.

Maria Emilia Maietti, University of Birmingham.
Linear Recursion. Abstract.

Laurent Regnier, University of Marseille.
From Girard's Geometry of Interaction to Krivine's Abstract Machine. Abstract.

Kristoffer Rose, Ecole Normale Superieure, Lyon.
TWUB or Why Using Variables is More Efficient than First-Order Codings

Eike Ritter Abstract Machines with the Single Pointer Property. Slides.

Harold Simmons, University of Manchester.
Some thoughts on the `space' of all proofs. Slides.

Wolam'98 took place as part of ESSLLI'1998 in Saarbruecken, Germany. Abstracts of the talks and more detailed information can be found here .