IMP with exceptions over decorated logic

Burak Ekici (1)

1 CASYS - Calculs Algébriques et Systèmes Dynamiques

In this paper, we separately design the decorated logic with respect to the state and the exception effects. Then, we combine two logics to be able to establish small-step semantics of IMP imperative language with exceptional abilities, in a decorated setting. We implement the decorated framework in Coq and certify program equivalence proofs written in that context.

Mots clés: proofs of programs; proof verification; Coq.; Decorated logic

Domaines: Logique en informatique [cs.LO]

Burak Ekici. IMP with exceptions over decorated logic. 2015. ⟨hal-01132831v1⟩