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

https://hal.inria.fr/inria-00434282
Contributor : Mathieu Boespflug <>
Submitted on : Monday, December 21, 2009 - 7:00:11 AM
Last modification on : Thursday, March 5, 2020 - 6:22:04 PM
Long-term archiving on: : Tuesday, October 16, 2012 - 2:40:35 PM

File

derivesn.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨inria-00434282⟩

Share

Metrics

Record views

310

Files downloads

188