The Curry–Howard correspondence also raised new questions regarding the computational content of proof concepts which were not covered by the original works of Curry and Howard. In particular, classical logic has been shown to correspond to the ability to manipulate the continuation of programs and the symmetry of sequent calculus to express the duality between the two evaluation strategies known as call-by-name and call-by-value.

Speculatively, the Curry–Howard correspondence may be expected to lead to a substantial unification between mathematical logic and foundational computer science: …

— Wikipedia on Curry–Howard correspondence

2010.03.08 Monday ACHK