Sciweavers

Share
FOSSACS
2011
Springer

Irrelevance in Type Theory with a Heterogeneous Equality Judgement

8 years 5 months ago
Irrelevance in Type Theory with a Heterogeneous Equality Judgement
Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To obtain reasonable performance of not only the compiled program but also the type checker such static terms need to be erased as early as possible, preferably immediately after type checking. To this end, Pfenning’s type theory with irrelevant quantification, that models a distinction between static and dynamic code, is extended to universes and large eliminations. Novel is a heterogeneously typed implementation of equality which allows the smooth construction of a universal Kripke model that proves normalization, consistency and decidability.
Andreas Abel
Added 28 Aug 2011
Updated 28 Aug 2011
Type Journal
Year 2011
Where FOSSACS
Authors Andreas Abel
Comments (0)
books