Peter Dybjer
Dept. of Computer Science and Engineering
Chalmers University of Technology and Gothenburg University
Sweden
Normalization by Evaluation
Abstract
Normalization by evaluation (nbe) is a new method for writing normalization algorithms. The idea is to first build a data structure which represents a model of the language in question. Then terms are interpreted in this model, and finally the normal forms are extracted from the semantic values. The method has both practical and theoretical interest. It has been used for program simplification (type-directed partial evaluation) and in type-checking algorithms for proof assistants based on type theory. Ideas from several fields in theoretical computer science are useful for analyzing the method, such as constructive type theory and program extraction, category theory, and domain theory. These lectures will both give an introduction to the technique and discuss some of these connections. Nbe-algorithms can often be programmed nicely in a functional programming language with dependent types. To this end we will use the Agda language which is based on Martin-Löf's intuitionistic type theory and developed in Gothenburg. We will introduce this language and explain how it can be used to give very informative types to programs as well as to formally prove correctness properties.
Course materials
- P. Dybjer. Normalization by evaluation. Lecture slides for EWSCS 2009. 2009. [pdf]
- Accompanying Agda code:
- Introduction: Power.agda, Product.agda
- Monoids: Exp.agda, Nbe.agda, Laws.agda, Pentagon.agda, NbeComplete.agda, NbeSound.agda
- Combinators: Exp.agda, Sem.agda, Lam*.agda, Nbe.agda
- P. Dybjer, A. Filinski. Normalization and partial evaluation. In G. Barthe, P. Dybjer, L. Pinto, J. Saraiva, eds., Advanced Lectures from Int. Summer School on Applied Semantics, APPSEM 2000 (Caminha, Sept. 2000), v. 2395 of Lect. Notes in Comput. Sci., pp. 137-192. Springer, 2002. Sections 1-3.
- P. Dybjer, A. Bove. Dependent types at work. Lecture notes for Int. Summer School on Language Engineering and Rigorous Software Development, LERNET 2008 (Piriapolis, Feb./March 2008). 2008.
- P. Dybjer, D. Kuperberg. Formal neighbourhoods, combinatory Böhm trees, and normalization by evaluation. 2008.
Last changed
March 6, 2009 16:11 EET
by
local organizers, ewscs09(at)cs.ioc.ee
EWSCS'09 page:
http://cs.ioc.ee/ewscs/2009/