CONSTRUCTIVE CLASSICAL LOGIC AS CPS-CALCULUS
Ichiro Ogata · International Journal of Foundations of Computer Science · 2000
We establish the Curry-Howard isomorphism between constructive classical logic and [Formula: see text]-calculus. [Formula: see text]-calculus exactly means the target language of Continuation Passing Style (CPS) transforms. Constructive classical logic we refer to are LKT and LKQ introduced by Danos et al.(1993).