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.