My research is centred on distributed systems, networks, compilers, and programming languages.
See also my old research page.
Distributed languages
Most programming languages in use today were designed for writing programs to run on a single computer. Most programs being written today, however, are distributed systems, with components running on multiple computers distributed across the Internet. Unsurprisingly, the languages we use do not make it easy to develop these systems. One recent focus of my research, therefore, has been the design of new language features to make the development of distributed systems easier and more reliable. These features are showcased in the language Acute.
Specifying TCP/IP
The vast majority of Internet communication is conducted using TCP, accessed through the Berkeley Sockets API. Despite this, the precise details of how TCP and Sockets should behave are surprisingly unclear, and the various implementations do in fact differ - sometimes in significant ways. Both developers of distributed systems / middleware and implementors of new TCP/IP stacks would benefit greatly from a precise description of TCP and Sockets as they exist in practice, rather than a theoretical description of an ideal. Recently we have developed such a description, and we are beginning to apply it to the construction of reliable middleware.
Program analysis
As programming languages become higher-level, the programmer has to write less code in order to achieve the same effect. This saves time, but more importantly reduces the opportunity for error - bug rates have been shown to be proportional to the number of lines of code, independent of language. However, as the gap between source language and target machine code becomes greater, the compiler must work harder and smarter: programs must be optimised, not merely translated. A promising technique in this area is type-based program analysis: the property upon which the optimisation depends is described formally by a type system, and the compiler calculates it using a custom type inference. I have applied this technique to usage analysis, optimising thunk update and inlining in Haskell. Along the way I developed simple polymorphism, a novel technique for simplifying such analyses.
Modular semantics
The definition of a programming language is a large formal document. Just like a program, a definition constructed from modular components is far more intelligible, maintainable, and extensible than one constructed as a single monolithic object. I applied the techniques of monadic semantics in order to modularise an early version (AN-1) of the Action Semantics language definition framework. I am pleased to report that the new version, AN-2, is much more modular in structure.
Miscellaneous
Other research not fitting into the above categories.