Source: http://www.cs.bham.ac.uk/research/projects/xslam/xslam.html
Timestamp: 2019-04-20 06:19:22+00:00

Document:
The advantages of functional programming are well-known: programs are easier to write, understand and verify than their imperative counterparts. However, functional languages tend to be more memory intensive and these problems have hindered their wider use in industry. The xSLAM project is addressing these issues by using recent developments in linear logic and explicit substitutions to construct and implement more efficient abstract machines. These theoretical foundations both aid the design of the machines and ensure their correctness.
The project grew out of Dr Ritter's previous work on categorical abstract machines for higher order typed lambda-calculi and Dr de Paiva's work on typed lambda-calculi for linear logic. This project was funded by an EPSRC grant (number GR/L28296), from 1.1.1997 - 31.3.2000. Some further work on this research has been done (see below) and some further work is expected.
A summary of the achievements is available.
Valeria de Paiva Principal Investigator, now at PARC (Palo Alto Research Center), CA, USA.
Neil Ghani Research Fellow on the grant, now a Lecturer in Leicester.
Maria Emilia Maietti Research Fellow on the grant, now a Research Associate in Padova, Italy.
Paola Maneggia PhD. Student, thesis submitted February 2004, under Achim Jung's supervision.
Alex Tucker PhD. Student until 1998, now pursuing a commercial career.
Francisco Alberti MSc thesis student in 1997, moved on to ENS (Paris) to study for a Ph.D.
E. Ritter. A calculus for Resource allocation.Technical Report, University of Birmingham, October 2000.
M.E. Maietti, V. de Paiva and E. Ritter. Linear primitive recursion. Technical Report, University of Padova, June 2000.
M.E. Maietti, V. de Paiva and E. Ritter. Categorical Models for Intuitionistic and Linear Type Theory. In Proc. of FoSSaCS'00. In Lecture Notes of Computer Science. dvi. ps.
I. Cervesato, V. de Paiva and E. Ritter. Explicit Substitutions for Linear Logical Frameworks. In Proc. of the Workshop on Logical Frameworks and Meta-Languages (LFM'99). ps.
Explicit Substitutions for Constructive Necessity. N. Ghani, V. de Paiva, E. Ritter. Published in the Proceedings of ICALP'98.
N. Ghani, V. de Paiva and E. Ritter. Linear Explicit Substitutions. Journal of the IGPL, Vol. 8, No. 1.
An Abstract Machine based on Linear Logic and Explicit Substitutions. Francisco Alberti. MSc in Advanced Computer Science, University of Birmingham 1997.
On Explicit Substitutions and Names. V. de Paiva, E. Ritter. To appear in Proceedings of ICALP'97. Also published as Technical Report CSR-97-5 , School of Computer Science, University of Birmingham. March 1997.
Categorical Abstract Machines for Higher Order Typed Lambda-Calculi. E. Ritter. In Theoretical Computer Science Volume 136, number 1, pages 125 - 162, 1994.
Rewriting Properties of Combinators for Intuitionistic Linear Logic. M. Nesi, V. de Paiva, E. Ritter. Proceedings of the Workshop on Higher Order Algebra, Logic and Term Rewriting, HOA'93. In Volume 816 of Lecture Notes in Computer Science, Springer Verlag. 1994.
Relating Categorical Semantics for Intuitionistic Linear Logic P. Maneggia, M. Maietti, Valeria de Paiva and E. Ritter, Presented at Natural Deduction 2001, Rio de Janeiro. Journal paper submitted.
Normalization Bounds in Rudimentary Linear Logic M. Maietti, Valeria de Paiva and E. Ritter, presented at the Workshop on Implicit Computational Complexity, FLoC'02, Copenhagen, 2002. Also technical report of the University of Padova, Italy, 2002.
Variations on Linear PCF Valeria de Paiva and Eike Ritter, Proc. WESTAPP-99, 1999.
We organised a workshop on Logical Abstract machines as part of the 10th European Summer School on Logic, Language and Information (ESSLLI) in Saarbruecken, 1998 . More information can be found here. We also organized a second workshop on Logical Abstract Machines in Birmingham, 1999. Details can be found here .

References: V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V.