Gyesik Lee ; Benjamin Werner - Proof-irrelevant model of CC with predicative induction and judgmental equality

lmcs:920 - Logical Methods in Computer Science, November 23, 2011, Volume 7, Issue 4 - https://doi.org/10.2168/LMCS-7(4:5)2011
Proof-irrelevant model of CC with predicative induction and judgmental equalityArticle

Authors: Gyesik Lee ; Benjamin Werner

    We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axiom for countably many inaccessible cardinals. We use Aczel's trace encoding which is universally defined for any function type, regardless of being impredicative. Direct and concrete interpretations of simultaneous induction and mutually recursive functions are also provided by extending Dybjer's interpretations on the basis of Aczel's rule sets. Our model can be regarded as a higher-order generalization of the truth-table methods. We provide a relatively simple consistency proof of type theory, which can be used as the basis for a theorem prover.


    Volume: Volume 7, Issue 4
    Published on: November 23, 2011
    Imported on: March 31, 2010
    Keywords: Computer Science - Logic in Computer Science,F.4.1, F.3.1

    2 Documents citing this article

    Consultation statistics

    This page has been seen 1727 times.
    This article's PDF has been downloaded 326 times.