Name
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 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. |
Year | Venue | Field |
|---|---|---|
2016 | APLAS | Intuitionistic logic,Algebra,Typed lambda calculus,Simply typed lambda calculus,Computer science,System F,Algorithm,Theoretical computer science,Pure type system,Dependent type,Realizability,Curry–Howard correspondence |
DocType | Citations | PageRank |
Conference | 2 | 0.37 |
References | Authors | |
9 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel J. Dougherty | 1 | 413 | 32.13 |
| Ugo de'Liguoro | 2 | 251 | 23.50 |
| Luigi Liquori | 3 | 398 | 38.85 |
| Claude Stolze | 4 | 2 | 0.71 |