CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

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

Andreas Abel ; Thierry Coquand ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
9th International Conference on Mathematics of Program Construction, MPC 2008; Marseille; France; 15 July 2008 through 18 July 2008 p. 29-56. (2008)
[Konferensbidrag, refereegranskat]

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.

Denna post skapades 2008-08-13. Senast ändrad 2017-12-06.
CPL Pubid: 72936


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU) (GU)
Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)


Teoretisk datalogi

Chalmers infrastruktur