Every proof assistant: Epigram 2 - Autopsy, Obituary, Apology
source link: http://math.andrej.com/2020/06/09/epigram-2-autopsy-obituary-apology/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
Every proof assistant: Epigram 2 - Autopsy, Obituary, Apology
This week shall witness a performance by Conor McBride.
Epigram 2: Autopsy, Obituary, Apology
Time: Thursday, June 11, 2020 from 16:00 to 17:00 (Central European Summer Time, UTC+2)
Location: online at Zoom ID 989 0478 8985
Speaker: Conor McBride (University of Strathclyde)
Proof assistant: Epigram 2Abstract: "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.
Upcoming talks:
Post a comment:
$⋯$ for inline and $$⋯$$ for display LaTeX formulas,
and <pre>⋯</pre> for display code. Your E-mail address is only used to compute
your Gravatar and is not stored anywhere.
Comments are moderated through pull requests.
Name
Website
Comment
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK