My primary research interest lies in the area of functional programming, covering foundations, program analysis, language design, (parallel) implementation, and applications. I am particularly interested in symbolic computation and embedded systems as application domains for functional languages and techniques.
My current research focus is on high-level programming models for parallel computation. In particular, I am working on the implementation of Glasgow parallel Haskell (GpH), its application to problems in the area of symbolic computation (in the SCIEnce and HPCGAP projects) and abstractions built on top of GpH (evaluation strategies). I have been involved in the design and implementation of the following programming languages: Glasgow parallel Haskell (GpH), Glasgow distributed Haskell, mobile Haskell and Camelot.
I am also doing research on foundations of programming languages and systems. In particular, I have developed a VDM-style program logic and a specialised resource logic for the expression-level fragment of the embedded systems language Hume. This is based on earlier work on a program logic for resources for a JVM-like language. All of these logics have been formalised and proven sound in Isabelle/HOL.
One particularly interesting area combining foundations and languages is program analysis. As part of my PhD thesis I have developed a granularity analysis for deriving bounds on the costs of (non-recursive) functional programs. More recently I have contributed to the development and implementation of a type-based inference of space and time consumption of Hume programs.
My research vision is one of formally-grounded design of effective and efficient complex systems. The design of such systems should build on formal foundations, such as type systems and program logics, and use formalisations in provers such as Isabelle/HOL to achieve a high degree of dependability and to be provably effective. To be efficient the system should support, as an essential ingredient, modern computer architectures such as multi- and many-core machines in-the-small and grid- and cloud-architectures in-the-large. This vision is exemplified, by using cost information of a granularity analysis to guide the management of parallelism in GpH; by using formally-driven program transformations to enhance the performance of parallel functional programs; by developing a proof-carrying-code infrastructure to assure bounded space consumption of mobile code; by jointly developing and implementing resource analyses for embedded systems programs, and using the resource bounds in compilation and in specialised resource logics for certification.
I am a member of the dependable systems group in the School of Mathematical and Computer Sciences of Heriot-Watt University. I am looking for potential PhD students in any of the areas described above. Visit my home page for contact details.
Last modified: Mon Feb 28 23:48:01 2011