Unifying Classical and Intuitionistic Logics for Computational Control - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Unifying Classical and Intuitionistic Logics for Computational Control

Résumé

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.
Fichier principal
Vignette du fichier
lics13.pdf (143.11 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-00906299 , version 1 (19-11-2013)

Identifiants

  • HAL Id : hal-00906299 , version 1

Citer

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⟩
169 Consultations
206 Téléchargements

Partager

Gmail Facebook X LinkedIn More