Article

The logical approach to stack typing

Authors:

David WalkerAuthors Info & Claims

TLDI '03: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation

Pages 74 - 85

https://doi.org/10.1145/604174.604185

Published: 18 January 2003 Publication History

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.

References

[1]

A. Ahmed, L. Jia, and D. Walker. Reasoning about hierarchical memory management. Unpublished manuscript., Nov. 2002.]]

[2]

A. W. Appel. Foundational proof-carrying code. In Sixteenth Annual IEEE Symposium on Logic in Computer Science, pages 247--258. IEEE, 2001.]]

Digital Library

[3]

A. W. Appel and A. P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Twenty-seventh ACM Symposium on Principles of Programming Languages, pages 243--253. ACM Press, Jan. 2000.]]

Digital Library

[4]

B.-Y. E. Chang, K. Crary, M. DeLap, R. Harper, J. Liszka, T. M. VII, and F. Pfenning. Trustless grid computing in Concert. In GRID 2002 Workshop, number 2536 in LNCS. Springer-Verlag, 2002.]]

Digital Library

[5]

J. Chirimar, C. A. Gunter, and J. G. Riecke. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming, 6(2):195--244, Mar. 1996.]]

[6]

K. Crary and J. Vanderwaart. An expressive, scalable type theory for certified code. In ACM International Conference on Functional Programming, Pittsburgh, Oct. 2002. ACM Press.]]

Digital Library

[7]

R. Deline and M. Fähndrich. Enforcing high-level protocols in low-level software. In ACM Conference on Programming Language Design and Implementation, pages 59--69, Snowbird, Utah, June 2001. ACM Press.]]

Digital Library

[8]

M. Elsman and N. Hallenberg. A region-based abstract machine for the ML Kit. Technical Report TR-2002-18, Royal Veterinary and Agricultural University of Denmark and IT University of Copenhagen, August 2002. IT University Technical Report Series.]]

[9]

J.-Y. Girard. Linear logic. Theoretical Computer Science, 50:1--102, 1987.]]

Digital Library

[10]

D. Grossman, G. Morrisett, T. Jim, M. Hicks, Y. Wang, and J. Cheney. Region-based memory management in cyclone. In ACM Conference on Programming Language Design and Implementation, Berlin, June 2002. ACM Press.]]

Digital Library

[11]

M. Hofmann. A type system for bounded space and functional in-place update--extended abstract. In G. Smolka, editor, European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 165--179, Berlin, Mar. 2000.]]

Digital Library

[12]

S. Ishtiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In Twenty-Eighth ACM Symposium on Principles of Programming Languages, pages 14--26, London, UK, Jan. 2001.]]

Digital Library

[13]

Y. Lafont. The linear abstract machine. Theoretical Computer Science, 59:157--180, 1988.]]

Digital Library

[14]

T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, 1996.]]

Digital Library

[15]

G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based Typed Assembly Language. In Second International Workshop on Types in Compilation, pages 95--117, Kyoto, Mar. 1998. Published in Xavier Leroy and Atsushi Ohori, editors, Lecture Notes in Computer Science, volume 1473, pages 28--52. Springer-Verlag, 1998.]]

Digital Library

[16]

G. Morrisett, K. Crary, N. Glew, and D. Walker. Stack-based Typed Assembly Language. Journal of Functional Programming, 12(1):43--88, Jan. 2002.]]

Digital Library

[17]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to Typed Assembly Language. ACM Transactions on Programming Languages and Systems, 3(21):528--569, May 1999.]]

Digital Library

[18]

G. Necula. Proof-carrying code. In Twenty-Fourth ACM Symposium on Principles of Programming Languages, pages 106--119, Paris, 1997.]]

Digital Library

[19]

G. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proceedings of Operating System Design and Implementation, pages 229--243, Seattle, Oct. 1996.]]

Digital Library

[20]

R. O'Callahan. A simple, comprehensive type system for java bytecode subroutines. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 70--78, San Antonio, Jan. 1999.]]

Digital Library

[21]

P. O'Hearn. On bunched typing. Journal of Functional Programming, 2002. To appear.]]

Digital Library

[22]

P. O'Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215--24, 1999.]]

[23]

P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In Computer Science Logic, number 2142 in LNCS, pages 1--19, Paris, 2001.]]

Digital Library

[24]

P. O'Hearn and J. C. Reynolds. From Algol to polymorphic linear lambda-calculus. Journal of the ACM, 47(1):167--223, 2000.]]

Digital Library

[25]

L. Petersen, R. Harper, K. Crary, and F. Pfenning. A type theory for memory allocation and data layout. In ACM Symposium on Principles of Programming Languages, Jan. 2003. To appear.]]

Digital Library

[26]

F. Pfenning and R. Davies. A judgment reconstruction of modal logic. Mathematical Structures in Computer Science, 2000. To appear.]]

Digital Library

[27]

J. Polakow. Ordered Linear Logic and Applications. PhD thesis, Carnegie Mellon University, 2001. Available As Technical Report CMU-CS-01-152.]]

Digital Library

[28]

J. Polakow and F. Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 295--309, Berlin, 1999. Springer-Verlag.]]

[29]

J. Polakow and F. Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. Electronic Notes in Theoretical Computer Science, 20, 1999.]]

[30]

J. Polakow and F. Pfenning. Properties of terms in continuation-passing style in an ordered logical framework. In Workshop on Logical Frameworks and Meta-Languages, Santa Barbara, June 2000.]]

[31]

J. Reynolds. Using functor categories to generate intermediate code. In Twenty-Second ACM Symposium on Principles of Programming Languages, pages 25--36, San Francisco, Jan. 1995.]]

Digital Library

[32]

J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial perspectives in computer science, Palgrove, 2000.]]

[33]

SETI@Home. http://setiathome.ssl.berkeley.edu.]]

[34]

Z. Shao, B. Saha, V. Trifonov, and N. Papaspyrou. A type system for certified binaries. In ACM Symposium on Principles of Programming Languages, London, Jan. 2002. ACM Press.]]

Digital Library

[35]

F. Smith, D. Walker, and G. Morrisett. Alias types. In European Symposium on Programming, pages 366--381, Berlin, Mar. 2000.]]

Digital Library

[36]

M. Tofte, L. Birkedal, M. Elsman, N. Hallenberg, T. H. Olesen, P. Sestoft, and P. Bertelsen. Programming with regions in the ML Kit (for version 3). Technical Report 98/25, Computer Science Department, University of Copenhagen, 1998.]]

[37]

M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109--176, 1997.]]

Digital Library

[38]

P. Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Progarmming Concepts and Methods, Sea of Galilee, Israel, Apr. 1990. North Holland. IFIP TC 2 Working Conference.]]

[39]

D. Walker. Typed Memory Management. PhD thesis, Cornell University, Jan. 2001.]]

Digital Library

[40]

D. Walker, K. Crary, and G. Morrisett. Typed memory management in a calculus of capabilities. ACM Transactions on Programming Languages and Systems, 22(4):701--771, May 2000.]]

Digital Library

[41]

D. Walker and G. Morrisett. Alias types for recursive data structures. In Workshop on Types in Compilation, Montreal, Sept. 2000.]]

Digital Library

[42]

H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In ACM Conference on Programming Language Design and Implementation, pages 249--257, Montreal, June 1998.]]

Digital Library

Cited By

Thielecke H(2019)From control effects to typed continuation passingACM SIGPLAN Notices10.1145/640128.60414438:1(139-149)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/640128.604144
Feng XShao ZVaynberg AXiang SNi Z(2019)Modular verification of assembly code with stack-based control abstractionsACM SIGPLAN Notices10.1145/1133255.113402841:6(401-414)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/1133255.1134028
Yu DShao Z(2019)Verification of safety properties for concurrent assembly codeACM SIGPLAN Notices10.1145/1016848.101687539:9(175-188)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/1016848.1016875
Show More Cited By

Index Terms

The logical approach to stack typing
1. Software and its engineering
  1. Software notations and tools
    1. Formal language definitions
2. Theory of computation

Recommendations

The logical approach to stack typing

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 ...
Semantical Analysis of the Logic of Bunched Implications
Abstract
We give a novel approach to proving soundness and completeness for a logic (henceforth: the object-logic) that bypasses truth-in-a-model to work directly with validity. Instead of working with specific worlds in specific models, we reason with ...
Bunched Logics Displayed

We formulate a unified display calculus proof theory for the four principal varieties of bunched logic by combining display calculi for their component logics. Our calculi satisfy cut-elimination, and are sound and complete with respect to their ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

TLDI '03: Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation

January 2003

144 pages

ISBN:1581136498

DOI:10.1145/604174

General Chair:
Zhong Shao
Yale University
,
Program Chair:
Peter Lee
Carnegie Mellon University

ACM SIGPLAN Notices Volume 38, Issue 3
March 2003
134 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/640136
Issue’s Table of Contents

Copyright © 2003 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 January 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

TLDI03

Sponsor:

TLDI03: International Workshop on Types in Language Design and Implementation 2003

January 18, 2003

Louisiana, New Orleans, USA

Acceptance Rates

TLDI '03 Paper Acceptance Rate 11 of 26 submissions, 42%;

Overall Acceptance Rate 11 of 26 submissions, 42%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

17
Total Citations
View Citations
363
Total Downloads

Downloads (Last 12 months)4
Downloads (Last 6 weeks)1

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Thielecke H(2019)From control effects to typed continuation passingACM SIGPLAN Notices10.1145/640128.60414438:1(139-149)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/640128.604144
Feng XShao ZVaynberg AXiang SNi Z(2019)Modular verification of assembly code with stack-based control abstractionsACM SIGPLAN Notices10.1145/1133255.113402841:6(401-414)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/1133255.1134028
Yu DShao Z(2019)Verification of safety properties for concurrent assembly codeACM SIGPLAN Notices10.1145/1016848.101687539:9(175-188)Online publication date: 27-Feb-2019
https://dl.acm.org/doi/10.1145/1016848.1016875
Vorreiter Pedersen MAskarov A(2019)Static Enforcement of Security in Runtime Systems2019 IEEE 32nd Computer Security Foundations Symposium (CSF)10.1109/CSF.2019.00030(335-33515)Online publication date: Jun-2019
https://doi.org/10.1109/CSF.2019.00030
Jiang XGuo YChen Y(2009)The Logical Approach to Low-Level Stack ReasoningProceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering10.1109/TASE.2009.17(209-216)Online publication date: 29-Jul-2009
https://dl.acm.org/doi/10.1109/TASE.2009.17
Nita MGrossman DChambers C(2008)A theory of platform-dependent low-level softwareACM SIGPLAN Notices10.1145/1328897.132846543:1(209-220)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.1145/1328897.1328465
Nita MGrossman DChambers CNecula GWadler P(2008)A theory of platform-dependent low-level softwareProceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1328438.1328465(209-220)Online publication date: 7-Jan-2008
https://dl.acm.org/doi/10.1145/1328438.1328465
Perry FJia LWalker DJarzabek SSchmidt DVeldhuizen T(2006)Expressing heap-shape contracts in linear logicProceedings of the 5th international conference on Generative programming and component engineering10.1145/1173706.1173723(101-110)Online publication date: 22-Oct-2006
https://dl.acm.org/doi/10.1145/1173706.1173723
Feng XShao ZVaynberg AXiang SNi ZSchwartzbach MBall T(2006)Modular verification of assembly code with stack-based control abstractionsProceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1133981.1134028(401-414)Online publication date: 11-Jun-2006
https://dl.acm.org/doi/10.1145/1133981.1134028
Ni ZShao Z(2006)Certified assembly programming with embedded code pointersACM SIGPLAN Notices10.1145/1111320.111106641:1(320-333)Online publication date: 11-Jan-2006
https://dl.acm.org/doi/10.1145/1111320.1111066
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents