Download the complete article:

@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},
}

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