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.
@InProceedings{altenkirch_et_al:LIPIcs.FSCD.2016.6, author = {Altenkirch, Thorsten and Kaposi, Ambrus}, 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 = {Kesner, Delia and Pientka, Brigitte}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.6}, 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} }
Feedback for Dagstuhl Publishing