{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:37:56Z","timestamp":1753889876065,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"Automata, Logic and Semantics","funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["714034"],"award-info":[{"award-number":["714034"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"accepted":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p xml:lang=\"en\">In this paper, we facilitate the reasoning about impure programming languages, by annotating terms with \u201cdecorations\u201dthat describe what computational (side) effect evaluation of a term may involve. In a point-free categorical language,called the \u201cdecorated logic\u201d, we formalize the mutable state and the exception effects first separately, exploiting anice duality between them, and then combined. The combined decorated logic is used as the target language forthe denotational semantics of the IMP+Exc imperative programming language, and allows us to prove equivalencesbetween programs written in IMP+Exc. The combined logic is encoded in Coq, and this encoding is used to certifysome program equivalence proofs.<\/jats:p>","DOI":"10.23638\/dmtcs-20-2-11","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T16:43:42Z","timestamp":1743698622000},"source":"Crossref","is-referenced-by-count":0,"title":["IMP with exceptions over decorated logic"],"prefix":"10.23638","volume":"vol. 20 no. 2","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6602-7906","authenticated-orcid":false,"given":"Burak","family":"Ekici","sequence":"first","affiliation":[{"name":"Department of Computer Science [Innsbruck]"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2018,10,29]]},"container-title":["Discrete Mathematics &amp; Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/hal.science\/hal-01132831v9\/document","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/hal.science\/hal-01132831v9\/document","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T16:43:42Z","timestamp":1743698622000},"score":1,"resource":{"primary":{"URL":"http:\/\/dmtcs.episciences.org\/3272"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,29]]},"references-count":0,"journal-issue":{"issue":"Automata, Logic and Semantics","published-online":{"date-parts":[[2018,10,29]]}},"URL":"https:\/\/doi.org\/10.23638\/dmtcs-20-2-11","relation":{"has-preprint":[{"id-type":"uri","id":"https:\/\/hal.science\/hal-01132831v8","asserted-by":"subject"},{"id-type":"uri","id":"https:\/\/hal.science\/hal-01132831v7","asserted-by":"subject"},{"id-type":"uri","id":"https:\/\/hal.science\/hal-01132831v6","asserted-by":"subject"}],"is-same-as":[{"id-type":"uri","id":"https:\/\/hal.science\/hal-01132831v9","asserted-by":"subject"}]},"ISSN":["1365-8050"],"issn-type":[{"type":"electronic","value":"1365-8050"}],"subject":[],"published":{"date-parts":[[2018,10,29]]},"article-number":"3272"}}