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.
Type de document :
Communication dans un congrès
Orna Kupferman. LOGIC IN COMPUTER SCIENCE (LICS 2013), Jun 2013, New Orleans, United States. 2013
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00906299
Contributeur : Dale Miller <>
Soumis le : mardi 19 novembre 2013 - 15:07:22
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : jeudi 20 février 2014 - 09:26:27

Fichier

lics13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00906299, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

381

Téléchargements de fichiers

118