Certifying compilation for a language with stack allocation

Limin Jia; Frances Spalding; David Walker; Neal Glew

doi:10.1109/LICS.2005.9

Certifying compilation for a language with stack allocation

Limin Jia, Frances Spalding, David Walker, Neal Glew

Computer Science

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

9 Scopus citations

Abstract

This paper describes an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is a tree of "stack tags" that tracks the evolution of the stack over time. To demonstrate the expressiveness of the type system, we define Micro-CLI, a simple imperative language that captures the essence of stack allocation in the Common Language Infrastructure. We show how to compile welltyped Micro-CLI into well-typed assembly.

Original language	English (US)
Title of host publication	Proceedings - 20th Annual IEEE symposium on Logic in Computer Science, LICS 2005
Pages	407-416
Number of pages	10
DOIs	https://doi.org/10.1109/LICS.2005.9
State	Published - 2005
Event	20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005 - Chicago, IL, United States Duration: Jun 26 2005 → Jun 29 2005

Publication series

Name	Proceedings - Symposium on Logic in Computer Science
ISSN (Print)	1043-6871

Other

Other	20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005
Country/Territory	United States
City	Chicago, IL
Period	6/26/05 → 6/29/05

All Science Journal Classification (ASJC) codes

Software
General Mathematics

Access to Document

10.1109/LICS.2005.9

Cite this

@inproceedings{e44505ddc68c47eba76919b599377363,

title = "Certifying compilation for a language with stack allocation",

abstract = "This paper describes an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is a tree of {"}stack tags{"} that tracks the evolution of the stack over time. To demonstrate the expressiveness of the type system, we define Micro-CLI, a simple imperative language that captures the essence of stack allocation in the Common Language Infrastructure. We show how to compile welltyped Micro-CLI into well-typed assembly.",

author = "Limin Jia and Frances Spalding and David Walker and Neal Glew",

year = "2005",

doi = "10.1109/LICS.2005.9",

language = "English (US)",

isbn = "0769522661",

series = "Proceedings - Symposium on Logic in Computer Science",

pages = "407--416",

booktitle = "Proceedings - 20th Annual IEEE symposium on Logic in Computer Science, LICS 2005",

note = "20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005 ; Conference date: 26-06-2005 Through 29-06-2005",

}

Jia, L, Spalding, F, Walker, D & Glew, N 2005, Certifying compilation for a language with stack allocation. in Proceedings - 20th Annual IEEE symposium on Logic in Computer Science, LICS 2005. Proceedings - Symposium on Logic in Computer Science, pp. 407-416, 20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005, Chicago, IL, United States, 6/26/05. https://doi.org/10.1109/LICS.2005.9

TY - GEN

T1 - Certifying compilation for a language with stack allocation

AU - Jia, Limin

AU - Spalding, Frances

AU - Walker, David

AU - Glew, Neal

PY - 2005

Y1 - 2005

N2 - This paper describes an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is a tree of "stack tags" that tracks the evolution of the stack over time. To demonstrate the expressiveness of the type system, we define Micro-CLI, a simple imperative language that captures the essence of stack allocation in the Common Language Infrastructure. We show how to compile welltyped Micro-CLI into well-typed assembly.

AB - This paper describes an assembly-language type system capable of ensuring memory safety in the presence of both heap and stack allocation. The type system uses linear logic and a set of domain-specific predicates to specify invariants about the shape of the store. Part of the model for our logic is a tree of "stack tags" that tracks the evolution of the stack over time. To demonstrate the expressiveness of the type system, we define Micro-CLI, a simple imperative language that captures the essence of stack allocation in the Common Language Infrastructure. We show how to compile welltyped Micro-CLI into well-typed assembly.

UR - http://www.scopus.com/inward/record.url?scp=26844555299&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=26844555299&partnerID=8YFLogxK

U2 - 10.1109/LICS.2005.9

DO - 10.1109/LICS.2005.9

M3 - Conference contribution

AN - SCOPUS:26844555299

SN - 0769522661

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 407

EP - 416

BT - Proceedings - 20th Annual IEEE symposium on Logic in Computer Science, LICS 2005

T2 - 20th Annual IEEE Symposium on Logic in Computer Science, LICS 2005

Y2 - 26 June 2005 through 29 June 2005

ER -

Certifying compilation for a language with stack allocation

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this