The Logical Approach to Stack Typing

Amal Ahmed; David Walker

The Logical Approach to Stack Typing

Amal Ahmed, David Walker

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

16 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 language	English (US)
Title of host publication	Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation
Pages	74-85
Number of pages	12
State	Published - 2003
Event	Proceedings of the TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation - New Orleans, LA, United States Duration: Jan 18 2003 → Jan 18 2003

Publication series

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

Other

Other	Proceedings of the TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation
Country/Territory	United States
City	New Orleans, LA
Period	1/18/03 → 1/18/03

All Science Journal Classification (ASJC) codes

General Engineering

Keywords

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

Cite this

@inproceedings{cdb26aad84f94ca690bb284c2ca4b6f0,

title = "The Logical Approach to Stack Typing",

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.",

keywords = "Bunched logic, Linear logic, Memory management, Ordered logic, Stack, Type systems, Typed assembly language",

author = "Amal Ahmed and David Walker",

year = "2003",

language = "English (US)",

isbn = "1581136498",

series = "Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation",

pages = "74--85",

booktitle = "Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation",

note = "Proceedings of the TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation ; Conference date: 18-01-2003 Through 18-01-2003",

}

Ahmed, A & Walker, D 2003, The Logical Approach to Stack Typing. in Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, pp. 74-85, Proceedings of the TLDI'03: 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, New Orleans, LA, United States, 1/18/03.

The Logical Approach to Stack Typing. / Ahmed, Amal; Walker, David.
Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation. 2003. p. 74-85 (Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - The Logical Approach to Stack Typing

AU - Ahmed, Amal

AU - Walker, David

PY - 2003

Y1 - 2003

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.

KW - Bunched logic

KW - Linear logic

KW - Memory management

KW - Ordered logic

KW - Stack

KW - Type systems

KW - Typed assembly language

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 -

The Logical Approach to Stack Typing

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Keywords

Other files and links

Fingerprint

Cite this