Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computing and Information Science
  4. Computing and Information Science Technical Reports
  5. Capsules and Separation

Capsules and Separation

File(s)
SeparationLogic.pdf (155.16 KB)
Content replaced at author's request on 24-Jan-2012.
Permanent Link(s)
https://hdl.handle.net/1813/28284
Collections
Computing and Information Science Technical Reports
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
capsule
•
separation logic
•
functional programming
•
imperative programming
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance