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, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
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.
Type de document :
Communication dans un congrès
Olivier Danvy. 2009 Workshop on Normalization by Evaluation, Aug 2009, Los Angeles, United States. 2009, 〈http://www.brics.dk/~danvy/NBE09/informal-proceedings/〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

Contributeur : Mathieu Boespflug <>
Soumis le : samedi 21 novembre 2009 - 18:18:04
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : mardi 16 octobre 2012 - 14:40:42


Fichiers éditeurs autorisés sur une archive ouverte


  • HAL Id : inria-00434283, version 1



Mathieu Boespflug. Efficient normalization by evaluation. Olivier Danvy. 2009 Workshop on Normalization by Evaluation, Aug 2009, Los Angeles, United States. 2009, 〈http://www.brics.dk/~danvy/NBE09/informal-proceedings/〉. 〈inria-00434283〉



Consultations de la notice


Téléchargements de fichiers