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
Pt. 1 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 - Elimination with a motive
Conor McBride in TYPES 2000
a presentation of a tactic Epigram could not be without - A view from the left
Conor McBride and James McKinna in JFP 14(1)
accidental candidate for the definition of Epigram - Another view from the left
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 much that isn't available elsewhere
Programming in Epigram
- 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
using a universe construction to write some generic programs