Research Papers
A selection of reseach papers that the Epigram community has produced over the last couple of years, they are split into two categories, those about implementing Epigram, and those about writing programs in Epigram.
Implementing Epigram
- I am not a number: I am a free variable
Conor McBride and James McKinna in Haskell Workshop 2004
Pt. 1 of how to implement Epigram - Epigram Reloaded: A Standalone Typechecker for ETT
James Chapman, Thorsten Altenkirch and Conor McBride in TFP 2005
Pt. 2 of how to implement Epigram - A few constructions on constructors
Conor McBride, Healfdene Goguen and James McKinna
A recipe book for creating the kind of gadgets used to elaborate Epigram programs - Eliminating Dependent Pattern Matching
Conor McBride, Healfdene Goguen and James McKinna in Joseph Goguen's forthcoming Festschrift (LNCS 4060)
Makes precise the translation from dependent pattern matching to elimination operators - Towards Observational Type Theory
Thorsten Altenkirch and Conor McBride Extensional Equality in Intentional Type Theory - Elimination with a motive
Conor McBride in TYPES 2000
a presentation of a tactic Epigram could not be without - The view from the left
Conor McBride and James McKinna in JFP 14(1)
accidental candidate for the definition of Epigram - The view from the left (early version)
Conor McBride and James McKinna
an earlier draft of the above that has more stuff to say on interactive programming - Inductive families need not store their indicies
Edwin Brady, Conor McBride and James McKinna in TYPES 2003
one way in which we can optimise compiled Epigram code - Dependently type programs and their proofs
Conor McBride
still contains slightly less that isn't available elsewhere
Programming in Epigram
- Tait in one big step
James Chapman and Thorsten Altenkirch in MSFP 2006
Implementing a functional normaliser for Gödel's System T in Epigram (Final version in preparation) - Why dependent types matter
Thorsten Altenkirch, Conor McBride and James McKinna
an exposition of the art of Epigram - Exploring the Regular Types
Peter Morris, Conor McBride and Thorsten Altenkirch in TYPES 2004
using a universe construction to write some generic programs