Sökning: id:"swepub:oai:research.chalmers.se:78c90bb0-23ac-452f-bd55-29d3c4e0f90e" >
Verifying a semanti...
Verifying a semantic βη-conversion test for martin-löf type theory
-
- Abel, Andreas, 1974 (författare)
- Ludwig-Maximilians-Universität München,Ludwig Maximilian University of Munich
-
- Coquand, Thierry, 1961 (författare)
- Göteborgs universitet,University of Gothenburg
-
- Dybjer, Peter, 1953 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- ISBN 9783540705932
- Berlin, Heidelberg : Springer Berlin Heidelberg, 2008
- 2008
- Engelska.
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783540705932 ; 5133 LNCS, s. 29-56
- Relaterad länk:
-
http://www.tcs.ifi.l...
-
visa fler...
-
https://doi.org/10.1...
-
https://research.cha...
-
visa färre...
Innehållsförteckning
Abstract
Ämnesord
Stäng
No table of content available
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas