Normalization by Evaluation (NbE) is an abstract framework for computing the full normal form of lambda-terms through an interpreter, just-in-time compiler or an abstract machine. While computational equality such as beta is part of every dependent type theory, the status of extensional laws such as eta is less clear. The reason is that eta needs a typed equality but many type theories (like Pure Type Systems) are formulated with untyped equality in order to decide equality by rewriting.
In this talk, I am arguing that NbE is the tool of choice to implement typed beta-eta equality for dependent type theory. I present typed NbE which computes eta-long normal forms, and show how to construct a model of (possibly impredicative) type theory that proves the correctness of NbE. Hence, NbE can be used to decide the built-in (``definitional'') equality of type theory with eta-rules.
The aim of this work is to provide foundational justifications of powerful type theories with beta-eta equality, such as the Calculus of Inductive Constructions.