2026-07-22T18:45:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5972 2024-03-06T10:37:24Z ddc:004 open_access

Normalisation by Evaluation for Dependent Types Altenkirch, Thorsten Kaposi, Ambrus normalisation by evaluation dependent types internal type theory logical relations Agda 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thorsten Altenkirch and Ambrus Kaposi 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.6 urn:nbn:de:0030-drops-59727 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.6 eng https://creativecommons.org/licenses/by/3.0/legalcode