Conversion 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 : 2010

Conversion by Evaluation

Résumé

We show how testing convertibility of two types in dependently typed systems can advantageously be implemented instead untyped normalization by evaluation, thereby reusing existing compilers and runtime environments for stock functional languages, without peeking 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), the reuse of native datatypes and pattern matching facilities of the underlying evaluator, we may obtain a normalizer with little to no performance overhead compared to a regular evaluator.
Fichier principal
Vignette du fichier
derivesn.pdf (165.27 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00434282 , version 1 (21-12-2009)

Identifiants

  • HAL Id : inria-00434282 , version 1

Citer

Mathieu Boespflug. Conversion by Evaluation. Twelfth International Symposium on Practical Aspects of Declarative Languages, Jan 2010, Madrid, Spain. ⟨inria-00434282⟩
139 Consultations
127 Téléchargements

Partager

Gmail Facebook X LinkedIn More