The xSLAM Project
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.
Members of the xSLAM Group
The group consisted mainly of the following people
-
Eike Ritter
Principal Investigator
- 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.
Research Papers
Some of the results of our research have been summarised in the
following papers
-
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.
-
E. Ritter. Characterising Explicit Substitutions which Preserve
Termination. In Proc. of TLCA'99, LNCS 1581. dvi
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. Categorical Models for Explicit Substitutions. Presented at FoSSaCS'99. dvi
ps
- 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.
- Linear Explicit
Substitutions (Extended Abstract). N. Ghani, V. de Paiva,
E. Ritter. Published in proceedings of WESTAPP'98.
Full version
- 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.
Further Work
- 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.
Workshops
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 .
Computer Science Home Page (http://www.cs.bham.ac.uk/)
Page maintained by E.Ritter@cs.bham.ac.uk