To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Normalization by Evaluati… - University of Gothenburg, Sweden Till startsida
Sitemap
To content Read more about how we use cookies on gu.se

Normalization by Evaluation for Martin-Löf Type Theory with Equality Judgements

Journal article
Authors Andreas Abel
Thierry Coquand
Peter Dybjer
Published in Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007.
Pages 3-12
Publication year 2007
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Pages 3-12
Language en
Links dx.doi.org/10.1109/lics.2007.33
Subject categories Computer science

Abstract

The decidability of equality is proved for Martin-Löf 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.

Page Manager: Webmaster|Last update: 9/11/2012
Share:

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?