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 » 
In  Programming Languages and Systems  14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 2123, 2016, Proceedings 
Series  Lecture Notes in Computer Science 
Volume  10017 
Page(s)  187205 
Year  2016 
Abstract 
Prooffunctional logical connectives allow reasoning about the structure of logical proofs, in this way giving to the latter the status of firstclass objects. This is in contrast to classical truthfunctional 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 prooffunctional logic. This calculus, directly derived from a typed calculus previously defined by two of the current authors, has been proved isomorphic to the wellknown BarbaneraDezaniCiancaglinideÕLiguoro type assignment system. We present a logic featuring two prooffunctional 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:
@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 2123, 2016, Proceedings},
tag = {{APLAS 2016}},
localfile = {http://www.di.unito.it/~deligu/papers/APLASRealizIntUnion.pdf},
title = {A Realizability Interpretation for Intersection and Union Types},
abstract = {Prooffunctional logical connectives allow reasoning about the
structure of logical proofs, in this way giving to the latter the
status of firstclass objects. This is in contrast to classical
truthfunctional 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 prooffunctional
logic. This calculus, directly derived from a typed calculus
previously defined by two of the current authors, has been proved
isomorphic to the wellknown
BarbaneraDezaniCiancaglinideÕLiguoro type assignment system. We
present a logic featuring two prooffunctional 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/9783319479583_11},
pages = {187205},
year = {2016},
}
This document was generated by bib2html 3.3.
(Modified by Luca Paolini, under the GNU General Public License)