Title
A proof-theoretic foundation of abortive continuations
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.
Year
DOI
Venue
2007
10.1007/s10990-007-9007-z
Higher-Order and Symbolic Computation
Keywords
DocType
Volume
classical logic,minimal logic,intuitionistic logic,natural deduction
Journal
20
Issue
Citations 
PageRank 
4
9
0.53
References 
Authors
21
3
Name
Order
Citations
PageRank
Zena M. Ariola148238.61
Hugo Herbelin243530.00
Amr Sabry352035.46