@article{Filinski_Rohde_2003, title={A Denotational Account of Untyped Normalization by Evaluation}, volume={10}, url={https://tidsskrift.dk/brics/article/view/21808}, DOI={10.7146/brics.v10i40.21808}, abstractNote={We show that the standard normalization-by-evaluation construction for the simply-typed lambda_{beta eta}-calculus has a natural counterpart for the untyped lambda_beta-calculus, with the central type-indexed logical relation replaced by a "recursively definedâ€™â€™ <em>invariant relation</em>, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.<br /> <br />In the untyped setting, not all terms have normal forms, so the normalization function is necessarily partial. We establish its correctness in the senses of <em>soundness</em> (the output term, if any, is beta-equivalent to the input term); <em>standardization</em> ( beta-equivalent terms are mapped to the same result); and <em>completeness</em> (the function is defined for all terms that do have normal forms). We also show how the semantic construction enables a simple yet formal correctness proof for the normalization algorithm, expressed as a functional program in an ML-like call-by-value language.}, number={40}, journal={BRICS Report Series}, author={Filinski, Andrzej and Rohde, Henning Korsholm}, year={2003}, month={Dec.} }