Abstract

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.

BibTeX

@article{BE-DMTCS18,
  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     = "https://dmtcs.episciences.org/4927"
}