Capsules and Separation
File(s)SeparationLogic.pdf (155.16 KB)
Content replaced at author's request on 24-Jan-2012.
Permanent Link(s)
Author
Jeannin, Jean-Baptiste
Kozen, Dexter
Abstract
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.
Date Issued
2012-01-14
Keywords
Type
technical report