Skip to Main content Skip to Navigation
New interface
Conference papers

Unifying Classical and Intuitionistic Logics for Computational Control

Abstract : We show that control operators and other extensions of the Curry-Howard isomorphism can be achieved without collapsing all of intuitionistic logic into classical logic. For this purpose we introduce a unified propositional logic using polarized formulas. We define a Kripke semantics for this logic. Our proof system extends an intuitionistic system that already allows multiple conclusions. This arrangement reveals a greater range of computational possibilities, including a form of dynamic scoping. We demonstrate the utility of this logic by showing how it can improve the formulation of exception handling in programming languages, including the ability to distinguish between different kinds of exceptions and constraining when an exception can be thrown, thus providing more refined control over computation compared to classical logic. We also describe some significant fragments of this logic and discuss its extension to second-order logic.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Tuesday, November 19, 2013 - 3:07:22 PM
Last modification on : Friday, November 18, 2022 - 9:26:55 AM
Long-term archiving on: : Thursday, February 20, 2014 - 9:26:27 AM


Files produced by the author(s)


  • HAL Id : hal-00906299, version 1



Chuck Liang, Dale Miller. Unifying Classical and Intuitionistic Logics for Computational Control. LOGIC IN COMPUTER SCIENCE (LICS 2013), Jun 2013, New Orleans, United States. ⟨hal-00906299⟩



Record views


Files downloads