some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

SPECIAL ISSUES

   Recent

   In Progress

   Archive

   Proposal

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

SPECIAL ISSUE:
Special Issue: Types for Proofs and Programs, 2010



On Irrelevance and Algorithmic Equality in Predicative Type Theory

©Andreas Abel, Department of Computer Science, Ludwig-Maximilians-University Munich
©Gabriel Scherer, Department of Computer Science, Ludwig-Maximilians-University Munich

Abstract
Dependently typed programs contain an excessive amount of static terms which are necessary to please the type checker but irrelevant for computation. To separate static and dynamic code, several static analyses and type systems have been put forward. We consider Pfenning's type theory with irrelevant quantification which is compatible with a type-based notion of equality that respects eta-laws. We extend Pfenning's theory to universes and large eliminations and develop its meta-theory. Subject reduction, normalization and consistency are obtained by a Kripke model over the typed equality judgement. Finally, a type-directed equality algorithm is described whose completeness is proven by a second Kripke model.

Publication date: March 27, 2012

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-8(1:29)2012

Hit Counts: 5965

Creative Commons