Glasgow
4pm Tuesday 22nd January 2008
Room 2511, JCMB, King's Buildings
We've recently redesigned Epigram's core type theory to expose a content-free fragment of the type language as a universe a la Tarski of propositions, with
This leads to a new presentation of propositional equality which supports extensional reasoning (as in NuPRL and friends) whilst retaining the good computational properties of intensional type theories (as found in Lego, Coq, Epigram, and Agda). I'll try to explain how this works and outline its potential advantages.
I'll also investigate the opportunties offered by the Prop universe for a high-level Epigram proof language, distinguished from but integrated with the Epigram programming language. It seems to me that proof irrelevance naturally provokes a more declarative style of proof, where we tend to be more explicit about propositions and less explicit about the expressions which inhabit their proof sets. This is in marked contrast to the syntax of programs, where we strive to have the machine infer type information where possible.
I hope to show that there is plenty of scope for fresh thinking in the design of principled programming languages. This talk draws on joint work with many people, but most particularly Thorsten Altenkirch, James McKinna and Nicolas Oury.