Skip to main content

Research Repository

Advanced Search

Normalisation by evaluation for dependent types

Altenkirch, Thorsten; Kaposi, Ambrus

Authors

Ambrus Kaposi auk@Cs.Nott.AC.UK



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.

Publication Date Jun 26, 2016
Peer Reviewed Peer Reviewed
APA6 Citation Altenkirch, T., & Kaposi, A. (2016). Normalisation by evaluation for dependent types
Keywords Normalisation by evaluation, dependent types, internal type theory, logical relations, Agda
Publisher URL http://drops.dagstuhl.de/opus/volltexte/2016/5972/pdf/LIPIcs-FSCD-2016-6.pdf
Copyright Statement Copyright information regarding this work can be found at the following address: http://creativecommons.org/licenses/by/4.0
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

nbe-dep.pdf (511 Kb)
PDF

Copyright Statement
Copyright information regarding this work can be found at the following address: http://creativecommons.org/licenses/by/4.0





You might also like



Downloadable Citations

;