Document Open Access Logo

Normalisation by Evaluation for Dependent Types

Authors Thorsten Altenkirch, Ambrus Kaposi

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2016.6.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Subject Classification

Keywords
  • normalisation by evaluation
  • dependent types
  • internal type theory
  • logical relations
  • Agda

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Thorsten Altenkirch and Ambrus Kaposi. Normalisation by Evaluation for Dependent Types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.6

Author Details

Thorsten Altenkirch
Ambrus Kaposi

References

  1. Andreas Abel. Towards normalization by evaluation for the βη-calculus of constructions. In Functional and Logic Programming, pages 224-239. Springer, 2010. Google Scholar
  2. Andreas Abel. Normalization by Evaluation: Dependent Types and Impredicativity. PhD thesis, Habilitation, Ludwig-Maximilians-Universität München, 2013. Google Scholar
  3. Andreas Abel, Thierry Coquand, and Peter Dybjer. Normalization by evaluation for Martin-Löf type theory with typed equality judgements. In Logic in Computer Science, 2007. LICS 2007. 22nd Annual IEEE Symposium on, pages 3-12. IEEE, 2007. Google Scholar
  4. The Agda Wiki, 2015. Available online. Google Scholar
  5. Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Phil Scott. Normalization by evaluation for typed lambda calculus with coproducts. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 303-310, 2001. Google Scholar
  6. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Categorical reconstruction of a reduction free normalization proof. In David Pitt, David E. Rydeheard, and Peter Johnstone, editors, Category Theory and Computer Science, LNCS 953, pages 182-199, 1995. Google Scholar
  7. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for a polymorphic system. In 11th Annual IEEE Symposium on Logic in Computer Science, pages 98-106, 1996. Google Scholar
  8. Thorsten Altenkirch, Martin Hofmann, and Thomas Streicher. Reduction-free normalisation for system F. Manuscript, 1997. URL: http://www.cs.nott.ac.uk/~txa/publ/f97.pdf.
  9. Thorsten Altenkirch and Ambrus Kaposi. Agda formalisation for the paper Normalisation by Evaluation for Dependent Types, 2016. Available online at the second author’s website. Google Scholar
  10. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pages 18-29, New York, NY, USA, 2016. ACM. URL: http://dx.doi.org/10.1145/2837614.2837638.
  11. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed λ-calculus. In Logic in Computer Science, 1991. LICS'91., Proceedings of Sixth Annual IEEE Symposium on, pages 203-211. IEEE, 1991. Google Scholar
  12. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical type theory: a constructive interpretation of the univalence axiom. Manuscript, December 2015. Google Scholar
  13. Nils Anders Danielsson. A formalisation of a dependently typed language as an inductive-recursive family. In Types for Proofs and Programs, pages 93-109. Springer, 2006. Google Scholar
  14. Olivier Danvy. Type-directed partial evaluation. Springer, 1999. Google Scholar
  15. Peter Dybjer. Internal type theory. In Types for Proofs and Programs, pages 120-134. Springer, 1996. Google Scholar
  16. Martin Hofmann. Syntax and semantics of dependent types. In Extensional Constructs in Intensional Type Theory, pages 13-54. Springer, 1997. Google Scholar
  17. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Chalmers University of Technology, 2007. Google Scholar
  18. Steven Schäfer, Gert Smolka, and Tobias Tebbi. Completeness and decidability of de Bruijn substitution algebra in Coq. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 67-73. ACM, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact