A logical analysis of aliasing in imperative higher-order functions

DOI10.1017/S0956796807006417zbMath1125.68027MaRDI QIDQ5308091

Martin Berger, Kohei Honda, Nobuko Yoshida

Publication date: 26 September 2007

Published in: Journal of Functional Programming (Search for Journal in Brave)

zbMATH Keywords

call-by-value imperative higher-order functionscompositional program logic

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

An observationally complete program logic for imperative higher-order functions

Uses Software

• LARCH

Cites Work

• The logic of aliasing
• A calculus of mobile processes. I
• A theory of type polymorphism in programming
• Writing Larch interface language specifications
• Algebraic laws for nondeterminism and concurrency
• Verification of Array, Record, and Pointer Operations in Pascal
• Assignment and Procedure Call Proof Rules
• Ten Years of Hoare's Logic: A Survey—Part I
• Specifying the Semantics of while Programs: A Tutorial and Critique of a Paper by Hoare and Lauer
• Modular specification of frame properties in JML
• An axiomatic basis for computer programming