Soundness of data refinement for a higher-order imperative language

DOI10.1016/S0304-3975(00)00339-XzbMath1002.68090MaRDI QIDQ1605184

David A. Naumann

Publication date: 15 July 2002

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

formal semanticssemanticsdata refinementpredicate transformersprogram correctnessOberonprogramming Calculi

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55)

Related Items

Towards imperative modules: reasoning about invariants and sharing of mutable state, On assertion-based encapsulation for object invariants and simulations, An observationally complete program logic for imperative higher-order functions, Category Theoretic Models of Data Refinement, State-level and value-level simulations in data refinement

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Predicate transformers and higher-order programs
• A single complete rule for data refinement
• Data refinement by calculation
• Data refinement of predicate transformers
• An algebraic construction of predicate transformers
• Data refinement, call by value and higher order programs
• Countable nondeterminism and random assignment
• The programming language oberon
• A categorical model for higher order imperative programming
• Parametricity and local variables
• Refinement Calculus
• Data Refinement
• Predicate transformer semantics of a higher-order imperative language with record subtyping