Capsules and Separation
Jean-Baptiste Jeannin, Dexter C. Kozen · 2012
We study a formulation of separation logic using capsules, a representation of the state of a computation in higher-order programming languages with mutable variables. We prove soundness of the frame rule in this context and investigate alternative formulations with weaker side conditions.