User:DPMulligan
I'm a post-doctoral computer scientist at the University of Bologna, Italy, working on a verified compiler for a large subset of the C programming language. Prior to this, I was a PhD student at Heriot-Watt University in Edinburgh, Scotland, working on nominal techniques, context calculi and proof terms for incomplete derivations.
My homepage is [http://www.macs.hw.ac.uk/~dpm8 here]. I also run a blog on name binding (nominal techniques, higher-order abstract syntax, de Bruijn indices etc.) and that can be found [http://namebinding.wordpress.com here].
I'm originally from Wigan, Greater Manchester, England.
=Pages started=
- Rippling, meta-level heuristic guidance for inductive proof.
- IsaPlanner, a proof planning system for Isabelle.
- Nominal techniques, a group of related techniques for working with, and simplifying the reasoning about, languages with name binders.
- Nominal terms, a metalanguage for embedding object languages with name binding constructs into.
=Pages I've made significant contributions to=
- Lambda calculus, a formal system that internalises the notion of function
- Unification, the process of synthesising a substitution that identifies two input terms