Normalisation by evaluation for dependent types

Altenkirch, Thorsten; Kaposi, Ambrus

Abstract

We develop normalisation by evaluation (NBE) for dependent types based on presheaf categories. Our construction is formulated using internal type theory using quotient inductive types. We use a typed presentation hence there are no preterms or realizers in our construction. NBE for simple types is using 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 have formalized parts of the construction in Agda.

Citation

Altenkirch, T., & Kaposi, A. Normalisation by evaluation for dependent types. Presented at FSCD 2016: 1st International Conference on Formal Structures for Computation and Deduction

• Conference Name: FSCD 2016: 1st International Conference on Formal Structures for Computation and Deduction
• End Date: Jun 26, 2016
• Acceptance Date: Apr 6, 2016
• Publication Date: Jun 26, 2016
• Deposit Date: Jun 22, 2016
• Publicly Available Date: Jun 26, 2016
• Peer Reviewed: Peer Reviewed
• Keywords: Normalisation by evaluation, dependent types, internal type theory, logical relations, Agda
• Public URL: https://nottingham-repository.worktribe.com/output/793447
• Publisher URL: http://drops.dagstuhl.de/opus/volltexte/2016/5972/pdf/LIPIcs-FSCD-2016-6.pdf
• Additional Information: Published in: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)/; editors Delia Kesner and Brigitte Pientka, article No. 6, p. 6:1–6:16.
• Contract Date: Jun 22, 2016