A collection of resources about normalization-by-evaluation

Normalization-by-evaluation ("NbE" for short) is an elegant technique for computing normal forms of object language terms. It consists of only two parts: evaluation (reflection, denotation), which maps syntactic terms to the semantic domain, and quotation (read-back, reification), which maps values from the semantic domain back to terms. The composition of evaluation followed by quotation is called normalization. One classical example of normalization-by-evaluation is computing β-normal forms of lambda calculus terms, optionally enriched with additional constructions. Alongside with bidirectional type checking, normalization-by-evaluation is considered traditional in the implementation of dependently typed programming languages & proof assistants based on type theory.

This is a collection of resources for studying normalization-by-evaluation & its applications, ranging from introductory materials to advanced papers. Any questions regarding NbE will be welcomed in the issues.

• AndrasKovacs/elaboration-zoo -- Minimal implementations for dependent type checking and elaboration.
• nguermond/normalization-by-evaluation -- Various implementations of normalization-by-evaluation.
• jozefg/nbe-for-mltt -- Normalization-by-evaluation for Martin-Löf Type Theory.
• AndrasKovacs/sysF-NbE -- Normalization-by-evaluation for intrinsic System F.
• nachivpn/nbe-edsl -- Normalization-by-evaluation for embedded domain-specific languages.
• examples/benchmarks/other/nbe.effekt -- Normalization-by-evaluation for the lambda calculus in Effekt.
• AndrasKovacs/FixNf.hs -- A minimal environment machine normalization with a fixpoint operator.
• src/Core/Normalise/Eval.idr, Quote.idr -- Normalization-by-evaluation for Idris2.
• webyrd/normalization-by-evaluation -- Normalization-by-evaluation for miniKanren.

• "A Brief Introduction to Normalization-By-Evaluation" by Louis F. Ashfield.
• "Checking Dependent Types with Normalization by Evaluation: A Tutorial" by David Thrane Christiansen.
  • Haskell version
• "Normalization by Evaluation Four Ways: Reconstructing NbE Designs from First Principles" by William J. Bowman.
• "Elementary Tutorial on Normalization-by-Evaluation" by Oleg Kiselyov.
• "Evaluators, Normalizers, Reducers: from denotational to operational semantics" by Oleg Kiselyov.

• Berger, Ulrich, and Helmut Schwichtenberg. "An inverse of the evaluation functional for typed lambda-calculus." (1991): 203-211.
  URL, webarchive

• Danvy, Olivier. "Type-directed partial evaluation." Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. 1996.
  URL

• Coquand, Thierry, and Peter Dybjer. "Intuitionistic model constructions and normalization proofs." Mathematical Structures in Computer Science 7.1 (1997): 75-94.
  URL, webarchive

• Filinski, Andrzej. "A semantic account of type-directed partial evaluation." International Conference on Principles and Practice of Declarative Programming. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999.
  URL, webarchive

• Altenkirch, Thorsten, et al. "Normalization by evaluation for typed lambda calculus with coproducts." Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. IEEE, 2001.
  URL, webarchive
• Danvy, Olivier, Morten Rhiger, and Kristoffer H. Rose. "Normalization by evaluation with typed abstract syntax." Journal of Functional Programming 11.6 (2001): 673-680.
  URL, webarhive

• Filinski, Andrzej, and Henning Korsholm Rohde. "Denotational aspects of untyped normalization by evaluation." RAIRO-Theoretical Informatics and Applications 39.3 (2005): 423-453.
  URL, webarchive

• Abel, Andreas, Klaus Aehlig, and Peter Dybjer. "Normalization by evaluation for Martin-Löf type theory with one universe." Electronic Notes in Theoretical Computer Science 173 (2007): 17-39.
  URL, webarchive
• Abel, Andreas, Thierry Coquand, and Peter Dybjer. "Normalization by evaluation for Martin-Löf Type Theory with typed equality judgements." 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007). IEEE, 2007.
  URL, webarchive

• Boespflug, Mathieu. "Efficient normalization by evaluation." 2009 Workshop on Normalization by Evaluation. 2009.
  URL, webarchive
• Coquand, Thierry, et al. “A Simple Type-Theoretic Language: Mini-TT.” From Semantics to Computer Science: Essays in Honour of Gilles Kahn. Ed. Yves Bertot, et al. Cambridge: Cambridge University Press, 2009. 139–164. Print.
  URL

• Mendel-Gleason, Gavin E., and Geoff W. Hamilton. "Supercompilation and normalisation by evaluation." (2010).
  URL, webarchive

• Abel, Andreas. "Normalization by evaluation: Dependent types and impredicativity." Habilitation. Ludwig-Maximilians-Universität München (2013).
  URL, webarchive
• Ahman, Danel, and Sam Staton. "Normalization by evaluation and algebraic effects." Electronic Notes in Theoretical Computer Science 298 (2013): 51-69.
  URL, webarchive

• Danvy, Olivier, Chantal Keller, and Matthias Puech. "Typeful normalization by evaluation." 20th International Conference on Types for Proofs and Programs, TYPES 2014. 2014.
  URL, webarchive

• Abel, Andreas, Andrea Vezzosi, and Theo Winterhalter. "Normalization by evaluation for sized dependent types." Proceedings of the ACM on Programming Languages 1.ICFP (2017): 1-30.
  URL, webarchive

• Gratzer, Daniel, Jonathan Sterling, and Lars Birkedal. "Implementing a modal dependent type theory." Proceedings of the ACM on Programming Languages 3.ICFP (2019): 1-29.
  URL, webarchive

• Valliappan, Nachiappan, Alejandro Russo, and Sam Lindley. "Practical normalization by evaluation for EDSLs." Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell. 2021.
  URL, webarchive

• Biernacka, Małgorzata, Witold Charatonik, and Tomasz Drab. "A simple and efficient implementation of strong call by need by an abstract machine." Proceedings of the ACM on Programming Languages 6.ICFP (2022): 109-136.
  URL