Abstract
We show that the one can consider proof of the Gentzen's LK as the continuation passing style(CPS) programs; and the cut-elimination procedure for LK as computation. To be more precise, we observe that Strongly Normalizable(SN) and Church-Rosser(CR) cut-elimination procedure for (intuitionistic decoration of) LKT and LKQ, as presented in Danos et al.(1993), precisely corresponds to call-by-name(CBN) and call-by-value(CBV) CPS calculi, respectively. This can also be seen as an extension to classical logic of Zucker-Pottinger-Mints investigation of the relations between cut-elimination and normalization.
Cite
CITATION STYLE
Ogata, I. (1998). Cut elimination for classical proofs as continuation passing style computation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1538, pp. 61–78). Springer Verlag. https://doi.org/10.1007/3-540-49366-2_5
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
