Burak Ekici - IMP with exceptions over decorated logic

dmtcs:3272 - Discrete Mathematics & Theoretical Computer Science, October 29, 2018, vol. 20 no. 2 - https://doi.org/10.23638/DMTCS-20-2-11
IMP with exceptions over decorated logicArticle

Authors: Burak Ekici ORCID1

  • 1 Department of Computer Science [Innsbruck]

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 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.


Volume: vol. 20 no. 2
Section: Automata, Logic and Semantics
Published on: October 29, 2018
Accepted on: October 5, 2018
Submitted on: April 18, 2017
Keywords: Coq,exceptions,state,program equivalence proofs,Computational effects,decorated logic, [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO]
Funding:
    Source : OpenAIRE Graph
  • Strong Modular proof Assistance: Reasoning across Theories; Funder: European Commission; Code: 714034
  • Interactive Proof: Proof Translation, Premise Selection, Rewriting; Funder: Austrian Science Fund (FWF); Code: P 26201

Consultation statistics

This page has been seen 646 times.
This article's PDF has been downloaded 642 times.