Name
Abstract | ||
|---|---|---|
This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type which is substitutive, allowing us to reason by replacing equal for equal in propositions;which reflects the observable behaviour of values rather than their construction: in particular, we have extensionality-- functions are equal if they take equal inputs to equal outputs;which retains strong normalisation, decidable typechecking and canonicity--the property that closed normal forms inhabiting datatypes have canonical constructors; which allows inductive data structures to be expressed in terms of a standard characterisation of well-founded trees;which is presented syntactically--you can implement it directly, and we are doing so this approach stands at the core of Epigram 2;which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system [21].. Until now, it has always been necessary to sacrifice some of these aspects. The closest attempt in the literature is Altenkirch's construction of a setoid-model for a system with canonicity and extensionality on top of an intensional type theory with proof-irrelevant propositions [4]. Our new proposal simplifies Altenkirch's construction by adopting McBride's heterogeneous approach to equality [19]. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1145/1292597.1292608 | PLPV |
Keywords | Field | DocType |
propositional equality,equal output,equal input,intensional type theory,heterogeneous approach,standard characterisation,standard examples package,new proposal,proof system,observational equality,propositional equality type,data structure,type theory,normal form | Data structure,Extensionality,Observable,Embedding,Computer science,Algorithm,Type theory,Decidability,Agda | Conference |
Citations | PageRank | References |
29 | 1.70 | 14 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Thorsten Altenkirch | 1 | 668 | 56.85 |
| Conor McBride | 2 | 752 | 47.89 |
| Wouter Swierstra | 3 | 196 | 15.46 |