Efficient normalization by evaluation - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2009

Efficient normalization by evaluation

Résumé

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
Origine : Fichiers éditeurs autorisés sur une archive ouverte
Loading...

Dates et versions

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

Identifiants

  • HAL Id : inria-00434283 , version 1

Citer

Mathieu Boespflug. Efficient normalization by evaluation. 2009 Workshop on Normalization by Evaluation, Olivier Danvy, Aug 2009, Los Angeles, United States. ⟨inria-00434283⟩
134 Consultations
690 Téléchargements

Partager

Gmail Facebook X LinkedIn More