VALERIA DE PAIVA and EIKE RITTER 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 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:
Computation
LOGICAL ABSTRACT MACHINES
Workshop
First week
vdp@cs.bham.ac.uk and exr@cs.bham.ac.u
Course description
Prerequisites
None
Literature
No specific recommendation