Skip to main content

Research Repository

Advanced Search

Normalisation by evaluation for dependent types

Altenkirch, Thorsten; Kaposi, Ambrus

Normalisation by evaluation for dependent types Thumbnail


Authors

Ambrus Kaposi



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. (2016). Normalisation by evaluation for dependent types.

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 Mar 28, 2024
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.

Files





You might also like



Downloadable Citations