Normalization by Evaluation for Martin-L "of Type Theorywith Typed Equality Judgements

Abstract The decidability of equality is proved for Martin-L"oftype theory with a universe 'a la Russell and typed betaeta-equality judgements. A corollary of this result is thatthe constructor for dependent function types is injective, a property which is crucial for establishing the correctness ofthe type-checking algorithm. The decision procedure uses normalization by evaluation, an algorithm which first in-terprets terms in a domain with untyped semantic elements and then extracts normal forms. The correctness of this al-gorithm is established using a PER-model and a logical relation between syntax and semantics