2008 | OriginalPaper | Chapter
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
Authors : Andreas Abel, Thierry Coquand, Peter Dybjer
Published in: Mathematics of Program Construction
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Type-checking algorithms for dependent type theories often rely on the interpretation of terms in some semantic domain of
values
when checking equalities. Here we analyze a version of Coquand’s algorithm for checking the
βη
-equality of such semantic values in a theory with a predicative universe hierarchy and large elimination rules. Although this algorithm does not rely on normalization by evaluation explicitly, we show that similar ideas can be employed for its verification. In particular, our proof uses the new notions of
contextual
reification and
strong semantic equality
.
The algorithm is part of a bi-directional type checking algorithm which checks whether a normal term has a certain semantic type, a technique used in the proof assistants Agda and Epigram. We work with an abstract notion of semantic domain in order to accommodate a variety of possible implementation techniques, such as normal forms, weak head normal forms, closures, and compiled code. Our aim is to get closer than previous work to verifying the type-checking algorithms which are actually used in practice.