Title :
Capsules and Separation
Author :
Jeannin, Jean-Baptiste ; Kozen, Dexter
Author_Institution :
Comput. Sci. Dept., Cornell Univ., Ithaca, NY, USA
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.
Keywords :
formal logic; high level languages; programming language semantics; capsules; frame rule; higher-order programming languages; mutable variables; separation logic; Computer languages; Context; Reactive power; Semantics; Standards; Syntactics; capsules; separation logic;
Conference_Titel :
Logic in Computer Science (LICS), 2012 27th Annual IEEE Symposium on
Conference_Location :
Dubrovnik
Print_ISBN :
978-1-4673-2263-8
DOI :
10.1109/LICS.2012.52
