{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T00:38:03Z","timestamp":1760575083272,"version":"build-2065373602"},"reference-count":16,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.431.1","type":"journal-article","created":{"date-parts":[[2025,10,13]],"date-time":"2025-10-13T09:32:32Z","timestamp":1760347952000},"page":"1-16","source":"Crossref","is-referenced-by-count":0,"title":["Ground Stratification for a Logic of Definitions with Induction"],"prefix":"10.4204","volume":"431","author":[{"given":"Nathan","family":"Guermond","sequence":"first","affiliation":[{"name":"University of Minnesota"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gopalan","family":"Nadathur","sequence":"additional","affiliation":[{"name":"University of Minnesota"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"2720","published-online":{"date-parts":[[2025,10,14]]},"reference":[{"key":"A77","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1016\/S0049-237X(08)71120-0","article-title":"An Introduction to Inductive Definitions","volume-title":"Handbook of Mathematical Logic","volume":"90","author":"Aczel","year":"1977"},{"issue":"2","key":"Baelde14jfr","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/4650","article-title":"Abella: A System for Reasoning about Relational Specifications","volume":"7","author":"Baelde","year":"2014","journal-title":"Journal of Formalized Reasoning"},{"key":"BaNa12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1109\/LICS.2012.22","article-title":"Combining Deduction Modulo and Logics of Fixed-Point Definitions","volume-title":"2012 27th Annual IEEE Symposium on Logic in Computer Science","author":"Baelde","year":"2012"},{"issue":"2","key":"Ch40","doi-asserted-by":"publisher","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"Journal of Symbolic Logic"},{"issue":"4","key":"dowek03jsl","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.2178\/jsl\/1067620188","article-title":"Proof Normalization Modulo","volume":"68","author":"Dowek","year":"2003","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"GMN11","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004","article-title":"Nominal abstraction","volume":"209","author":"Gacek","year":"2011","journal-title":"Information and Computation"},{"volume-title":"Proofs and Types","year":"1989","author":"Girard","key":"GTL89"},{"key":"Ha16","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316576892","volume-title":"Practical Foundations for Programming Languages","author":"Harper","year":"2016"},{"key":"ML71","series-title":"Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/s0049-237x(08)70847-4","article-title":"Hauptsatz for the intuitionistic theory of iterated inductive definitions","volume-title":"Proc. of the Second Scandinavian Logic Symposium","volume":"63","author":"Martin-L\u00f6f","year":"1971"},{"key":"MDM00","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1016\/S0304-3975(99)00171-1","article-title":"Cut-elimination for a logic with definitions and induction","volume":"232","author":"McDowell","year":"2000","journal-title":"Theoretical Computer Science"},{"key":"MN12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139021326","volume-title":"Programming with Higher-Order Logic","author":"Miller","year":"2012"},{"key":"MT04","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-24849-1_19","article-title":"Induction and Co-induction in Sequent Calculus","volume-title":"TYPES","volume":"3085","author":"Momigliano","year":"2004"},{"issue":"2","key":"Ta67","doi-asserted-by":"publisher","first-page":"198","DOI":"10.2307\/2271658","article-title":"Intensional Interpretations of Functionals of Finite Type I","volume":"32","author":"Tait","year":"1967","journal-title":"Journal of Symbolic Logic"},{"volume-title":"A Logical Framework for Reasoning about Logical Specifications","year":"2004","author":"Tiu","key":"Tiu04"},{"key":"Tiu12","doi-asserted-by":"publisher","first-page":"544","DOI":"10.1007\/978-3-642-31365-3_43","article-title":"Stratification in Logics of Definitions","volume-title":"Automated Reasoning","author":"Tiu","year":"2012"},{"key":"WN16","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1007\/978-3-662-49498-1_29","article-title":"A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs","volume-title":"Programming Languages and Systems","author":"Wang","year":"2016"}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2025,10,15]],"date-time":"2025-10-15T11:11:14Z","timestamp":1760526674000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/2510.12297v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,14]]},"references-count":16,"URL":"https:\/\/doi.org\/10.4204\/eptcs.431.1","relation":{},"ISSN":["2075-2180"],"issn-type":[{"type":"electronic","value":"2075-2180"}],"subject":[],"published":{"date-parts":[[2025,10,14]]}}}