A Realizability Interpretation for Intersection and Union Types

Abstract : Proof-functional logical connectives allow reasoning about the structure of logical proofs, in this way giving to the latter the status of first-class objects. This is in contrast to classical truth-functional con- nectives where the meaning of a compound formula is dependent only on the truth value of its subformulas. In this paper we present a typed lambda calculus, enriched with strong products, strong sums, and a related proof-functional logic. This cal- culus, directly derived from a typed calculus previously defined by two of the current authors, has been proved isomorphic to the well-known Barbanera-Dezani-Ciancaglini-de’Liguoro type assignment system. We present a logic L∩∪ featuring two proof-functional connectives, namely strong conjunction and strong disjunction. We prove the typed calculus to be isomorphic to the logic L∩∪ and we give a realizability semantics using Mints’ realizers [Min89] and a completeness theorem. A prototype implementation is also described.
Type de document :
Communication dans un congrès
14th Asian Symposium on Programming Languages and Systems, Nov 2016, Hanoi, Vietnam. Springer Verlag, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01317213
Contributeur : Luigi Liquori <>
Soumis le : vendredi 9 septembre 2016 - 11:38:57
Dernière modification le : mercredi 28 novembre 2018 - 01:22:44
Document(s) archivé(s) le : samedi 10 décembre 2016 - 12:55:32

Fichier

0-paper.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01317213, version 2

Collections

Citation

Daniel J. Dougherty, Ugo De 'Liguoro, Luigi Liquori, Claude Stolze. A Realizability Interpretation for Intersection and Union Types. 14th Asian Symposium on Programming Languages and Systems, Nov 2016, Hanoi, Vietnam. Springer Verlag, Lecture Notes in Computer Science. 〈hal-01317213v2〉

Partager

Métriques

Consultations de la notice

437

Téléchargements de fichiers

176