A Realizability Interpretation for Intersection and Union Types
| Autor: | Claude Stolze, Daniel J. Dougherty, Ugo de'Liguoro, Luigi Liquori |
|---|---|
| Přispěvatelé: | Department of Computer Science (WPI CS), Worcester Polytechnic Institute, Dipartimento di Informatica [Torino], Università degli studi di Torino = University of Turin (UNITO), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure - Rennes (ENS Rennes), Université Pierre et Marie Curie - Paris 6 (UPMC), European Project: COST Action CA15123 ,COST - European Cooperation in Science and Technology,EUTYPES(2016), Università degli studi di Torino (UNITO) |
| Rok vydání: | 2016 |
| Předmět: |
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory
Computer science 0102 computer and information sciences Intuitionistic logic Intersection and union types 01 natural sciences Dependent type Curry–Howard correspondence Theoretical Computer Science Church-style vs. Curry-style [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] Explicitely typed calculi vs. implicitely typed calculi Computer Science::Logic in Computer Science Realizability 0101 mathematics Proof-functional logics ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.3: Studies of Program Constructs/F.3.3.4: Type structure [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC] [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Simply typed lambda calculus System F realizability intersection and union types 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] Pure type system ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.2: Lambda calculus and related systems Algebra [MATH.MATH-LO]Mathematics [math]/Logic [math.LO] TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Algorithm Typed lambda calculus |
| Zdroj: | Programming Languages and Systems ISBN: 9783319479576 APLAS 14th Asian Symposium on Programming Languages and Systems 14th Asian Symposium on Programming Languages and Systems, Nov 2016, Hanoi, Vietnam |
| DOI: | 10.1007/978-3-319-47958-3_11 |
| Popis: | International audience; 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 cal- culus, 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|