CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Normalization by evaluation for Martin-Löf type theory with one universe

Andreas Abel ; Klaus Aehlig ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers) ; Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Mathematical Foundations of Programming Semantics, New Orleans, LA, USA, April 2007. Ed. M. Fiore. Electronic Notes in Theoretical Computer Science, Elsevier. Vol. 173 (2007), p. 17-40.
[Konferensbidrag, refereegranskat]

We present an algorithm for computing normal terms and types in Martin-Löf 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-Löf 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.



Denna post skapades 2007-05-07. Senast ändrad 2016-10-18.
CPL Pubid: 41353