Normalisation by Evaluation

  • Klaus T. Aehlig | University of Munich

Normalisation by Evaluation is a technique to efficiently compute the normal form of, possibly open, lambda terms with respect to beta reduction and rewrite rules. It works by compiling terms into some functional programming language and reading off a term representation from the evaluated program. It has been implemented in the theorem prover Isabelle, and a detailed model has been formally verified. The talk will explain the technique and details of the implementation and verification.

Speaker Details

Klaus Aehlig studied mathematics and computer science, specialising in Mathematical Logic. He received both, his Master in 2000 (with a thesis on Implicit Computational Complexity), and his PhD in 2003 (with a thesis on Proof Theory) from the University of Munich. As a postdoc, he has been working at the Computer Science departments in Oxford, Toronto and Swansea. Currently, he has a teaching and research position at the University of Munich. His main area of research is the lambda calculus, where he mainly focuses on operational aspects (continuous normalisation, normalisation by evaluation), but he is also interested in questions of complexity and decidability (for certain, e.g., typed, fragments). Besides that, he is working in proof theory and proof complexity.

Watch Next