Links und Funktionen

Sie sind hier: Startseite / Lehre / WS 2010/11 / Oberseminar / Andreas Abel, On Irrelevance in Type Theory


Andreas Abel, On Irrelevance in Type Theory

TCS Oberseminar, 17.12.2010, 14:15
Wann 14:15 15:45 17.12.2010
von bis
Wo L109
Termin übernehmen vCal

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.


abgelegt unter: