THORSTEN ALTENKIRCH THORSTEN.ALTENKIRCH@NOTTINGHAM.AC.UK
Professor of Computer Science
Normalisation by evaluation for dependent types
Altenkirch, Thorsten; Kaposi, Ambrus
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
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
Should Type Theory Replace Set Theory as the Foundation of Mathematics?
(2023)
Journal Article
Constructing a universe for the setoid model
(2021)
Conference Proceeding
Big Step Normalisation for Type Theory
(2020)
Journal Article
Naive Type Theory
(2019)
Book Chapter
Towards a cubical type theory without an interval
(2018)
Journal Article
Downloadable Citations
About Repository@Nottingham
Administrator e-mail: digital-library-support@nottingham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2024
Advanced Search