What this page used to say
.bib
 Eliminating Dependent Pattern Matching
with Healfdene Goguen and
James McKinna
proves the reducibility of dependent pattern matching to oldfashioned
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.
 my
AFP notes on practical
dependently typoed
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 howtoimplementEpigram,
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
of Epigram
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 welltyped 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.
 Firstorder unification by structural
recursion Contains the world's shortest termination proof of
unification... Status: in JFP 13(6). Accompanied by
online resources
(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 nestedtypesarenotasmuchfun.
 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:
Michael Abbott,
Thorsten Altenkirch,
and Neil Ghani:
 Generic Programming Within Dependently Typed
Programming with
Thorsten Altenkirch.
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
Proofs.
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
proofstatesasvalidcontexts, tacticsasadmissiblerules.
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
Martin
Hofmann. Apologies to my examiners,
Christine PaulinMohring and
Alex Simpson.
 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
OneHole 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
Sense
and Sensibility has been scanned recently (ta!).
Thatcher's children and inquisitive nonBrits may find
this helpful...