Normalization by Evaluation. Andreas Abel.
Abstract: In computer systems that manipulate syntactic objects, like computeralgebra systems, compilers, and theorem provers, we find algorithms that check whether two expressions are equal. Some expression classes admit normal forms. For objects of these classes, equality can be decided by checking that the expressions under consideration have the same normal form. Conversion to normal form is called normalization.
In this talk, I show how normalizers can be obtained from interpreters in a principled and elegant way. The process of normalizing an expression via an interpreter is called normalization by evaluation. I will demonstrate normalization by evaluation for two structures: monoids and lambda-calculus.
Normalization by evaluation is applied in type-directed partial evaluation of functional programs, in implementation of proofassistants, and in foundational studies of Type Theory.
Universidad EAFIT. Marzo 9 de 2017