Conversion by Evaluation

Mathieu Boespflug 1, 2, *
* Auteur correspondant
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Type de document :
Communication dans un congrès
Twelfth International Symposium on Practical Aspects of Declarative Languages, Jan 2010, Madrid, Spain. 2010
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00434282
Contributeur : Mathieu Boespflug <>
Soumis le : lundi 21 décembre 2009 - 07:00:11
Dernière modification le : jeudi 10 mai 2018 - 02:06:47
Document(s) archivé(s) le : mardi 16 octobre 2012 - 14:40:35

Fichier

derivesn.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00434282, version 1

Collections

Citation

Mathieu Boespflug. Conversion by Evaluation. Twelfth International Symposium on Practical Aspects of Declarative Languages, Jan 2010, Madrid, Spain. 2010. 〈inria-00434282〉

Partager

Métriques

Consultations de la notice

257

Téléchargements de fichiers

111