Sciweavers

PADL
2010
Springer
14 years 16 days 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 reusin...
Mathieu Boespflug