zbMATH — the first resource for mathematics

IMP with exceptions over decorated logic. (English) Zbl 1402.68032
Summary: 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 serves 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.
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
03G30 Categorical logic, topoi
68N15 Theory of programming languages
68Q55 Semantics in the theory of computing
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
IMP+Exc; Coq
Full Text: Link