sem2009/abstracts/abel

Normalization by Evaluation for Dependent Type Theory (Work in Progress)

Andreas Abel (LMU, Munich)

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. Currently Coq supports normalization through computational rules (beta-delta-iota), eta equality is not supported. In this talk, 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.