14th Estonian Winter School in Computer Science (EWSCS)
XIV Eesti Arvutiteaduse Talvekool

Palmse, Estonia, March 1-6, 2009

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

Valid CSS! Valid XHTML 1.0 Strict 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/