Andreas Abel ; Gabriel Scherer - On Irrelevance and Algorithmic Equality in Predicative Type Theory

lmcs:1045 - Logical Methods in Computer Science, March 27, 2012, Volume 8, Issue 1 - https://doi.org/10.2168/LMCS-8(1:29)2012
On Irrelevance and Algorithmic Equality in Predicative Type Theory

Authors: Andreas Abel ; Gabriel Scherer

    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.


    Volume: Volume 8, Issue 1
    Published on: March 27, 2012
    Accepted on: June 25, 2015
    Submitted on: May 23, 2011
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.4.1

    Linked data

    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.types.2019.9
    • 10.4230/lipics.types.2019.9
    Is Impredicativity Implicitly Implicit?
    Monnier, Stefan ; Bos, Nathaniel ;

    19 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 780 times.
    This article's PDF has been downloaded 254 times.