Type Systems for Resource Bounded Programming and Compilation
EPSRC Grant GR/N28436, June 2000 - October 2002
This project draws on ideas of
see his papers
on the subject area.
Martin co-ordinated the project until May 2001, when he left Edinburgh.
has co-ordinated since then, and is continuing work together
with Martin Hofmann,
and other collaborators.
Here are links to some of our work:
- The case for support which describes the project in more detail.
- A web interface to three prototype LFPL compilers
LFPL is the heap-bounded functional programming language described in
Martin's papers below.
The latest compiler (by Robert Atkey) supports also two
improved typings described in several papers below.
Linear Types and Non-Size Increasing Polynomial Time Computation
by Martin Hofmann, Theoretical Computer Science, to appear
(expanded journal version of a
A Type System for Bounded Space and Functional In-Place
by Martin Hofmann, Nordic Journal of Computing 7(4):258-289, 2000
The strength of non size-increasing computation
by Martin Hofmann, LICS 2002
Another Type System for In-Place Update
by David Aspinall and Martin Hofmann, ESOP 2002.
(Implementation available through the web interface.)
Typing with Conditions and Guarantees for Functional In-Place Update
by Michal Konečný, to appear in Proceedings of TYPES 2002
Typing with Conditions and Guarantees in LFPL
by Michal Konečný, Technical Report, October 2002, (similar to the above)
Functional In-place Update with Layered Datatype Sharing
by Michal Konečný, to appear in TLCA2003
(Implementation available through the
LFPL with Types for Deep Sharing
by Michal Konečný, Technical Report, November 2002 (extended version of the above)
Static prediction of heap space usage for first-order functional programs
by Martin Hofmann and Steffen Jost, POPL 2003
- Heap Bounded Assembly Language
by David Aspinall and Adriana Compagnoni.,
Journal of Automated Reasoning, 2003, to appear.
Here is a link to a related project:
Last modified: Thu Feb 27 14:35:03 GMT 2003