TY - GEN
T1 - The Logical Approach to Stack Typing
AU - Ahmed, Amal
AU - Walker, David P.
PY - 2003/10/17
Y1 - 2003/10/17
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=0141886045&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0141886045&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:0141886045
SN - 1581136498
T3 - Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation
SP - 74
EP - 85
BT - Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation
T2 - Proceedings of the TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation
Y2 - 18 January 2003 through 18 January 2003
ER -