School of Computer Science, University of Birmingham

First week and
Course description

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 on a level of abstraction which is high enough to make it possible to reason about the implementation but low enough as to allow an easy coding of the abstract machine. The workshop is aimed at students and researchers with a basic understanding of functional programming and intuitionistic logic who want to work on the exciting field of programming with a solid logical basis.

We focus the workshop along two main themes: explicit substitutions and abstract machines based on Linear Logic. Explicit substitutions are additions to the lambda-calculus which model the dynamics of execution in functional languages: the basic idea is to make the substitutions part of the object-calculus and not simply a meta-theoretical operation. The explicit substitutions meta-theory turned out to be more difficult than expected, and as a result there have been several different calculi of explicit substitutions proposed in the literature. We shall aim to discuss advantages and drawbacks of several of these and link them to the design of abstract machines.

As for the second theme, most of the more recent work on abstract machines is directed towards implementing and proving correct functional languages based on Linear Logic ideas. Linear Logic, being a resource logic, was deemed ideal to model resource control in functional languages. But the implementation of this idea was besetted by problems. First it was not trivial to devise a correct linear lambda-calculus (now we have several of these). Then the obvious first approach of using a correct calculus to implement reference counting (as memory management) was shown to flounder. Our approach, based on integrating explicit substitutions and linearity constraints, turns out to be more complicated than expected, but it works. We shall present our prototype of an abstract machine for linear logic based on these ideas.

Other approaches for the design of abstract machines are based on ideas from the "geometry of interaction" and on games semantics, originally conceived for Linear Logic. Girard's proof nets are the essential tool for this approach. On a slightly orthogonal way, linear logic has also been extensively used to study optimal reductions in the lambda-calculus: the idea is that common instances of redexes should be shared as much as possible to reduce the number of computations steps to a minimum. But there are serious bookkeeping overheads when implementing this strategy. The use of linear logic is supposed to alleviate these overheads and make the implementation of optimal reductions atractive. Asperti constructed an abstract machine called BOHM which follows this approach.

Invited speakers:

  • Andrea Asperti
  • Kristoffer Rose
  • Hugo Herbelin
  • Ian Mackie
  • Jorge Pinto
  • Francisco Alberti
  • Prahlad Sampath


No specific recommendation