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.