# What sort of program is a proof?

Conor McBride 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

Prf : Prop -> Set Proofs of propositions are never inspected for computational purposes, hence we may establish proof irrelevance, identifying all inhabitants of Prf P definitionally.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.