My specific interests include: category theory, especially categorical algebra; equational logic and term rewriting; logical relation and compiler correctness.
Compositional compiler correctness with quantified types
(with Nick Benton).
Submitted.
[preprint: pdf]
[coq script: zip]
Strongly typed term representations in Coq
(with Nick Benton and Andrew Kennedy).
The 4th Informal ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM 2009).
[abstract: pdf]
Biorthogonality, step-indexing and compiler correctness
(with Nick Benton).
Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009).
[preprint: pdf]
[coq script: zip]
On the construction of free algebras for equational systems
(with Marcelo Fiore).
Theoretical Computer Science, 410(18):1704-1729, 2009.
[preprint: pdf]
Term equational systems and logics
(with Marcelo Fiore).
Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2008).
[preprint: pdf]
Equational systems and free constructions
(with Marcelo Fiore).
Proceedings of the 34th International Colloquium on Automata, Languages and Programming (ICALP 2007).
[preprint: pdf]
[errata: pdf]
Non-refereed Publications
Mathematical synthesis of equational deduction systems
(with Marcelo Fiore).
Marcelo's invited address at the 9th International Conference on Typed Lambda Calculi and Applications (TLCA 2009).
[abstract: pdf]
Talks
Logical relations and compositional compiler correctness.
Equational systems and free constructions. ICALP 2007,
University of Wroclaw, Poland, 12 Jul 2007.
[slides: pdf]
Equational systems and free constructions. Extreme Theory Meeting,
Computer Laboratory, Cambridge, UK, 28 Jun 2007.
Algebraic theories in the presence of binding operators, substitution, etc. Semantics Lunch,
Computer Laboratory, Cambridge, UK, 20 Mar 2006.
[slides: pdf]
Abstract models for structural data and its substitution. Extreme Theory Meeting,
Computer Laboratory, Cambridge, UK, 19 Oct 2005.