The Logical Approach to Stack Typing

Amal Ahmed, David P. Walker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

15 Scopus citations

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 languageEnglish (US)
Title of host publicationProceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation
Pages74-85
Number of pages12
StatePublished - Oct 17 2003
EventProceedings of the TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation - New Orleans, LA, United States
Duration: Jan 18 2003Jan 18 2003

Publication series

NameProceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation

Other

OtherProceedings of the TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation
CountryUnited States
CityNew Orleans, LA
Period1/18/031/18/03

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'The Logical Approach to Stack Typing'. Together they form a unique fingerprint.

  • Cite this

    Ahmed, A., & Walker, D. P. (2003). The Logical Approach to Stack Typing. In Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (pp. 74-85). (Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation).