EPISODE · Jan 6, 2020 · 11 MIN
Curry-Howard for classical logic
from Iowa Type Theory Commute · host Aaron Stump
CH can be applied to classical logic, too. The seminal paper is <a href="https://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf">A Formulae-as-Types Notion of Control</a> by Timothy Griffin. I discuss how backtracking implements the law of excluded middle.
What this episode covers
CH can be applied to classical logic, too. The seminal paper is <a href="https://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf">A Formulae-as-Types Notion of Control</a> by Timothy Griffin. I discuss how backtracking implements the law of excluded middle.
NOW PLAYING
Curry-Howard for classical logic
No transcript for this episode yet
Similar Episodes
Mar 4, 2026 ·7m
Feb 22, 2026 ·9m
Feb 8, 2026 ·11m
Feb 2, 2026 ·12m
Jan 30, 2026 ·31m
Jan 29, 2026 ·39m