Idealized ML and Its Separation Logic
Neelakantan R. Krishnaswami, Lars Birkedal, Jonathan Aldrich, John Reynolds · 2006
Separation logic is an extension of Hoare logic which permits reasoning about low-level imperative programs that use shared mutable heap structure. In this work, we present a version of separation logic that permits effective, modular reasoning about typed, higherorder functional programs that use aliased mutable heap data, including pointers to code. Furthermore, we show how to use predicates in higher-order separation logic to modularly and abstractly specify the sharing behavior of programs.