bread_juice

I'm not an expert, so please take the following with the grain of salt.

One of the examples of computation formalisms providing the classical logic at the type level is the Parigot's [λμ-calculus](https://en.wikipedia.org/wiki/Lambda-mu_calculus). λμ-calculus adds μ-abstraction to the classical λ-calculus.

μ-abstraction resembles the notion of continuation. With that addition Peirce's law of classical logic becomes deductible without any modifications (e.g. double-negation translation). The program that proves Peirce's law is just call/cc function.

This topic seems to be an ongoing research, so you may find lots of articles in public internet space. Many interesting introductory articles are among the advanced materials of [this course](https://www.cs.ru.nl/~freek/courses/tt-2011/), including the original Parigot's paper.

That's fantastic! Being a lecturer at one of the universities I am very grateful to this research. It changes my perspective.