Thorsten Altenkirch ; Ambrus Kaposi - Normalisation by Evaluation for Type Theory, in Type Theory

lmcs:2588 - Logical Methods in Computer Science, October 23, 2017, Volume 13, Issue 4 - https://doi.org/10.23638/LMCS-13(4:1)2017
Normalisation by Evaluation for Type Theory, in Type TheoryArticle

Authors: Thorsten Altenkirch ; Ambrus Kaposi

    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.


    Volume: Volume 13, Issue 4
    Published on: October 23, 2017
    Accepted on: September 3, 2017
    Submitted on: September 4, 2017
    Keywords: Computer Science - Logic in Computer Science,F.4.1
    Funding:
      Source : OpenAIRE Graph
    • Homotopy Type Theory: Programming and Verification; Funder: UK Research and Innovation; Code: EP/M016951/1

    3 Documents citing this article

    Consultation statistics

    This page has been seen 2161 times.
    This article's PDF has been downloaded 780 times.