Andreas Abel, On Irrelevance in Type Theory
TCS Oberseminar, 17.12.2010, 14:15
Andreas Abel, On Irrelevance in Type Theory
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, I have extended Pfenning's type theory with irrelevant quantification, that models a distinction between static and dynamic code, to universes and recursive type functions. This theory serves as the basis for proof irrelevance in Agda.
Artikelaktionen
abgelegt unter:
Oberseminar