Reasoning About Exceptions and Interrupts

Lead Research Organisation: University of Nottingham
Department Name: School of Computer Science

Abstract

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.

Publications

10 25 50
publication icon
Danielsson N (2010) Total parser combinators in ACM SIGPLAN Notices

publication icon
Danielsson N (2012) Operational semantics using the partiality monad in ACM SIGPLAN Notices

publication icon
GILL A (2009) The worker/wrapper transformation in Journal of Functional Programming

publication icon
HUTTON G (2007) What is the meaning of these constant interruptions? in Journal of Functional Programming

publication icon
HUTTON G (2010) Factorising folds for faster functions in Journal of Functional Programming

publication icon
Nils Anders Danielsson (2008) Lightweight Semiformal Time Complexity Analysis for Purely Functional Data Structures

 
Description 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
Exploitation Route The ideas from papers [2,3] above are now being integrated into the Glasgow Haskell Compiler by a team at the University of Kansas.
Sectors Digital/Communication/Information Technologies (including Software)
 
Description The ideas from papers [2,3] above are now being integrated into the Glasgow Haskell Compiler by a team at the University of Kansas.
First Year Of Impact 2010
Sector Digital/Communication/Information Technologies (including Software)
Impact Types Societal,Economic