{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,18]],"date-time":"2025-12-18T19:06:48Z","timestamp":1766084808070,"version":"build-2065373602"},"reference-count":47,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.435.4","type":"journal-article","created":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T17:08:07Z","timestamp":1762016887000},"page":"41-57","source":"Crossref","is-referenced-by-count":1,"title":["Ruitenburg's Theorem Mechanized and Contextualized"],"prefix":"10.4204","volume":"435","author":[{"given":"Tadeusz","family":"Litak","sequence":"first","affiliation":[{"name":"University of Naples Federico II"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"2720","published-online":{"date-parts":[[2025,11,4]]},"reference":[{"key":"Benthem06:sl","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s11225-006-8301-9","article-title":"Modal Frame Correspondences and Fixed-Points","volume":"83","author":"van Benthem","year":"2006","journal-title":"Studia Logica"},{"issue":"2","key":"BentonBP98:jfp","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1017\/S0956796898002998","article-title":"Computational Types from a Logical Perspective","volume":"8","author":"Benton","year":"1998","journal-title":"J. Funct. Program."},{"key":"BirkedalMSS12:lmcs","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-8(4:1)2012","article-title":"First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees","volume":"8","author":"Birkedal","year":"2012","journal-title":"LMCS"},{"key":"BlokP89:ams","series-title":"Memoirs AMS","volume-title":"Algebraizable logics","volume":"77 (396)","author":"Blok","year":"1989"},{"issue":"2","key":"BrotherstonK14:jacm","doi-asserted-by":"publisher","DOI":"10.1145\/2542667","article-title":"Undecidability of Propositional Separation Logic and Its Neighbours","volume":"61","author":"Brotherston","year":"2014-04","journal-title":"J. ACM"},{"key":"ChagrovZ97:ml","series-title":"Oxford Logic Guides","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198537793.001.0001","volume-title":"Modal Logic","volume":"35","author":"Chagrov","year":"1997"},{"key":"CloustonG15:fossacs","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/978-3-662-46678-0.08emwidth.35em height.6pt.08em9","article-title":"Sequent Calculus in the Topos of Trees","volume-title":"Proceedings of FoSSaCS 2015","volume":"9034","author":"Clouston","year":"2015"},{"issue":"1","key":"Dunn70","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/2271149","article-title":"Algebraic Completeness Results for R-Mingle and Its Extensions","volume":"35","author":"Dunn","year":"1970","journal-title":"The Journal of Symbolic Logic"},{"key":"dyck:cont92","doi-asserted-by":"publisher","first-page":"795","DOI":"10.2307\/2275431","article-title":"Contraction-free sequent calculi for intuitionistic logic","volume":"57","author":"Dyckhoff","year":"1992","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"FairtloughM97:ic","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1997.2627","article-title":"Propositional Lax Logic","volume":"137","author":"Fairtlough","year":"1997","journal-title":"Information and Computation"},{"key":"FereeG23","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1145\/3573105.3575668","article-title":"Formalizing and Computing Propositional Quantifiers","volume-title":"Proceedings of CPP 2023","author":"F\u00e9r\u00e9e","year":"2023"},{"key":"FontJP03a:sl","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1023\/A:1024621922509","article-title":"A Survey of Abstract Algebraic Logic","volume":"74","author":"Font","year":"2003","journal-title":"Studia Logica"},{"key":"GalatosJKO07","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Residuated Lattices: An Algebraic Glimpse at Substructural Logics","volume":"151","author":"Galatos","year":"2007"},{"key":"ghil:shea02","series-title":"Trends In Logic, Studia Logica Library","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9936-8","volume-title":"Sheaves, Games and Model Completions","volume":"14","author":"Ghilardi","year":"2002"},{"key":"Ghilardi2016","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-662-49630-5.08emwidth.35em height.6pt.08em8","article-title":"Fixed-Point Elimination in the Intuitionistic Propositional Calculus","volume-title":"Proceedings of FoSSaCS 2016","author":"Ghilardi","year":"2016"},{"issue":"1","key":"GhilardiGS20","doi-asserted-by":"publisher","DOI":"10.1145\/3359669","article-title":"Fixed-point Elimination in the Intuitionistic Propositional Calculus","volume":"21","author":"Ghilardi","year":"2020","journal-title":"ACM Trans. Comput. Log."},{"key":"GhilardiS18","first-page":"277","article-title":"Ruitenburg's Theorem via Duality and Bounded Bisimulations","volume-title":"Proceedings of AiML 2018","author":"Ghilardi","year":"2018"},{"issue":"6","key":"GhilardiS20","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1017\/S0960129519000203","article-title":"Free Heyting algebra endomorphisms: Ruitenburg's Theorem and beyond","volume":"30","author":"Ghilardi","year":"2020","journal-title":"Math. Struct. Comput. Sci."},{"key":"ghil:shea95","doi-asserted-by":"publisher","first-page":"911","DOI":"10.2307\/2275765","article-title":"A sheaf representation and duality for finitely presented Heyting algebras","volume":"60","author":"Ghilardi","year":"1995","journal-title":"Journal of Symbolic Logic"},{"issue":"2","key":"GilFJM20","doi-asserted-by":"publisher","DOI":"10.1007\/s00012-020-00659-5","article-title":"Structure theorems for idempotent residuated lattices","volume":"81","author":"Gil-F\u00e9rez","year":"2020","journal-title":"Algebra universalis"},{"key":"GoreRS21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-030-86059-2.08emwidth.35em height.6pt.08em18","article-title":"Cut-Elimination for Provability Logic by Terminating Proof-Search: Formalised and Deconstructed Using Coq","volume-title":"Proceedings of TABLEAUX 2021","volume":"12842","author":"Gor\u00e9","year":"2021"},{"key":"hude:boun89","series-title":"Ph.D. Thesis","volume-title":"Bounds for cut elimination in intuitionistic propositional logic","author":"Hudelmaier","year":"1989"},{"key":"Humberstone2011","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/9055.001.0001","volume-title":"The Connectives","author":"Humberstone","year":"2011"},{"key":"Litak14:trends","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-94-017-8860-1.08emwidth.35em height.6pt.08em8","article-title":"Constructive Modalities with Provability Smack","volume-title":"Leo Esakia on Duality in Modal and Intuitionistic Logics","author":"Litak","year":"2014"},{"key":"litakpr17","series-title":"Leibniz International Proceedings in Informatics (LIPIcs)","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.27","article-title":"Negative Translations and Normal Modality","volume-title":"2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)","volume":"84","author":"Litak","year":"2017"},{"issue":"5","key":"Mardaev1993:al","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/BF02261708","article-title":"Least fixed points in Grzegorczyk's logic and in the intuitionistic propositional logic","volume":"32","author":"Mardaev","year":"1993","journal-title":"Algebra and Logic"},{"issue":"2","key":"Mardaev1994:al","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/BF00739995","article-title":"Convergence of positive schemes in S4 and Int","volume":"33","author":"Mardaev","year":"1994","journal-title":"Algebra and Logic"},{"key":"Mardaev1997:bsl","first-page":"135","article-title":"Fixed points of modal negative operators","volume":"26","author":"Mardaev","year":"1997","journal-title":"Bull. Sect. Log., Univ. Lodz, Dep. Log"},{"issue":"3","key":"Mardaev1998:al","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BF02671590","article-title":"Negative modal schemes","volume":"37","author":"Mardaev","year":"1998","journal-title":"Algebra and Logic"},{"issue":"3","key":"Mardaev2007:jancl","doi-asserted-by":"publisher","first-page":"317","DOI":"10.3166\/jancl.17.317-346","article-title":"Definable fixed points in modal and temporal logics\u2014a survey","volume":"17","author":"Mardaev","year":"2007","journal-title":"Journal of Applied Non-Classical Logics"},{"issue":"1","key":"McBrideP08:jfp","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S095679680700632","article-title":"Applicative programming with effects","volume":"18","author":"McBride","year":"2008","journal-title":"J. Funct. Program."},{"issue":"4","key":"Nishimura60:jsl","doi-asserted-by":"publisher","first-page":"327","DOI":"10.2307\/2963526","article-title":"On Formulas of One Variable in Intuitionistic Propositional Calculus","volume":"25","author":"Nishimura","year":"1960","journal-title":"The Journal of Symbolic Logic"},{"issue":"2","key":"OHearnP99:jsl","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","article-title":"The Logic of Bunched Implications","volume":"5","author":"O'Hearn","year":"1999","journal-title":"The Bulletin of Symbolic Logic"},{"key":"Pitts92:jsl","doi-asserted-by":"publisher","first-page":"33","DOI":"10.2307\/2275175","article-title":"On an interpretation of second order quantification in first order intuitionistic propositional logic","volume":"57","author":"Pitts","year":"1992","journal-title":"The Journal of Symbolic Logic"},{"issue":"1","key":"PymOHY04:tcs","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/j.tcs.2003.11.020","article-title":"Possible worlds and resources: the semantics of BI","volume":"315","author":"Pym","year":"2004","journal-title":"Theoretical Computer Science"},{"key":"Raftery07","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-07-04235-3","article-title":"Representable idempotent commutative residuated lattices","volume":"359","author":"Raftery","year":"2007","journal-title":"Trans. Am. Math. Soc."},{"key":"Reynolds02:lics","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1109\/LICS.2002.1029817","article-title":"Separation Logic: A Logic for Shared Mutable Data Structures","volume-title":"Proceedings of LiCS 2002","author":"Reynolds","year":"2002"},{"key":"Rieger49","series-title":"Acta Facultatis Rerum Naturalium Universitatis Carolinae","doi-asserted-by":"publisher","DOI":"10.2307\/2266273","volume-title":"On the lattice theory of Brouwerian propositional logic","volume":"189","author":"Rieger","year":"1949"},{"key":"Ruitenburg84:jsl","doi-asserted-by":"publisher","first-page":"892","DOI":"10.2307\/2274142","article-title":"On the period of sequences (A^n(p)) in intuitionistic propositional calculus","volume":"49","author":"Ruitenburg","year":"1984","journal-title":"Journal of Symbolic Logic"},{"issue":"8","key":"Shapirovsky18:aiml","first-page":"2333","article-title":"Glivenko's Theorem, Finite Height, and Local Tabularity","volume":"8","author":"Shapirovsky","year":"2021","journal-title":"FLAP"},{"key":"ShillitoGGI23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/978-3-031-43513-3.08emwidth.35em height.6pt.08em5","article-title":"A New Calculus for Intuitionistic Strong L\u00f6b Logic: Strong Termination and Cut-Elimination, Formalised","volume-title":"Proceedings of TABLEAUX 2023","volume":"14278","author":"Shillito","year":"2023"},{"key":"ShillitoG22","first-page":"429","article-title":"Direct elimination of additive-cuts in GL4ip: verified and extracted","volume-title":"Proceedings of AiML 2022","author":"Shillito","year":"2022"},{"volume-title":"The Proof Theory and Semantics of Intuitionistic Modal Logic","year":"1994","author":"Simpson","key":"Simpson94:phd"},{"key":"viss:laye96","first-page":"139","article-title":"Uniform Interpolation and Layered Bisimulation","volume-title":"G\u00f6del '96, Logical Foundations of Mathematics, Computer Science and Physics \u2014Kurt G\u00f6del's Legacy","author":"Visser","year":"1996"},{"key":"Visser05:lncs","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/11601548.08emwidth.35em height.6pt.08em3","article-title":"L\u00f6b's Logic Meets the \u03bc-calculus","volume-title":"Processes, Terms and Cycles: Steps on the Road to Infinity, Essays Dedicated to Jan Willem Klop, on the Occasion of His 60th Birthday","volume":"3838","author":"Visser","year":"2005"},{"key":"WolterZ97:al","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF02672476","article-title":"On the relation between intuitionistic and classical modal logics","volume":"36","author":"Wolter","year":"1997","journal-title":"Algebra and Logic"},{"key":"WolterZ98:lw","first-page":"168","article-title":"Intuitionistic Modal Logics as fragments of Classical Modal Logics","volume-title":"Logic at Work, Essays in honour of Helena Rasiowa","author":"Wolter","year":"1998"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T12:01:20Z","timestamp":1762344080000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2402.01840v2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,4]]},"references-count":47,"URL":"https:\/\/doi.org\/10.4204\/eptcs.435.4","relation":{},"ISSN":["2075-2180"],"issn-type":[{"type":"electronic","value":"2075-2180"}],"subject":[],"published":{"date-parts":[[2025,11,4]]}}}