Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

DoughertydLS16 (In proceedings)
Author(s) Daniel J. Dougherty, Ugo de' Liguoro, Luigi Liquori and Claude Stolze
Title« A Realizability Interpretation for Intersection and Union Types »
InProgramming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings
SeriesLecture Notes in Computer Science
Volume10017
Page(s)187--205
Year2016
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 calculus, 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 featuring two proof-functional connectives, namely strong conjunction and strong disjunction. We prove the typed calculus to be isomorphic to the logic and we give a realizability semantics using MintsÕ realizers and a completeness theorem. A prototype implementation is also described.

Download the complete article: APLAS-RealizIntUnion.pdf

BibTeX code

@inproceedings{DoughertydLS16,
  volume = {10017},
  author = {Daniel J. Dougherty and Ugo de' Liguoro and Luigi Liquori and Claude
            Stolze},
  series = {Lecture Notes in Computer Science},
  booktitle = {Programming Languages and Systems - 14th Asian Symposium, {APLAS}
               2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings},
  tag = {{APLAS 2016}},
  localfile = {http://www.di.unito.it/~deligu/papers/APLAS-RealizIntUnion.pdf},
  title = {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 calculus, 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 featuring two proof-functional connectives, namely
              strong conjunction and strong disjunction. We prove the typed
              calculus to be isomorphic to the logic and we give a realizability
              semantics using Mints’ realizers and a completeness theorem. A
              prototype implementation is also described.},
  doi = {10.1007/978-3-319-47958-3_11},
  pages = {187--205},
  year = {2016},
}


 Chronological Overview 
 Type-Hierarchical Overview 
Formal Methods in Computing
(Most of the papers antecedent to 1995
are not included in the list)
FRAMES  NO FRAME 

This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)

Valid HTML 4.01!