This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)
Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements
Wroclaw, Poland
July 10-July 14
ISBN: 0-7695-2908-9
ASCII Text
x 
 
Andreas Abel, Thierry Coquand, Peter Dybjer, "Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements," Logic in Computer Science, Symposium on, pp. 3-12, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007.
 
 
BibTex
x
 
@article{ 10.1109/LICS.2007.33,
author = {Andreas Abel and Thierry Coquand and Peter Dybjer},
title = {Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements},
journal ={Logic in Computer Science, Symposium on},
volume = {0},
year = {2007},
issn = {1043-6871},
pages = {3-12},
doi = {http://doi.ieeecomputersociety.org/10.1109/LICS.2007.33},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Logic in Computer Science, Symposium on
TI - Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements
SN - 1043-6871
SP3
EP12
A1 - Andreas Abel,
A1 - Thierry Coquand,
A1 - Peter Dybjer,
PY - 2007
KW - null
VL - 0
JA - Logic in Computer Science, Symposium on
ER -
 
Andreas Abel, Ludwig-Maximilians-Universitat, Germany
Thierry Coquand, Chalmers University of Technology, Sweden
Peter Dybjer, Chalmers University of Technology, Sweden
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.
Citation:
Andreas Abel, Thierry Coquand, Peter Dybjer, "Normalization by Evaluation for Martin-Lof Type Theory with Typed Equality Judgements," lics, pp.3-12, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.