PLS Lab

Normalization by Evaluation

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:

References

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 https://github.com/jozefg/blott 
@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}
}

Implementations