2008 | OriginalPaper | Buchkapitel
Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory
verfasst von : Andreas Abel, Thierry Coquand, Peter Dybjer
Erschienen in: Mathematics of Program Construction
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. 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.