Lee, Gyesik and Werner, Benjamin - 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
Proof-irrelevant model of CC with predicative induction and judgmental equality

Authors: Lee, Gyesik and Werner, Benjamin

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.


Source : oai:arXiv.org:1111.0123
DOI : 10.2168/LMCS-7(4:5)2011
Volume: Volume 7, Issue 4
Published on: November 23, 2011
Submitted on: March 31, 2010
Keywords: Computer Science - Logic in Computer Science,F.4.1, F.3.1


Share

Consultation statistics

This page has been seen 88 times.
This article's PDF has been downloaded 18 times.