Skip to Main content Skip to Navigation
Conference papers

Conversion by Evaluation

Mathieu Boespflug 1, 2, * 
* Corresponding author
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France
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.
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Mathieu Boespflug Connect in order to contact the contributor
Submitted on : Monday, December 21, 2009 - 7:00:11 AM
Last modification on : Friday, February 4, 2022 - 3:17:24 AM
Long-term archiving on: : Tuesday, October 16, 2012 - 2:40:35 PM


Files produced by the author(s)


  • HAL Id : inria-00434282, version 1



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



Record views


Files downloads