Type Systems for Resource Bounded Programming and Compilation

EPSRC Grant GR/N28436, June 2000 - October 2002

This project draws on ideas of Martin Hofmann, see his papers on the subject area.
Martin co-ordinated the project until May 2001, when he left Edinburgh.
David Aspinall has co-ordinated since then, and is continuing work together with Martin Hofmann, Michal Konečný, 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 LICS'99 paper )
• A Type System for Bounded Space and Functional In-Place Update
  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 web interface.)
• 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:

• Mobile Resource Guarantees