Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.6
URN: urn:nbn:de:0030-drops-59727
URL: https://drops.dagstuhl.de/opus/volltexte/2016/5972/
Altenkirch, Thorsten ; Kaposi, Ambrus
Normalisation by Evaluation for Dependent Types
| pdf-format: |
|
Abstract
We develop normalisation by evaluation (NBE) for dependent types basedon 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.
BibTeX - Entry
@InProceedings{altenkirch_et_al:LIPIcs:2016:5972,
author = {Thorsten Altenkirch and Ambrus Kaposi},
title = {{Normalisation by Evaluation for Dependent Types}},
booktitle = {1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
pages = {6:1--6:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-010-1},
ISSN = {1868-8969},
year = {2016},
volume = {52},
editor = {Delia Kesner and Brigitte Pientka},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/5972},
URN = {urn:nbn:de:0030-drops-59727},
doi = {10.4230/LIPIcs.FSCD.2016.6},
annote = {Keywords: normalisation by evaluation, dependent types, internal type theory, logical relations, Agda}
}
| Keywords: | normalisation by evaluation, dependent types, internal type theory, logical relations, Agda | |
| Seminar: | 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) | |
| Issue date: | 2016 | |
| Date of publication: | 17.06.2016 |
