Skip to main content


eCommons@Cornell

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

Files in This Item:

File Description SizeFormat
SeparationLogic.pdfContent replaced at author's request on 24-Jan-2012.155.16 kBAdobe PDFView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us