Normalization by Evaluation (NbE) is a technique for normalizing the terms of a language, calculus, or type theory.
In NbE, a term is first evaluated in some 'semantic' model of language. The resulting value is reified back into a term. This gives a practical method for deciding definitional equality even in complicated dependent type theories, where rewriting becomes prohibitively complicated.
Normalization by evaluation has been formulated for the following systems:
Christiansen, David Raymond. ‘Checking Dependent Types with Normalization by Evaluation: A Tutorial’. Tutorial, 2018. http://davidchristiansen.dk/tutorials/nbe/.
Christiansen, David Raymond. ‘Checking Dependent Types with Normalization by Evaluation: A Tutorial (Haskell Version)’. 21 May 2019. http://davidchristiansen.dk/tutorials/implementing-types-hs.pdf.
Abel, Andreas. 2013. ‘Normalization by Evaluation: Dependent Types and Impredicativity’. Habilitation thesis, Ludwig-Maximilians-Universität München. http://www.cse.chalmers.se/~abela/habil.pdf.
@phdthesis{abel_2013,
type = {Habilitation thesis},
title = {Normalization by {Evaluation}: {Dependent} {Types} and {Impredicativity}},
url = {http://www.cse.chalmers.se/~abela/habil.pdf},
school = {Ludwig-Maximilians-Universität München},
author = {Abel, Andreas},
year = {2013}
}
Berger, U., and H. Schwichtenberg. 1991. ‘An Inverse of the Evaluation Functional for Typed Lambda-Calculus’. In Proceedings of the 6th Annual IEEE Symposium on Logic in Computer Science, 203–11. IEEE. https://doi.org/10.1109/LICS.1991.151645.
@inproceedings{berger_1991,
title = {An inverse of the evaluation functional for typed lambda-calculus},
doi = {10.1109/LICS.1991.151645},
booktitle = {Proceedings of the 6th {Annual} {IEEE} {Symposium} on {Logic} in {Computer} {Science}},
publisher = {IEEE},
author = {Berger, U. and Schwichtenberg, H.},
year = {1991},
pages = {203--211}
}
Filinski, Andrzej, and Henning Korsholm Rohde. 2004. ‘A Denotational Account of Untyped Normalization by Evaluation’. In Foundations of Software Science and Computation Structures, edited by Igor Walukiewicz, 2987:167–81. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-24727-2_13.
@inproceedings{filinski_2004,
address = {Berlin, Heidelberg},
series = {Lecture {Notes} in {Computer} {Science}},
title = {A {Denotational} {Account} of {Untyped} {Normalization} by {Evaluation}},
volume = {2987},
doi = {10.1007/978-3-540-24727-2_13},
booktitle = {Foundations of {Software} {Science} and {Computation} {Structures}},
publisher = {Springer Berlin Heidelberg},
author = {Filinski, Andrzej and Rohde, Henning Korsholm},
editor = {Walukiewicz, Igor},
year = {2004},
pages = {167--181}
}
Altenkirch, Thorsten, and Ambrus Kaposi. 2016. ‘Normalisation by Evaluation for Dependent Types’. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), edited by Delia Kesner and Brigitte Pientka, 52:6:1-6:16. Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl, Germany: Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.FSCD.2016.6.
@inproceedings{altenkirch_normalisation_2016,
address = {Dagstuhl, Germany},
series = {Leibniz {International} {Proceedings} in {Informatics} ({LIPIcs})},
title = {Normalisation by {Evaluation} for {Dependent} {Types}},
volume = {52},
isbn = {978-3-95977-010-1},
url = {http://drops.dagstuhl.de/opus/volltexte/2016/5972},
doi = {10.4230/LIPIcs.FSCD.2016.6},
booktitle = {1st {International} {Conference} on {Formal} {Structures} for {Computation} and {Deduction} ({FSCD} 2016)},
publisher = {Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik},
author = {Altenkirch, Thorsten and Kaposi, Ambrus},
editor = {Kesner, Delia and Pientka, Brigitte},
year = {2016},
pages = {6:1--6:16}
}
Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. 2019. Implementing a modal dependent type theory. Proc. ACM Program. Lang. 3, ICFP, Article 107 (August 2019), 29 pages. DOI:https://doi.org/10.1145/3341711
@article{10.1145/3341711,
author = {Gratzer, Daniel and Sterling, Jonathan and Birkedal, Lars},
title = {Implementing a Modal Dependent Type Theory},
year = {2019},
issue_date = {August 2019},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {3},
number = {ICFP},
url = {https://doi.org/10.1145/3341711},
doi = {10.1145/3341711},
articleno = {107},
numpages = {29}
}
Fredriksson, Olle. ‘Dependent type checker using normalisation by evaluation’. 16 January 2021. https://github.com/ollef/sixty
Kovács, András. ‘Demo for high-performance type theory elaboration’. 2019. https://github.com/AndrasKovacs/smalltt
Kovács, András. ‘Non-deterministic normalization-by-evaluation in Olle Fredriksson's flavor’. 21 Nov 2020. https://gist.github.com/AndrasKovacs/a0e0938113b193d6b9c1c0620d853784
Sterling, Jon. ‘A pedagogic implementation of abstract bidirectional elaboration for dependent type theory’. 18 Oct 2020. https://github.com/jonsterling/dreamtt
RedPRL Development Team. ‘A cool implementation of normalization by evaluation (nbe) & elaboration for Cartesian cubical type theory’. 25 Aug 2020. https://github.com/RedPRL/cooltt