Skip to main content

Research Repository

See what's under the surface

Advanced Search

Normalisation by evaluation for type theory, in type theory

Altenkirch, Thorsten; Kaposi, Ambrus

Authors

Thorsten Altenkirch txa@cs.nott.ac.uk

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 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.

Journal Article Type Article
Publication Date Oct 23, 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:1
APA6 Citation Altenkirch, T., & Kaposi, A. (2017). Normalisation by evaluation for type theory, in type theory. Logical Methods in Computer Science, 13(4:1), doi:10.23638/LMCS-13(4:1)2017
DOI https://doi.org/10.23638/LMCS-13%284%3A1%292017
Keywords normalisation by evaluation; dependent types; internal type theory; logical relations; Agda
Publisher URL https://lmcs.episciences.org/4005
Related Public URLs https://lmcs.episciences.org/
Copyright Statement Copyright information regarding this work can be found at the following address: http://creativecommons.org/licenses/by-nd/4.0

Files

1612.02462.pdf (417 Kb)
PDF

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





You might also like



Downloadable Citations

;