<p>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.</p>

CH can be applied to classical logic, too. The seminal paper is A Formulae-as-Types Notion of Control by Timothy Griffin. I discuss how backtracking implements the law of excluded middle.

<p>CH can be applied to classical logic, too.&nbsp; The seminal paper is <a href="https://www.cl.cam.ac.uk/~tgg22/publications/popl90.pdf" rel="noopener noreferrer">A Formulae-as-Types Notion of Control</a> by Timothy Griffin.&nbsp; I discuss how backtracking implements the law of excluded middle.</p>

Curry-Howard for classical logic

Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.

Share Curry-Howard for classical logic

Sign up to save your podcasts

Curry-Howard for classical logic

Curry-Howard for classical logic