On Irrelevance and Algorithmic Equality in Predicative Type Theory

TL;DR

This paper extends Pfenning's type theory with irrelevant quantification to include universes and large eliminations, establishing its meta-theory and a complete, type-directed equality algorithm.

Contribution

It introduces an extension of Pfenning's theory with universes and large eliminations, along with a meta-theoretical foundation and a complete equality algorithm.

Findings

Subject reduction, normalization, and consistency proven via Kripke model.

Meta-theory extended to universes and large eliminations.

A complete, type-directed equality algorithm developed.

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.