Conor McBride – Epigram 2: Autopsy, Obituary, Apology
Channel: FMF Foundations seminar
Date: 02/11/2021

Epigram 2: Autopsy, Obituary, Apology

Time: Thursday, June 11, 2020
Speaker: Conor McBride (University of Strathclyde)
Proof assistant: https://github.com/mietek/epigram2

Abstract: "A good pilot is one with the same number of take-offs and landings." runs the old joke, which makes me a very bad pilot indeed. The Epigram 2 project was repeatedly restarted several times in the late 2000s and never even reached cruising altitude. This talk is absolutely not an attempt to persuade you to start using it. Rather, it is an exploration of the ideas which drove it: proof irrelevant observational equality, first class datatype descriptions, nontrivial equational theories for neutral terms. We may yet live to see such things. Although the programming language elaborator never happened, the underlying proof engine was accessible via an imperative interface called "Cochon": we did manage some interesting constructions, at least one of which I can walk through. I'll also explore the reasons, human and technological, why the thing did not survive the long dark.