Curry-Howard for classical logic

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

b'

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.

'