EPSRC logo

Details of Grant 

EPSRC Reference: EP/E04350X/1
Title: Reasoning About Exceptions and Interrupts
Principal Investigator: Hutton, Professor G
Other Investigators:
Researcher Co-investigators:
Project Partners:
Department: School of Computer Science
Organisation: University of Nottingham
Scheme: Standard Research
Starts: 01 October 2007 Ends: 30 September 2010 Value (£): 306,915
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
Information Technologies
Related Grants:
Panel History:  
Summary on Grant Application Form
Dealing with unexpected events is an important, and increasingly inevitable, aspect of modern computer programming. As a result, most programming languages provide special features for detecting and managing these events, in the form of so-called exception and interrupt handling primitives. Such primitives are a key feature of modern languages, allowing programs to be written that are robust to various kinds of unexpected events, without having to spoil the structure of the program with a proliferation of tests for special cases. Despite their importance, however, the issue of provable correctness for programs involving exceptions and interrupts has received little attention, but is particularly crucial given the difficulty of writing correct programs in this setting. The aim of this project is to build upon the success of a programme of groundwork that we have conducted in this area, and significantly advance the state-of-the art in formal reasoning about exceptions and interrupts in programming languages.
Key Findings
The project produced a number of fundamental new results, including the first formally justified semantics for interrupts [1], a simple but powerful new approach to program optimisation that unifies a large class of previously unconnected techniques [2,3], a typed-based system for analysing the time complexity of purely functional data structures and algorithms [4], and a new approach to functional parsing that guarantees termination [5]. Three of these articles were published to the top international journal in the field (Journal of Functional Programming), and the remaining two in leading international conferences (Symposium on Principles of Programming Languages and the International Conference on Functional Programming.)

[1] What is the meaning of these constant interruptions? Graham Hutton and Joel Wright. Journal of Functional Programming, 17(6):777-792, Cambridge University Press, November 2007.

[2] The worker/wrapper transformation. Andy Gill and Graham Hutton. Journal of Functional Programming, 19(2):227-251, CambridgeUniversity Press, March 2009.

[3] Factorising folds for faster functions. Graham Hutton, Mauro Jaskelioff, and Andy Gill. Journal of Functional Programming Special Issue on Generic Programming, 20(3&4):353-373, Cambridge University Press, June 2010.

[4] Lightweight semiformal time complexity analsyis for purely functional data structures. Nils Anders Danielsson. ACM SIGPLAN Symposium on Principles of Programming Languages, 2008.

[5] Total parser combinators. Nils Anders Danielsson. ACM SIGPLAN International Conference on Functional Programming, 2010
Potential use in non-academic contexts
No information has been submitted for this grant.
Impacts
No information has been submitted for this grant.
Sectors submitted by the Researcher
Information & Communication Technologies
Project URL:  
Further Information:  
Organisation Website: http://www.nott.ac.uk