Paper Info
Title
Normalisation by Evaluation for Type Theory, in Type Theory.
Abstract
We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated in the metalanguage of type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction, and every construction respects the conversion relation. NBE for simple types uses a logical relation between the syntax and the presheaf interpretation. In our construction, we merge the presheaf interpretation and the logical relation into a proof-relevant logical predicate. We prove normalisation, completeness, stability and decidability of definitional equality. Most of the constructions were formalized in Agda.
Year
DOI
Venue
2017
10.23638/LMCS-13(4:1)2017
LOGICAL METHODS IN COMPUTER SCIENCE
Keywords
DocType
Volume
normalisation by evaluation,dependent types,internal type theory,logical relations,Agda
Journal
13
Issue
ISSN
Citations 
4
1860-5974
0
PageRank 
References 
Authors
0.34
0
2
Name
Order
Citations
PageRank
Thorsten Altenkirch166856.85
Ambrus Kaposi2164.29