Abstract
We develop a logic for reasoning about adjacency and separation of memory blocks, as well as aliasing of pointers. We provide a memory model for our logic and present a sound set of natural deduction-style inference rules. We deploy the logic in a simple type system for a stack-based assembly language. The connectives for the logic provide a flexible yet concise mechanism for controlling allocation, deallocation and access to both heap-allocated and stack-allocated data.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 74-85 |
| Number of pages | 12 |
| Journal | SIGPLAN Notices (ACM Special Interest Group on Programming Languages) |
| Volume | 38 |
| Issue number | 3 |
| DOIs | |
| State | Published - Mar 2003 |
All Science Journal Classification (ASJC) codes
- Software
- Computer Graphics and Computer-Aided Design
Keywords
- Bunched logic
- Linear logic
- Memory management
- Ordered logic
- Stack
- Type systems
- Typed assembly language