Formal verification in Coq of program properties involving the global state effect
JFLA, pp. 1-16, 2014.
The syntax of an imperative language does not mention explicitly the state, while its denotational semantics has to mention it. In this paper we present a framework for the verification in Coq of properties of programs manipulating the global state effect. These properties are expressed in a proof system which is close to the syntax, as i...More
PPT (Upload PPT)