Paper: Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements (at LICS 2007)

Authors: Andreas Abel Thierry Coquand Peter Dybjer

Abstract

The decidability of equality is proved for Martin-Lof type theory with a universe Ža la Russell and typed beta-eta- equality judgements. A corollary of this result is that the constructor for dependent function types is injective, a property which is crucial for establishing the correctness of the type-checking algorithm. The decision procedure uses normalization by evaluation, an algorithm which first interprets terms in a domain with untyped semantic elements and then extracts normal forms. The correctness of this algorithm is established using a PER-model and a logical relation between syntax and semantics.

BibTeX

  @InProceedings{AbelCoquandDybjer-NormalizationbyEval,
    author = 	 {Andreas Abel and Thierry Coquand and Peter Dybjer},
    title = 	 {Normalization by Evaluation for Martin-Löf Type Theory with Typed Equality Judgements},
    booktitle =  {Proceedings of the Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)},
    year =	 {2007},
    month =	 {July}, 
    pages =      {3--12},
    location =   {Wroclaw, Poland}, 
    publisher =	 {IEEE Computer Society Press}
  }