Research
We list active/up-coming projects in rough chronological order, with some indication of their funding status.
Formalising the Interface between Software and Hardware (FISH)
Andrew Butterfield (PI), Riccardo Bresciani and Jim Woodcock Sep. 2008 - Aug. 2011 SFI RFP/08/CMS1277
This research proposal seeks to explore the space between the hardware and the algorithms of mission-critical filestores, by establishing a series of formal models at each level, linked by formal refinement steps. These models are to be developed within the Unifying Theories of Programming paradigm, in the context of the Grand Challenge GC6 on "Dependable Systems Evolution" which seeks to establish a repository of formally verified computer components. A key research goal is to drive the development of techniques that will be applicable in other such safety-critical application areas.
Unifying Synchronous Systems (USS)
Andrew Butterfield (PI), Pawel Gancarski and Jim Woodcock Sep. 2007 - Aug. 2010 SFI RFP/07/CMSF186
This project will explore the development of a theory of hardware compilers within the UTP framework. Furthermore, it will look at developing a parameterised collection of theories that allow straightforward verification of simple designs, whilst still being able to support reasoning involving the more complex properties required in more sophisticated systems. The key idea is to be able to integrate the simple and complex reasoning as required by the design of different parts of a system.
Foundations of Global Computing
Matthew Hennessy (PI) Feb. 2007 - Jan. 2012 SFI 06 IN.1 1898
The purpose of this SFI project is to develop a sound mathematical and logical understanding for the next generation of widely distributed computing environments. This understanding will be expressed in terms of
- mathematical models of the computational entities underlying these environments
- logical reasoning techniques for assuring their behaviour.
Generic Programming and Theorem Provers
Wendy Verbruggen and Arthur Hughes (PI) Oct. 2005 - Oct. 2009 IRCSET
We propose adding support for kind-indexed generic programming to the proof assistant Coq. Our main goal will be to facilitate reasoning about kind-indexed generic functions. In his habilitationsschrift Hinze uses generic logical relations to be able to prove properties about generic programs that have a kind-indexed type. We propose to lift this technique to the constructive logic of Coq. This will bring all the advantage of Coq to proving properties about generic programs. Coq can guarantee that the proofs are correct, and it will help ensure that the proofs are consistent. We can use the support for proof libraries and specialised tactics in Coq to automate finding solutions to common subgoals that occur often in proofs about generic functions.
Simplifying and extending uniqueness typing
Edsko de Vries and David M Abrahamson (PI) Oct 2004 - Oct 2008 IRCSET
The aim of this work is to extend uniqueness typing with support for first class polymorphism, in particular higher rank types. To be able to do so, we have focussed on simplifying the core uniqueness typing system so that it is sufficiently similar to the conventional Hindley/Milner type system that extensions to H/M type systems can easily be applied in the context of uniqueness typing.
