My thesis clarified the relationships between existing dialects of ML and studied extending ML with support for recursive modules. Solve a critical problem involving the interaction of recursion and data abstraction known as the double vision problem. In other work with Bob Harper and Manuel Chakravarty, I showed how to extend ML with support for overloading and ad hoc polymorphism through Haskell-style type classes. This work exposes connections between ML modules and Haskell type classes, resulting in a unifying account of the two features Andreas and I have developed a novel module system design that addresses one of the key remaining problems with recursive modules, namely separate compilation. This design seamlessly integrates elements of both traditional ML module systems and Bracha-style mixin modules, resulting in a minimalist account of the ML module system that unifies features. A prototype is available
I am a postdoctoral research fellow, interested in type theory, dependently typed functional programming, multi-stage programming, compilers and programming language design. I am now working on the Generative Programming for Embedded Systems project, in the context of the Hume programming language. Software * Idris, an experimental language with full dependent types. * Ivor, a type theory based theorem proving engine with a Haskell API. * A Supercombinator Compiler, intended as a back end for Epigram. Some other toys: * A simple functional language with a built-in theorem prover, implemented with the help of Ivor. * An implementation of the simply typed lambda calculus in Ivor, with a Haskell driver. * An SK calculus evaluator, being a small experiment in modelling partial functions in Coq.