IMP with Exceptions over Decorated Logic

Burak Ekici

Discrete Mathematics and Theoretical Computer Science 20(2), pp. 1 – 43, 2018.


In this paper, we facilitate the reasoning about impure programming languages, by annotating terms with “decorations” that describe what computational (side) effect evaluation of a term may involve. In a point-free categorical language, called the “decorated logic”, we formalize the mutable state and the exception effects first separately, exploiting a nice duality between them, and then combined.

The combined decorated logic is used as the target language for the denotational semantics of the IMP+Exc imperative programming language, and allows us to prove equivalences between programs written in IMP+Exc. The combined logic is encoded in Coq, and this encoding is used to certify some program equivalence proofs..


  PDF |  © Creative Commons License – CC BY 4.0


author = "Burak Ekici",
title = "IMP with exceptions over decorated logic",
journal = "Discrete Mathematics and Theoretical Computer Science",
editor = "Anca Muscholl and Jens Gustedt",
series = "Episciences",
volume = "vol. 20 no. 2",
pages = "1--43",
year = "2018",
url = ""
Nach oben scrollen