Separation Logic for a Higher-Order Typed Language
Neelakantan R. Krishnaswami, John Reynolds, Jonathan Aldrich · 2005
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 create an extension of separation logic that permits effective, modular reasoning about typed, higher-order functional programs that use aliased mutable heap data, including pointers to code.