{"docId":4005,"paperId":2588,"url":"https:\/\/lmcs.episciences.org\/2588","doi":"10.23638\/LMCS-13(4:1)2017","journalName":"Logical Methods in Computer Science","issn":"","eissn":"1860-5974","volume":[{"vid":315,"name":"Volume 13, Issue 4"}],"section":[],"repositoryName":"arXiv","repositoryIdentifier":"1612.02462","repositoryVersion":4,"repositoryLink":"https:\/\/arxiv.org\/abs\/1612.02462v4","dateSubmitted":"2017-09-04 22:50:20","dateAccepted":"2017-10-23 21:00:10","datePublished":"2017-10-23 21:01:42","titles":["Normalisation by Evaluation for Type Theory, in Type Theory"],"authors":["Altenkirch, Thorsten","Kaposi, Ambrus"],"abstracts":["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."],"keywords":["Computer Science - Logic in Computer Science","F.4.1"]}