A proof-theoretic foundation of abortive continuations |
| |
Authors: | Zena M Ariola Hugo Herbelin Amr Sabry |
| |
Affiliation: | (1) University of Oregon, Eugene, USA;(2) INRIA-Futurs, Orsay, France;(3) Indiana University, Bloomington, USA |
| |
Abstract: | We give an analysis of various classical axioms and characterize a notion of minimal classical logic that enforces Peirce’s
law without enforcing Ex Falso Quodlibet. We show that a “natural” implementation of this logic is Parigot’s classical natural
deduction. We then move on to the computational side and emphasize that Parigot’s λ
μ corresponds to minimal classical logic. A continuation constant must be added to λ
μ to get full classical logic. The extended calculus is isomorphic to a syntactical restriction of Felleisen’s theory of control
that offers a more expressive reduction semantics. This isomorphic calculus is in correspondence with a refined version of
Prawitz’s natural deduction.
This article is an extended version of the conference article “Minimal Classical Logic and Control Operators” (Ariola and
Herbelin, Lecture Notes in Computer Science, vol. 2719, pp. 871–885, 2003). A longer version is available as a technical report (Ariola
et al., Technical Report TR608, Indiana University, 2005).
Z.M. Ariola supported by National Science Foundation grant number CCR-0204389.
A. Sabry supported by National Science Foundation grant number CCR-0204389, by a Visiting Researcher position at Microsoft
Research, Cambridge, U.K., and by a Visiting Professor position at the University of Genova, Italy. |
| |
Keywords: | Callcc Minimal logic Intuitionistic logic Classical logic |
本文献已被 SpringerLink 等数据库收录! |
|