School of Computer Science, University of Birmingham.
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.