- 2015-04-23:
The Incremental λ-Calculus and Relational Parametricity - 2015-04-19:
Slides for “An Algebraic Approach to Typechecking and Elaboration” - 2015-04-17:
Propositions as Filenames, Builds as Proofs: The Essence of Make - 2014-01-29:
POPL Slides - 2013-07-17:
One Done, Two Submitted - 2013-03-29:
Productive Coprogramming with Guarded Recursion - 2012-11-07:
Theorems for Free - 2012-11-07:
Abstraction and Invariance for Algebraically Indexed Types - 2012-09-06:
Interleaving Data and Effects - 2012-09-05:
Relational Parametricity for Higher Kinds - 2012-01-06:
Reasoning about Stream Processing with Effects - 2011-12-14:
A Type Checker that knows its Monad from its Elbow - 2011-11-14:
How to be a Productive Programmer - 2011-04-28:
On Structural Recursion II: Folds and Induction - 2011-04-22:
On Structural Recursion

- Models for Polymorphism over Physical Dimensions,
*TLCA 2015* - Interleaving data and effects,
*Journal of Functional Programming (to appear), 2015* - From Parametricity to Conservation Laws, via Noether's Theorem,
*POPL 2014* - A Relationally Parametric Model of Dependent Type Theory,
*POPL 2014* - Abstraction and Invariance for Algebraically Indexed Types,
*POPL 2013* - Productive Coprogramming with Guarded Recursion,
*ICFP 2013* - Relational Parametricity for Higher Kinds,
*CSL 2012* - Fibrational Induction Meets Effects,
*FoSSaCS 2012* - Refining Inductive Types,
*Logical Methods in Computer Science* - The Semantics of Parsing with Semantic Actions,
*LICS 2012* - Amortised Resource Analysis with Separation Logic,
*Logical Methods in Computer Science* - When Is a Type Refinement an Inductive Type?,
*FoSSaCS 2011* - Amortised Resource Analysis with Separation Logic,
*ESOP 2010* - Symbolic and Analytic Techniques for Resource Analysis of Java Bytecode,
*TGC 2010* - Algebras for Parameterised Monads,
*CALCO 2009* - A Deep Embedding of Parametric Polymorphism in Coq,
*WMM 2009* - Parameterised notions of computation,
*Journal of Functional Programming* - Syntax for Free: Representing Syntax with Binding Using Parametricity,
*TLCA 2009* - Unembedding domain-specific languages,
*Haskell Symposium 2009* - What is a Categorical Model of Arrows?,
*MSFP 2008* - Secure Execution of Mobile Java using Static Analysis and Proof Carrying Code,
*UK e-Science All-Hands Meeting 2007* - CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types,
*TYPES 2007* - Specifying and Verifying Heap Space Allocation with JML and ESC/Java2,
*FTfJP 2006* - Parameterised Notions of Computation,
*MSFP 2006* - Substructural Simple Type Theories for Separation and In-place Update,
*PhD Thesis* - A 𝜆-Calculus for Resource Separation,
*ICALP 2004*