{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:21Z","timestamp":1753894401460,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We introduce an extension of first-order logic that comes equipped with\nadditional predicates for reasoning about an abstract state. Sequents in the\nlogic comprise a main formula together with pre- and postconditions in the\nstyle of Hoare logic, and the axioms and rules of the logic ensure that the\nassertions about the state compose in the correct way. The main result of the\npaper is a realizability interpretation of our logic that extracts programs\ninto a mixed functional\/imperative language. All programs expressible in this\nlanguage act on the state in a sequential manner, and we make this intuition\nprecise by interpreting them in a semantic metatheory using the state monad.\nOur basic framework is very general, and our intention is that it can be\ninstantiated and extended in a variety of different ways. We outline in detail\none such extension: A monadic version of Heyting arithmetic with a wellfounded\nwhile rule, and conclude by outlining several other directions for future work.<\/jats:p>","DOI":"10.46298\/lmcs-20(1:7)2024","type":"journal-article","created":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T10:43:11Z","timestamp":1707475391000},"source":"Crossref","is-referenced-by-count":0,"title":["Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language"],"prefix":"10.46298","volume":"Volume 20, Issue 1","author":[{"given":"Thomas","family":"Powell","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,1,26]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/12947\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/12947\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,9]],"date-time":"2024-02-09T10:43:12Z","timestamp":1707475392000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/10776"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,26]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(1:7)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2301.01690v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2301.01690v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2301.01690","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2301.01690","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,1,26]]},"article-number":"10776"}}