[1] 
Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori, and Claude Stolze.
A realizability interpretation for intersection and union types.
In Programming Languages and Systems  14th Asian Symposium,
APLAS 2016, Hanoi, Vietnam, November 2123, 2016, Proceedings, pages
187205, 2016.
[ bib 
DOI 
http ]
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 connectives 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 products, coproducts, 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 L featuring two prooffunctional 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 [?] and a completeness theorem. A prototype implementation is also described.

This file was generated by bibtex2html 1.97.