Details of Grant 

EPSRC Reference:	GR/S41937/01
Title:	Bunched ML
Principal Investigator:	O'Neill, Professor E
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	University of Bath
Scheme:	Standard Research (Pre-FEC)
Starts:	01 November 2003	Ends:	31 October 2006	Value (£):	152,451
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:	GR/S41845/01
Panel History:
Summary on Grant Application Form
Types in programming languages are intimately related to logics. Recent advances in program logic allow us to specify and verify, with comparative ease, the manipulation of resources in a program heap. These advances use the bunched logic of O'Hearn and Pym as a language for writing assertions about storage; the present project aims to use a type system based on bunched logic in a programming language. We propose to develop a language, based on a fragment of ML, in which the type structure allows the programmer to describe, and the compiler to verify, resource management between program components. The project has both practical and theoretical aspects, and the expected outcomes include not only the language and its compiler, but also an increased understanding of logical and automated reasoning about resource management in programs.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.bath.ac.uk