|
eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/28284
| Title: | Capsules and Separation |
| Authors: | Jeannin, Jean-Baptiste
Kozen, Dexter |
| Keywords: | capsule
separation logic
functional programming
imperative programming |
| Issue Date: | 14-Jan-2012 |
| 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. |
| URI: | http://hdl.handle.net/1813/28284 |
| Appears in Collections: | Computing and Information Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
