Jeannin, Jean-BaptisteKozen, Dexter2012-01-142012-01-142012-01-14https://hdl.handle.net/1813/28284We 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.en-UScapsuleseparation logicfunctional programmingimperative programmingtechnical report