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.
