The logical approach to stack typing

Amal Ahmed, David Walker

Research output: Contribution to journalArticle

3 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)
Pages (from-to)74-85
Number of pages12
JournalACM SIGPLAN Notices
Volume38
Issue number3
DOIs
StatePublished - Mar 2003

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Graphics and Computer-Aided Design

Keywords

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

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

Cite this