Normalisation by evaluation for type theory, in type theory

Altenkirch, Thorsten; Kaposi, Ambrus

Abstract

© Altenkirch and Kaposi. 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.

Citation

Altenkirch, T., & Kaposi, A. (2017). Normalisation by evaluation for type theory, in type theory. Logical Methods in Computer Science, 13(4), https://doi.org/10.23638/LMCS-13%284%3A1%292017

• Journal Article Type: Article
• Acceptance Date: Sep 4, 2017
• Publication Date: Oct 23, 2017
• Deposit Date: Oct 30, 2017
• Publicly Available Date: Oct 30, 2017
• Journal: Logical Methods in Computer Science
• Print ISSN: 1860-5974
• Electronic ISSN: 1860-5974
• Publisher: Logical Methods in Computer Science
• Peer Reviewed: Peer Reviewed
• Volume: 13
• Issue: 4
• DOI: https://doi.org/10.23638/LMCS-13%284%3A1%292017
• Keywords: normalisation by evaluation; dependent types; internal type theory; logical relations; Agda
• Public URL: https://nottingham-repository.worktribe.com/output/888899
• Publisher URL: https://lmcs.episciences.org/4005
• Related Public URLs: https://lmcs.episciences.org/
• Contract Date: Oct 30, 2017