{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:37:19Z","timestamp":1753889839797,"version":"3.41.2"},"reference-count":24,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,2,16]],"date-time":"2012-02-16T00:00:00Z","timestamp":1329350400000},"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>This paper defines a sound and complete semantic criterion, based on reducibility candidates, for strong normalization of theories expressed in minimal deduction modulo \\`a la Curry. The use of Curry-style proof-terms allows to build this criterion on the classic notion of pre-Heyting algebras and makes that criterion concern all theories expressed in minimal deduction modulo. Compared to using Church-style proof-terms, this method provides both a simpler definition of the criterion and a simpler proof of its completeness.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:3)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":0,"title":["On completeness of reducibility candidates as a semantics of strong normalization"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"given":"Denis","family":"Cousineau","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,2,16]]},"reference":[{"key":"10.2168\/LMCS-8(1:3)2012_BG01","doi-asserted-by":"crossref","unstructured":"H. Barendregt and H. Geuvers. Proof-assistants using dependent type systems. In J. A. Robinson and A. Voronkov, editors,Handbook of Automated Reasoning, pages 1149-1238. Elsevier and MIT Press, 2001.","DOI":"10.1016\/B978-044450813-3\/50020-5"},{"key":"10.2168\/LMCS-8(1:3)2012_CohenCH","unstructured":"Paul J. Cohen. The independence of the continuum hypothesis. Stanford University Press, 1963,64."},{"key":"10.2168\/LMCS-8(1:3)2012_Coq","unstructured":"Coq proof assistant. http:\/\/coq.inria.fr. Denis Cousineau. Complete reducibility candidates. InProof search in Type Theory, pages 1-13, 2009."},{"key":"10.2168\/LMCS-8(1:3)2012_Theseoim","unstructured":"Denis Cousineau.Models and proof normalization. PhD thesis, \u00c9cole Polytechnique, 2009."},{"key":"10.2168\/LMCS-8(1:3)2012_PTS","doi-asserted-by":"crossref","unstructured":"Denis Cousineau and Gilles Dowek. Embedding pure type systems in the lambda-pi-calculus modulo. InTLCA, pages 102-117, 2007.","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"10.2168\/LMCS-8(1:3)2012_CouMiq","unstructured":"Denis Cousineau and Alexandre Miquel. On proof-terms for deduction modulo. (submitted)."},{"key":"10.2168\/LMCS-8(1:3)2012_CurryCL","unstructured":"Haskell B. Curry and Feys Robert.Combinatory Logic. Amsterdam: North Holland, 1958."},{"key":"10.2168\/LMCS-8(1:3)2012_dedukti","unstructured":"Dedukti proof-checker. http:\/\/www.lix.polytechnique.fr\/dedukti. Gilles Dowek. Truth value algebras and normalization. In Thorsten Altenkirch and Conor McBride, editors,TYPES for proofs and programs, volume 4502 ofLecture Notes in Computer Science, pages 110-124. Springer, 2007."},{"key":"10.2168\/LMCS-8(1:3)2012_DHK","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"Gilles Dowek, Th\u00e9r\u00e8se Hardin, and Claude","year":"2003","journal-title":"Journal of Automated Reasoning"},{"key":"10.2168\/LMCS-8(1:3)2012_GDowAMiq07","unstructured":"Gilles Dowek and Alexandre Miquel. Cut elimination for Zermelo's set theory.manuscript, 2007."},{"issue":"4","key":"10.2168\/LMCS-8(1:3)2012_DW","doi-asserted-by":"crossref","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","volume":"68","author":"Gilles Dowek and Benjamin Werner","year":"2003","journal-title":"The Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(1:3)2012_GDowBWer05","doi-asserted-by":"crossref","unstructured":"Gilles Dowek and Benjamin Werner. Arithmetic as a theory modulo. In J\u00fcrgen Giesl, editor,RTA, volume 3467 ofLecture Notes in Computer Science, pages 423-437. Springer, 2005.","DOI":"10.1007\/978-3-540-32033-3_31"},{"key":"10.2168\/LMCS-8(1:3)2012_Girard71","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"10.2168\/LMCS-8(1:3)2012_Godel","unstructured":"Kurt G\u00f6del.\u00dcber die Vollst\u00e4ndigkeit des Logikkalk\u00fcls. PhD thesis, University Of Vienna, 1929."},{"key":"10.2168\/LMCS-8(1:3)2012_GodelcontCH","unstructured":"Kurt G\u00f6del. The consistency of the axiom of choice and of the generalized continuum hypothesis with the axioms of set theory. Princeton University Press, 1940."},{"key":"10.2168\/LMCS-8(1:3)2012_Henkin49","doi-asserted-by":"crossref","first-page":"159","DOI":"10.2307\/2267044","volume":"14","author":"Leon Henkin","year":"1949","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"10.2168\/LMCS-8(1:3)2012_Henkin","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"Leon Henkin","year":"1950","journal-title":"Journal of Symbolic Logic"},{"key":"10.2168\/LMCS-8(1:3)2012_hollight","unstructured":"Hol-light proof assistant. http:\/\/www.cl.cam.ac.uk\/ jrh13\/hol-light. J. L. Krivine.Lambda-calculus, types and models. Masson, 1993."},{"key":"10.2168\/LMCS-8(1:3)2012_Leivant83","doi-asserted-by":"crossref","unstructured":"Daniel Leivant. Polymorphic type inference. InPOPL, pages 88-98, 1983.","DOI":"10.1145\/567067.567077"},{"key":"10.2168\/LMCS-8(1:3)2012_HSchATro96","unstructured":"Helmut Schwichtenberg and Anne Sjerp Troelstra.Basic Proof Theory. Cambridge University Press, 1996."},{"key":"10.2168\/LMCS-8(1:3)2012_Tarskitrans","unstructured":"Alfred Tarski (Magda Stroi\u00c5\u0084ska and trans.) David Hitchcock. On the concept of following logically. Inistory and Philosophy of Logic, pages 55-96, 2002."},{"key":"10.2168\/LMCS-8(1:3)2012_Tait66","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1966-11611-7"},{"key":"10.2168\/LMCS-8(1:3)2012_Tarski","doi-asserted-by":"crossref","unstructured":"Alfred Tarski. \u00fcber den begriff der logischen folgerung. InCongr\u00e8s international de philosophie scientifique, pages 1-11. Paris Sorbonne, 1936.","DOI":"10.5840\/icus11936742"},{"key":"10.2168\/LMCS-8(1:3)2012_BLRU94","doi-asserted-by":"crossref","unstructured":"Steffen van Bakel, Luigi Liquori, Simona Ronchi Della Rocca, and Pawel Urzyczyn. Comparing cubes. In Anil Nerode and Yuri Matiyasevich, editors,LFCS, volume 813 ofLecture Notes in Computer Science, pages 353-365. Springer, 1994.","DOI":"10.1007\/3-540-58140-5_33"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/845\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/845\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:09:52Z","timestamp":1744067392000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/845"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,2,16]]},"references-count":24,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:3)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1201.1705","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1201.1705","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,2,16]]},"article-number":"845"}}