Curry-Howard for classical logic

Published: Jan. 6, 2020, 9 p.m.

CH can be applied to classical logic, too.\xa0 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.\xa0 I discuss how backtracking implements the law of excluded middle.