The logical approach to stack typing
Amal Ahmed, David P. Walker · 2003
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.