Skip to Main content Skip to Navigation
New interface
Conference papers

Efficient normalization by evaluation

Mathieu Boespflug 1, 2 
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
Abstract : Dependently typed theorem provers allow arbitrary terms in types. It is convenient to identify large classes of terms during type checking, hence many such systems provision some form of conversion rule. A standard algorithm for testing the convertibility of two types consists in normalizing them, then testing for syntactic equality of the normal forms. Normalization by evaluation is a standard technique enabling the use of existing compilers and runtimes for functional languages to implement normalizers, without peaking under the hood, for a fast yet cheap system in terms of implementation effort. Our focus is on performance of untyped normalization by evaluation. We demonstrate that with the aid of a standard optimization for higher order programs (namely uncurrying) and the reuse of pattern matching facilities of the evaluator for datatypes, we may obtain a normalizer that evaluates non-functional values about as fast as the underlying evaluator, but as an added benefit can also fully normalize functional values — or to put it another way, partially evaluates functions efficiently.
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Mathieu Boespflug Connect in order to contact the contributor
Submitted on : Saturday, November 21, 2009 - 6:18:04 PM
Last modification on : Friday, February 4, 2022 - 3:14:33 AM
Long-term archiving on: : Tuesday, October 16, 2012 - 2:40:42 PM


Publisher files allowed on an open archive


  • HAL Id : inria-00434283, version 1



Mathieu Boespflug. Efficient normalization by evaluation. 2009 Workshop on Normalization by Evaluation, Olivier Danvy, Aug 2009, Los Angeles, United States. ⟨inria-00434283⟩



Record views


Files downloads