Capsules and Separation
MetadataShow full item record
Jeannin, Jean-Baptiste; Kozen, Dexter
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.
capsule; separation logic; functional programming; imperative programming