The logical approach to stack typing

11 years 3 months ago
The logical approach to stack typing
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. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.1 [Logics and Meanings of Programs]: Specifying and Reasoning about Programs; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages General Terms Reliability, Security, Languages, Verification Keywords stack, memory management, ordered logic, bunched logic, linear logic, type systems, typed assembly language
Amal J. Ahmed, David Walker
Added 05 Jul 2010
Updated 05 Jul 2010
Type Conference
Year 2003
Where TLDI
Authors Amal J. Ahmed, David Walker
Comments (0)