11 maja 2017 10:00
Paweł Wieczorek: A Coq Formalization of Normalization-By-Evaluation for Martin-Löf Type Theory
Normalization by Evaluation (NbE) is a reduction-free normalization technique for lambda calculus, where a term is interpreted and evaluated in a sophisticated domain and then its normal form is read back from a computed value. The technique can be used as a decision procedure for term equality, which plays a key role in type-checkers for proof assistants such as Coq.
In this talk I would like to introduce audience to NbE for Dependent Type Theory and present the results of my master's thesis -- a Coq formalization and extraction of a normalization procedure for Martin-Löf type theory. In my work I take an unusual approach to program extraction where the theoretical results and the extraction-related part are highly decoupled. I believe such a path can be seen as a general way of dealing with program extraction.