Proof Abstraction for Imperative Languages

straction for Imperative Languages William L. Harrison Dept. of Computer Science, University of Missouri, Columbia, Missouri, USA. ty in programming language semantics derives from abstracting over the structure of underlying denotations, yielding semantic descriptions that are tract and reusable. One such semantic framework is Liang’s modular monadic semantics in which the underlying semantic structure is encapsulated with a monad. Such abstraction can be at odds with program verification, however, because program specifications require access to the (deliberately) hidden semantic representation. The techniques for reasoning about modular monadic definitions of imperative programs introduced here overcome this barrier. And, just like program definitions in modular monadic semantics, our program specifications and proofs are representation-independent and hold for whole classes of monads, thereby yielding proofs of great generality.

• Type: Conference
• Year: 2006
• Where: APLAS
• Authors: William L. Harrison
• Keywords: APLAS 2006, Modular Monadic Definitions, Modular Monadic Semantics, Programming Language Semantics