The logical approach to stack typing

Amal Ahmed, David Walker

Research output: Contribution to journalArticlepeer-review

3 Scopus citations


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)
Pages (from-to)74-85
Number of pages12
JournalSIGPLAN Notices (ACM Special Interest Group on Programming Languages)
Issue number3
StatePublished - Mar 2003

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Graphics and Computer-Aided Design


  • Bunched logic
  • Linear logic
  • Memory management
  • Ordered logic
  • Stack
  • Type systems
  • Typed assembly language


Dive into the research topics of 'The logical approach to stack typing'. Together they form a unique fingerprint.

Cite this