24 listopada 2016 14:00
Dariusz Biernacki: Minimal classical logic and control operators
I will present the main results of the paper "A Proof-Theoretic Foundation of Abortive Continuations" by Zena M. Ariola, Hugo Herbelin, and Amr Sabry, published in Higher-Order and Symbolic Computation in 2007. The abstract of the paper follows:
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.