### Skapa referens, olika format (klipp och klistra)

**Harvard**

Abel, A., Coquand, T. och Dybjer, P. (2008) *Verifying a semantic βη-conversion test for martin-löf type theory*.

** BibTeX **

@conference{

Abel2008,

author={Abel, Andreas and Coquand, Thierry and Dybjer, Peter},

title={Verifying a semantic βη-conversion test for martin-löf type theory},

booktitle={9th International Conference on Mathematics of Program Construction, MPC 2008; Marseille; France; 15 July 2008 through 18 July 2008},

isbn={978-354070593-2},

pages={29-56},

abstract={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.},

year={2008},

}

** RefWorks **

RT Conference Proceedings

SR Print

ID 72936

A1 Abel, Andreas

A1 Coquand, Thierry

A1 Dybjer, Peter

T1 Verifying a semantic βη-conversion test for martin-löf type theory

YR 2008

T2 9th International Conference on Mathematics of Program Construction, MPC 2008; Marseille; France; 15 July 2008 through 18 July 2008

SN 978-354070593-2

SP 29

OP 56

AB 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.

LA eng

OL 30