Efficient normalization by evaluation - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2009

Efficient normalization by evaluation

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.
Fichier principal
Vignette du fichier
NBE09-Boespflug-fastnbe.pdf (113.6 Ko) Télécharger le fichier
Origin : Publisher files allowed on an open archive
Loading...

Dates and versions

inria-00434283 , version 1 (21-11-2009)

Identifiers

  • HAL Id : inria-00434283 , version 1

Cite

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

Share

Gmail Facebook X LinkedIn More