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 metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-00906299
Contributor : Dale Miller <>
Submitted on : Tuesday, November 19, 2013 - 3:07:22 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on: Thursday, February 20, 2014 - 9:26:27 AM

File

lics13.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00906299, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

446

Files downloads

245