zbMATH — the first resource for mathematics

Proof abstraction for imperative languages. (English) Zbl 1168.68361
Kobayashi, Naoki (ed.), Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8–10, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-48937-5/pbk). Lecture Notes in Computer Science 4279, 97-113 (2006).
Summary: Modularity in programming language semantics derives from abstracting over the structure of underlying denotations, yielding semantic descriptions that are more abstract 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.
For the entire collection see [Zbl 1133.68007].
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
18C50 Categorical semantics of formal languages
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI