{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:23Z","timestamp":1780994543411,"version":"3.54.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,10,3]],"date-time":"2012-10-03T00:00:00Z","timestamp":1349222400000},"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 the topos S of trees as a model of guarded recursion. We study the\ninternal dependently-typed higher-order logic of S and show that S models two\nmodal operators, on predicates and types, which serve as guards in recursive\ndefinitions of terms, predicates, and types. In particular, we show how to\nsolve recursive type equations involving dependent types. We propose that the\ninternal logic of S provides the right setting for the synthetic construction\nof abstract versions of step-indexed models of programming languages and\nprogram logics. As an example, we show how to construct a model of a\nprogramming language with higher-order store and recursive types entirely\ninside the internal logic of S. Moreover, we give an axiomatic categorical\ntreatment of models of synthetic guarded domain theory and prove that, for any\ncomplete Heyting algebra A with a well-founded basis, the topos of sheaves over\nA forms a model of synthetic guarded domain theory, generalizing the results\nfor S.<\/jats:p>","DOI":"10.2168\/lmcs-8(4:1)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:21:33Z","timestamp":1385731293000},"source":"Crossref","is-referenced-by-count":46,"title":["First steps in synthetic guarded domain theory: step-indexing in the topos of trees"],"prefix":"10.46298","volume":"Volume 8, Issue 4","author":[{"given":"Lars","family":"Birkedal","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rasmus Ejlers","family":"M\u00f8gelberg","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jan","family":"Schwinghammer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kristian","family":"St\u00f8vring","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"25203","published-online":{"date-parts":[[2012,10,3]]},"reference":[{"key":"713:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1041\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1041\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:01:59Z","timestamp":1681243319000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1041"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,3]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(4:1)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1208.3596","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1208.3596","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,10,3]]},"article-number":"1041"}}