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 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 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 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.
CITATION STYLE
Dougherty, D. J., de’Liguoro, U., Liquori, L., & Stolze, C. (2016). A realizability interpretation for intersection and union types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10017 LNCS, pp. 187–205). Springer Verlag. https://doi.org/10.1007/978-3-319-47958-3_11
Mendeley helps you to discover research relevant for your work.