IMP with exceptions over decorated logic

IMP with exceptions over decorated logic

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

Full description

Bibliographic Details
Main Author: Burak Ekici
Format: Article
Language:English
Published: Discrete Mathematics & Theoretical Computer Science 2018-10-01
Series:Discrete Mathematics & Theoretical Computer Science
Subjects:
coq
exceptions
state
program equivalence proofs
computational effects
decorated logic
[ info.info-lo ] computer science [cs]/logic in computer science [cs.lo]
Online Access:https://dmtcs.episciences.org/3272/pdf

Internet

https://dmtcs.episciences.org/3272/pdf

Similar Items