What this page used to say
- Eliminating Dependent Pattern Matching
with Healfdene Goguen and
proves the reducibility of dependent pattern matching to old-fashioned
eliminators and heterogeneous equality. In particular, we show how to
formulate reduction rules which actually make sense, and that the translated
programs preserve this computational behaviour.
- Exploring the Regular Tree Types
with Peter Morris
and Thorsten Altenkirch. Draft.
- A Few Constructions on Constructors
with Healf Goguen
and James McKinna. Draft.
- Why Dependent Types Matter
with Thorsten Altenkirch and
James McKinna. Submitted to ICFP 2005.
AFP notes on practical
programming in Epigram. In colour. Shortly to appear in an LNCS volume.
I am not a number: I am a free variable
with James McKinna. This is the first instalment of how-to-implement-Epigram,
but it's generally useful stuff if you're hacking around with syntax.
Presented at the Haskell Workshop 2004, in
Utah, but not by either of us:
thanks to Thomas, no thanks to KLM.
- The view from the left with
James McKinna. By accident, this paper is effectively the definition
Status: in JFP 14(1). Here's our typechecker
example, written almost live at MGS this year. And yes, we know about
the bug in the ML version of elem to be found in this draft: simple
type systems have the property that you can replace any
subexpression of a well-typed term by another of the same type!
- The view from the left (as we
originally wrote it) This version has much less to say
about typechecking and much more to say about interactive programming.
- First-order unification by structural
recursion Contains the world's shortest termination proof of
unification... Status: in JFP 13(6). Accompanied by
(correctness proof, OLEG development).
- Faking It (Simulating Dependent Types in
Haskell). Even before the revolution, we can still abuse the
class system. With a side order of nested-types-are-not-as-much-fun.
- Inductive Families Need Not Store Their
Indices with Edwin
Brady and James McKinna. The more static information your
compiler has, the better the object code it can spit out. Epigram
has more static information than we know what to do with. This paper
shoots the first few fish in that barrel. Status: in TYPES 2003.
- With the Container gang:
and Neil Ghani:
- Generic Programming Within Dependently Typed
Here we give a universe construction for a whole scary bunch of
types you'd find in Haskell, and then we write some generic
programs using OLEG. It's a pity Epigram wasn't around at the
time. Status: in WCGP 2002.
- Elimination with a Motive. A modern
convenience no theorem prover should be without. Sez I. Status:
in TYPES 2000.
- Dependently Typed Programs and their
My campaign to burn my thesis has not yet succeeded. It's still the only
place where I've written up OLEG, my holey type theory with
It's also the place to go for all those gadgets like proofs of Peano
axioms. Caution: I was East Ham when I wrote it. Many thanks to my
supervisor, Rod Burstall, and to my uncles, James McKinna,
Healf Goguen and
Hofmann. Apologies to my examiners,
Christine Paulin-Mohring and
- Inverting Inductively Defined Relations in
LEGO. The paper emerging from my MSc, supervised by James McKinna
and Alan Smaill. This is where I learned the song I've been singing ever
since. Status: in TYPES 1996.
- The Derivative of a Regular Type is its Type of
One-Hole Contexts Status: unpublished. My most
influential work, some allege.
Old slides live in the Colour Supplement.
Newer slides live in my filing cabinet (sorry!), but my APPSEM 2003 gig
and Sensibility has been scanned recently (ta!).
Thatcher's children and inquisitive non-Brits may find