{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,26]],"date-time":"2026-09-26T12:30:16Z","timestamp":1790425816484,"version":"4.1.0"},"reference-count":26,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,11,23]],"date-time":"2011-11-23T00:00:00Z","timestamp":1322006400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a set-theoretic, proof-irrelevant model for Calculus of\nConstructions (CC) with predicative induction and judgmental equality in\nZermelo-Fraenkel set theory with an axiom for countably many inaccessible\ncardinals. We use Aczel's trace encoding which is universally defined for any\nfunction type, regardless of being impredicative. Direct and concrete\ninterpretations of simultaneous induction and mutually recursive functions are\nalso provided by extending Dybjer's interpretations on the basis of Aczel's\nrule sets. Our model can be regarded as a higher-order generalization of the\ntruth-table methods. We provide a relatively simple consistency proof of type\ntheory, which can be used as the basis for a theorem prover.<\/jats:p>","DOI":"10.2168\/lmcs-7(4:5)2011","type":"journal-article","created":{"date-parts":[[2012,6,20]],"date-time":"2012-06-20T09:05:51Z","timestamp":1340183151000},"source":"Crossref","is-referenced-by-count":6,"title":["Proof-irrelevant model of CC with predicative induction and judgmental equality"],"prefix":"10.46298","volume":"Volume 7, Issue 4","author":[{"given":"Gyesik","family":"Lee","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin","family":"Werner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2011,11,23]]},"reference":[{"key":"10.2168\/LMCS-7(4:5)2011_aczel-induction","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71120-0"},{"key":"10.2168\/LMCS-7(4:5)2011_aczel-relating","doi-asserted-by":"crossref","unstructured":"Peter Aczel. On relating type theories and set theories. InProceedings of Types '98, volume 1657 ofLecture Notes in Comput. Sci., pages 1-18. Springer, 1998.","DOI":"10.1007\/3-540-48167-2_1"},{"key":"10.2168\/LMCS-7(4:5)2011_adams-eq","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005770"},{"key":"10.2168\/LMCS-7(4:5)2011_coqman","doi-asserted-by":"crossref","unstructured":"Yves Bertot and Pierre Cast\u00e9ran.Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Springer Verlag, 2004.","DOI":"10.1007\/978-3-662-07964-5"},{"key":"10.2168\/LMCS-7(4:5)2011_coquand-meta","unstructured":"Thierry Coquand. Metamathematical Investigation on a Calculus of Constructions. In P. Odifreddi, editor,Logic and Computer Science, volume 31 of APIC series, pages 91-122. Academic Press, 1990."},{"key":"10.2168\/LMCS-7(4:5)2011_coquand-algo","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569807.011"},{"key":"10.2168\/LMCS-7(4:5)2011_drake","unstructured":"Frank R. Drake.Set Theory: An Introduction to Large Cardinals, volume 76 ofStudies in logic and the foundations of mathematics. North Holland, 1974."},{"key":"10.2168\/LMCS-7(4:5)2011_dybjer","doi-asserted-by":"crossref","unstructured":"Peter Dybjer. Inductive sets and families in Martin-L\u00f6f's type theory and their set-theoretic semantics. InLogical frameworks (Sophia-Antipolis, 1990), pages 280-306. Cambridge Univ. Press, 1991.","DOI":"10.1017\/CBO9780511569807.012"},{"key":"10.2168\/LMCS-7(4:5)2011_dybjer00","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"10.2168\/LMCS-7(4:5)2011_gimenez","doi-asserted-by":"crossref","unstructured":"Eduardo Gim\u00e9nez. Codifying guarded definitions with recursive schemes. InTypes for proofs and programs (Bastad, 1994), volume 996 ofLecture Notes in Comput. Sci., pages 39-59. Springer, 1995.","DOI":"10.1007\/3-540-60579-7_3"},{"key":"10.2168\/LMCS-7(4:5)2011_girard-proofs","unstructured":"Jean-Yves Girard, Paul Taylor, and Yves Lafont.Proofs and types, volume 7 ofCambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989."},{"key":"10.2168\/LMCS-7(4:5)2011_goguen-phd","doi-asserted-by":"crossref","unstructured":"Healfdene Goguen.A Typed {Operational Semantics for Type Theory}. PhD thesis, University of Edinburgh, 1994.","DOI":"10.1007\/BFb0014053"},{"key":"10.2168\/LMCS-7(4:5)2011_letouzey","unstructured":"Pierre Letouzey.Programmation fonctionnelle certifi\u00e9e - L'extraction de programmes dans l'assistant Coq. PhD thesis, Universit\u00e9 Paris-Sud, July 2004."},{"key":"10.2168\/LMCS-7(4:5)2011_luo89-lics","unstructured":"Zhaohui Luo. Ecc, an extended calculus of constructions. InLICS, pages 386-395. IEEE Computer Society, 1989."},{"key":"10.2168\/LMCS-7(4:5)2011_luo-ecc","unstructured":"Zhaohui Luo.An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, November 1990."},{"key":"10.2168\/LMCS-7(4:5)2011_luo-utt","unstructured":"Zhaohui Luo.Computation and reasoning: a type theory for computer science, volume 11 ofInternational Series of Monographs on Computer Science. Oxford University Press, Inc., 1994."},{"key":"10.2168\/LMCS-7(4:5)2011_ml-84","unstructured":"Per Martin-L\u00f6f.Intuitionistic type theory, volume 1 ofStudies in Proof Theory. Lecture Notes. Bibliopolis, 1984."},{"key":"10.2168\/LMCS-7(4:5)2011_miwe","doi-asserted-by":"crossref","unstructured":"Alexandre Miquel and Benjamin Werner. The not so simple proof-irrelevant model of CC. InTypes for proofs and programs, volume 2646 ofLecture Notes in Comput. Sci., pages 240-258. Springer, 2003.","DOI":"10.1007\/3-540-39185-1_14"},{"key":"10.2168\/LMCS-7(4:5)2011_moschovakis74","unstructured":"Yiannis N. Moschovakis.Elementary induction on abstract structures, volume 77 ofStudies in logic and the foundations of mathematics. North Holland, 1974."},{"key":"10.2168\/LMCS-7(4:5)2011_moschovakis","unstructured":"Yiannis N. Moschovakis.Descriptive set theory, volume 100 ofStudies in logic and the foundations of mathematics. North Holland, 1980."},{"key":"10.2168\/LMCS-7(4:5)2011_nordstroem","unstructured":"Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith.Programming in Martin-L\u00f6f's type theory: An introduction.Oxford University Press, 1990."},{"key":"10.2168\/LMCS-7(4:5)2011_pm-habili","unstructured":"Christine Paulin-Mohring.D\u00b4efinitions {Inductives en Th\u00e9orie des Types d'Ordre Sup\u00e9rieur}. Habilitation \u00e1 diriger les recherches. Universit\u00e9 Claude Bernard Lyon I, 1996."},{"key":"10.2168\/LMCS-7(4:5)2011_reynolds","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. Polymorphism is not set-theoretic. InSemantics of Data Types, volume 173 ofLecture Notes in Comput. Sci., pages 145-156. Springer, 1984.","DOI":"10.1007\/3-540-13346-1_7"},{"key":"10.2168\/LMCS-7(4:5)2011_siles","doi-asserted-by":"crossref","unstructured":"Vincent Siles and Hugo Herbelin. Equality is typable in semi-full pure type systems. InLICS, pages 21-30, 2010.","DOI":"10.1109\/LICS.2010.19"},{"key":"10.2168\/LMCS-7(4:5)2011_werner-set","doi-asserted-by":"crossref","unstructured":"Benjamin Werner. Sets in Types, Types in Sets. InTheoretical Aspects of Computer Software, volume 1281 ofLecture Notes in Comput. Sci., pages 530-546. Springer, 1997.","DOI":"10.1007\/BFb0014566"},{"key":"10.2168\/LMCS-7(4:5)2011_werner-proof","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(3:13)2008"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/920\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/920\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:59:15Z","timestamp":1681243155000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/920"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,11,23]]},"references-count":26,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(4:5)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1111.0123","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1111.0123","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,11,23]]},"article-number":"920"}}