Name
Abstract | ||
|---|---|---|
We present an algorithm for computing normal terms and types in Martin-Lof type theory with one universe and eta-conversion. We prove that two terms or types are equal in the theory iff the normal forms are identical (as de Bruijn terms). It thus follows that our algorithm can be used for deciding equality in Martin-Lof type theory. The algorithm uses the technique of normalization by evaluation; normal forms are computed by first evaluating terms and types in a suitable model. The normal forms are then extracted from the semantic elements. We prove its completeness by a PER model and its soundness by a Kripke logical relation. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.entcs.2007.02.025 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
normalization by evaluation,normal term,theory iff,per model,type theory,domain semantics,normal form,de bruijn term,universe,suitable model,dependent types,kripke logical relation,semantic element,martin-lof type theory,martin lof type theory | Discrete mathematics,Normalization (statistics),Intuitionistic type theory,Type theory,Universe,Soundness,De Bruijn sequence,Completeness (statistics),Mathematics | Journal |
Volume | ISSN | Citations |
173, | Electronic Notes in Theoretical Computer Science | 7 |
PageRank | References | Authors |
0.58 | 9 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andreas Abel | 1 | 49 | 4.61 |
| Klaus Aehlig | 2 | 123 | 12.08 |
| Peter Dybjer | 3 | 540 | 76.99 |