Conversion by Evaluation

10 years 10 months ago
Conversion by Evaluation
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.
Mathieu Boespflug
Added 17 Mar 2010
Updated 17 Mar 2010
Type Conference
Year 2010
Where PADL
Authors Mathieu Boespflug
Comments (0)