Article

Stratified operational semantics for safety and correctness of the region calculus

Author:

Cristiano CalcagnoAuthors Info & Claims

POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 155 - 165

https://doi.org/10.1145/360204.360217

Published: 01 January 2001 Publication History

Abstract

The region analysis of Tofte and Talpin is an attempt to determine statically the life span of dynamically allocated objects. But the calculus is at once intuitively simple, yet deceptively subtle, and previous theoretical analyses have been frustratingly complex: no analysis has revealed and explained in simple terms the connection between the subleties of the calculus and the imperative features it builds on. We present a novel approach for proving safety and correctness of a simplified version of the region calculus. We give a stratified operational semantics, composed of a highlevel semantics dealing with the conceptual difficulties of effect annotations, and a low-level one with explicit operations on a region-indexed store. The main results of the paper are a proof simpler than previous ones, and a modular approach to type safety and correctness. The flexibility of this approach is demonstrated by the simplicity of the extension to the full calculus with type and region polymorphism.

References

[1]

A. Aiken, M. Fahndrich, and R. Levien. Better static memory management: Improving region-based analysis of higher-order languages. In ACM SIGPLAN Conference on Programming Language Design and Implementation", pages 174-185, 1995. La Jolla, California.]]

Digital Library

[2]

A. Banerjee, N. Heintze, and J. G. Riecke. Region analysis and the polymorphic lambda calculus. In Fourteenth IEEE Symposium on Logic in Computer Science, pages 88-97. IEEE Computer Society Press, 1999.]]

Digital Library

[3]

N. Benton and A. Kennedy. Monads, effects and transformations. In Third International Workshop on Higher Order Operational Techniques in Semantics (HOOTS), 1999. Paris, France.]]

[4]

N. Benton, A. Kennedy, and G. Russel. Compiling Standard ML to Java bytecodes. In Proceedings of the 3rd ACM SIGPLAN Conference on Functional Programming, 1998.]]

Digital Library

[5]

L. Birkedal and M. Tofte. A constraint-based region inference algorithm. Theoretical Computer Science, 1998.]]

Digital Library

[6]

L. Birkedal, M. Tofte, and M. Vejlstrup. From region inference to yon Neumann machines via region representation inference. In Proceedings of the 23- rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 171-183. ACM Press, 1996.]]

Digital Library

[7]

R. Bornat. Proving pointer programs in Hoare logic. To appear in Mathematics of Program Construction, 2000.]]

Digital Library

[8]

C. Calcagno, S. Ishtiaq, and P. W. OHearn. Semantic analysis of pointer aliasing, allocation and disposal in Hoare logic. To appear in Principles and Practice of Declarative Programming (PPDP 2000), Montreal, September 2000.]]

Digital Library

[9]

K. Crary, D. Walker, and G. Morrisett. Typed memory management in a calculus of capabilities. In Twenty-Sixth Symposium on Principles of Programming Languages (POPL), pages 262-275, January 1999. San Antonio, TX, USA.]]

Digital Library

[10]

S. dal Zilio and A. Gordon. Region analysis and a 7r-calculus with groups. In MFCS 2000: the Z5th International Symposium on Mathematical Foundations of Computer Science, August 2000.]]

Digital Library

[11]

S. Helsen and P. Thiemann. Syntactic type soundness for the region calculus. In Workshop on Higher Order Operational Techniques in Semantics, HOOTS. Volume 41 of Electronic Notes in Theoretical Computer Science, Montreal, Canada, September 2000.]]

[12]

S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. Manuscript, March 2000.]]

[13]

J. Lucassen and D. Gifford. Polymorphic effect systems. In Proceedings of the 1988 ACM conference on Principles of programming languages, 1988.]]

Digital Library

[14]

G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to Typed Assembly Language. In Twenty-Filth ACM Symposium on Principles of Programming Languages, 1998.]]

Digital Library

[15]

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

Digital Library

[16]

J. C. Reynolds. Intuitionistic reasoning about shared mutable data structure. To appear in the Proceedings of the Symposium in Celebration of the Work of C.A.R. Hoare, 2000.]]

[17]

J. Talpin and P. Jouvelot. Polymorphic typed region and effect inference. Journal of Functional Programming, 2(3), 1992.]]

[18]

M. Tofte and L. Birkedal. A region inference algorithm. ACM Transactions on Programming Languages and Systems, 20(4):734-767, July 1998.]]

Digital Library

[19]

M. Tofte and J. Talpin. Implementation of the typed call-by-value lambda calculus using a stack of regions. In ACM Symposium on Principles of Programming Languages (POPL'94). ACM Press, January 1994.]]

Digital Library

[20]

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

Digital Library

Cited By

Pearce D(2021)A Lightweight Formalism for Reference Lifetimes and Borrowing in RustACM Transactions on Programming Languages and Systems10.1145/344342043:1(1-73)Online publication date: 17-Apr-2021
https://dl.acm.org/doi/10.1145/3443420
Boudol G(2008)Typing safe deallocationProceedings of the Theory and practice of software, 17th European conference on Programming languages and systems10.5555/1792878.1792891(116-130)Online publication date: 29-Mar-2008
https://dl.acm.org/doi/10.5555/1792878.1792891
Craciun FQin SChin W(2008)A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented ParadigmProceedings of the 10th International Conference on Formal Methods and Software Engineering10.1007/978-3-540-88194-0_10(126-146)Online publication date: 27-Oct-2008
https://dl.acm.org/doi/10.1007/978-3-540-88194-0_10
Show More Cited By

Index Terms

Recommendations

Stratified operational semantics for safety and correctness of the region calculus

The region analysis of Tofte and Talpin is an attempt to determine statically the life span of dynamically allocated objects. But the calculus is at once intuitively simple, yet deceptively subtle, and previous theoretical analyses have been ...
Coinductive big-step operational semantics

Using a call-by-value functional language as an example, this article illustrates the use of coinductive definitions and proofs in big-step operational semantics, enabling it to describe diverging evaluations in addition to terminating evaluations. We ...
A Fixpoint Semantics and an SLD-Resolution Calculus for Modal Logic Programs

We propose a modal logic programming language called MProlog, which is as expressive as the general modal Horn fragment. We give a fixpoint semantics and an SLD-resolution calculus for MProlog in all of the basic serial modal logics KD, T, KDB, B, KD4, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '01: Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2001

304 pages

ISBN:1581133367

DOI:10.1145/360204

Chairmen:
Chris Hankin
Imperial College, London, U. K.
,
Dave Schmidt
Kansas State Univ., Manhattan

ACM SIGPLAN Notices Volume 36, Issue 3
March 2001
303 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/373243
Editors:
Cindy Norris
Appalachian State Univ., Boone, NC
,
James B. Fenwick
Appalachian State Univ., Boone, NC
Issue’s Table of Contents

Copyright © 2001 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: 01 January 2001

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL01

Sponsor:

POPL01: The 28th Annual ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages

London, United Kingdom

Acceptance Rates

POPL '01 Paper Acceptance Rate 24 of 126 submissions, 19%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

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

19
Total Citations
View Citations
300
Total Downloads

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

Reflects downloads up to 24 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Pearce D(2021)A Lightweight Formalism for Reference Lifetimes and Borrowing in RustACM Transactions on Programming Languages and Systems10.1145/344342043:1(1-73)Online publication date: 17-Apr-2021
https://dl.acm.org/doi/10.1145/3443420
Boudol G(2008)Typing safe deallocationProceedings of the Theory and practice of software, 17th European conference on Programming languages and systems10.5555/1792878.1792891(116-130)Online publication date: 29-Mar-2008
https://dl.acm.org/doi/10.5555/1792878.1792891
Craciun FQin SChin W(2008)A Formal Soundness Proof of Region-Based Memory Management for Object-Oriented ParadigmProceedings of the 10th International Conference on Formal Methods and Software Engineering10.1007/978-3-540-88194-0_10(126-146)Online publication date: 27-Oct-2008
https://dl.acm.org/doi/10.1007/978-3-540-88194-0_10
Boudol G(2008)Typing Safe DeallocationProgramming Languages and Systems10.1007/978-3-540-78739-6_10(116-130)Online publication date: 2008
https://doi.org/10.1007/978-3-540-78739-6_10
Neamtiu IHicks MStoyle GOriol MSchwartzbach MBall T(2006)Practical dynamic software updating for CProceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/1133981.1133991(72-83)Online publication date: 11-Jun-2006
https://dl.acm.org/doi/10.1145/1133981.1133991
Neamtiu IHicks MStoyle GOriol M(2006)Practical dynamic software updating for CACM SIGPLAN Notices10.1145/1133255.113399141:6(72-83)Online publication date: 11-Jun-2006
https://dl.acm.org/doi/10.1145/1133255.1133991
Fluet MMorrisett GOkasaki CFisher K(2004)Monadic regionsProceedings of the ninth ACM SIGPLAN international conference on Functional programming10.1145/1016850.1016867(103-114)Online publication date: 19-Sep-2004
https://dl.acm.org/doi/10.1145/1016850.1016867
Fluet MMorrisett G(2004)Monadic regionsACM SIGPLAN Notices10.1145/1016848.101686739:9(103-114)Online publication date: 19-Sep-2004
https://dl.acm.org/doi/10.1145/1016848.1016867
Tofte MBirkedal LElsman MHallenberg N(2004)A Retrospective on Region-Based Memory ManagementHigher-Order and Symbolic Computation10.1023/B:LISP.0000029446.78563.a417:3(245-265)Online publication date: 1-Sep-2004
https://dl.acm.org/doi/10.1023/B%3ALISP.0000029446.78563.a4
Aiken AFoster JKodumal JTerauchi TCytron RGupta R(2003)Checking and inferring local non-aliasingProceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation10.1145/781131.781146(129-140)Online publication date: 9-Jun-2003
https://dl.acm.org/doi/10.1145/781131.781146
Show More Cited By

View Options

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