More Web Proxy on the site http://driver.im/

research-article

The essence of monotonic state

Authors:

Alexandre Pilkiewicz,

François PottierAuthors Info & Claims

TLDI '11: Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation

Pages 73 - 86

https://doi.org/10.1145/1929553.1929565

Published: 25 January 2011 Publication History

Abstract

We extend a static type-and-capability system with new mechanisms for expressing the promise that a certain abstract value evolves monotonically with time; for enforcing this promise; and for taking advantage of this promise to establish non-trivial properties of programs. These mechanisms are independent of the treatment of mutable state, but combine with it to offer a flexible account of "monotonic state".

We apply these mechanisms to solve two reasoning challenges that involve mutable state. First, we show how an implementation of thunks in terms of references can be assigned types that reflect time complexity properties, in the style of Danielsson (2008). Second, we show how an implementation of hash-consing can be assigned a specification that conceals the existence of an internal state yet guarantees that two pieces of input data receive the same hash code if and only if they are equal.

References

[1]

Amal Ahmed, Derek Dreyer, and Andreas Rossberg. http://ttic.uchicago.edu/~amal/papers/sdri.pdf State-dependent representation independence. In ACM Symposium on Principles of Programming Languages (POPL), pages 340--353, January 2009.

Digital Library

[2]

Robert Atkey. http://personal.cis.strath.ac.uk/~raa/amortised-sep-logic.pdf Amortised resource analysis with separation logic. In European Symposium on Programming (ESOP), volume 6012 of Lecture Notes in Computer Science, pages 85--103. Springer, 2010.

Digital Library

[3]

Arthur Charguéraud and François Pottier. http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-capabilit%ies.pdf Functional translation of a calculus of capabilities. In ACM International Conference on Functional Programming (ICFP), pages 213--224, September 2008.

Digital Library

[4]

Karl Crary, David Walker, and Greg Morrisett. http://www.cs.cornell.edu/talc/papers/capabilities.pdf Typed memory management in a calculus of capabilities. In ACM Symposium on Principles of Programming Languages (POPL), pages 262--275, January 1999.

Digital Library

[5]

Karl Crary and Stephanie Weirich. http://www.cs.cornell.edu/talc/papers/resource_bound/res.pdf Resource bound certification. In ACM Symposium on Principles of Programming Languages (POPL), pages 184--198, January 2000.

Digital Library

[6]

Nils Anders Danielsson. http://www.cs.chalmers.se/~nad/publications/danielsson-popl2008.pdf Lightweight semiformal time complexity analysis for purely functional data structures. In ACM Symposium on Principles of Programming Languages (POPL), January 2008.

Digital Library

[7]

Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis. http://ttic.uchicago.edu/~feng/research/publications/DG.pdf Deny-guarantee reasoning. In European Symposium on Programming (ESOP), volume 5502 of Lecture Notes in Computer Science, pages 363--377. Springer, March 2009.

Digital Library

[8]

Vincent Dornic, Pierre Jouvelot, and David K. Gifford. https://eprints.kfupm.edu.sa/58299/1/58299.pdf Polymorphic time systems for estimating program complexity. ACM Letters on Programming Languages and Systems, 1(1):33--45, 1992.

Digital Library

[9]

Derek Dreyer, Georg Neis, and Lars Birkedal. http://www.itu.dk/~birkedal/papers/stslr-conf.pdf The impact of higher-order state and control effects on local relational reasoning. In ACM International Conference on Functional Programming (ICFP), pages 143--156, September 2010.

Digital Library

[10]

Manuel Fähndrich and Rustan Leino. http://research.microsoft.com/en-us/um/people/leino/papers/krml123.pdf Heap monotonic typestates. In International Workshop on Alias Confinement and Ownership (IWACO), July 2003.

[11]

Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. http://ftp.research.microsoft.com/pub/tr/TR-2007-39.pdf Local reasoning for storable locks and threads. Technical Report MSR-TR-2007-39, Microsoft Research, September 2007.

[12]

Eric C. R. Hehner. http://www.cs.toronto.edu/~hehner/AoT.pdf Abstractions of Time, pages 191--210. Prentice Hall, 1994.

Digital Library

[13]

Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. http://www.cs.princeton.edu/~appel/papers/concurrent.pdf Oracle semantics for concurrent separation logic. In European Symposium on Programming (ESOP), volume 4960 of Lecture Notes in Computer Science, pages 353--367. Springer, April 2008.

Digital Library

[14]

Martin Hofmann. http://www.tcs.informatik.uni-muenchen.de/~mhofmann/nordic.ps.gz A type system for bounded space and functional in-place update. Nordic Journal of Computing, 7(4):258--289, 2000.

Digital Library

[15]

Gary T. Leavens and Albert L. Baker. http://dx.doi.org/10.1007/3-540-48118-4_8 Enhancing the pre- and postcondition technique for more expressive specifications. In Formal Methods (FM), volume 1709 of Lecture Notes in Computer Science, pages 1087--1106. Springer, January 1999.

Digital Library

[16]

Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. http://www.jmlspecs.org/OldReleases/jmlrefman.pdf JML Reference Manual, May 2008.

[17]

K. Rustan M. Leino and Wolfram Schulte. http://research.microsoft.com/en-us/um/people/leino/papers/krml166.pdf Using history invariants to verify observers. In European Symposium on Programming (ESOP), volume 4421 of Lecture Notes in Computer Science, pages 80--94. Springer, 2007.

Digital Library

[18]

Barbara Liskov and Jeannette M. Wing. http://www.cs.cmu.edu/~wing/publications/LiskovWing94.pdf A behavioral notion of subtyping. ACM Transactions on Programming Languages and Systems, 16(6):1811--1841, 1994.

Digital Library

[19]

Karl Mazurak, Jianzhou Zhao, and Steve Zdancewic. http://www.cis.upenn.edu/~stevez/papers/MZZ10.pdf Lightweight linear types in system Fº. In Workshop on Types in Language Design and Implementation (TLDI), pages 77--88, January 2010.

Digital Library

[20]

Aleksandar Nanevski, Amal Ahmed, Greg Morrisett, and Lars Birkedal. http://www.eecs.harvard.edu/~aleks/papers/hoarelogic/esop07.pdf Abstract predicates and mutable ADTs in Hoare type theory. In European Symposium on Programming (ESOP), volume 4421 of Lecture Notes in Computer Science, pages 189--204. Springer, March 2007.

Digital Library

[21]

Peter W. O'Hearn. http://www.dcs.qmul.ac.uk/~ohearn/papers/concurrency.pdf Resources, concurrency and local reasoning. Theoretical Computer Science, 375(1--3):271--307, May 2007.

Digital Library

[22]

Chris Okasaki. http://www.cambridge.org/us/catalogue/catalogue.asp?isbn=0521663504 Purely Functional Data Structures. Cambridge University Press, 1999.

Digital Library

[23]

Benjamin C. Pierce and David N. Turner. http://www.cis.upenn.edu/~bcpierce/papers/oop.ps Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207--247, April 1994.

[24]

François Pottier. http://gallium.inria.fr/~fpottier/publis/fpottier-antiframe-2008.pdf Hiding local state in direct style: a higher-order anti-frame rule. In IEEE Symposium on Logic in Computer Science (LICS), pages 331--340, June 2008.

Digital Library

[25]

François Pottier. http://gallium.inria.fr/~fpottier/publis/fpottier-gaf-2009.pdf Generalizing the higher-order frame and anti-frame rules. Unpublished, July 2009.

[26]

François Pottier. http://gallium.inria.fr/~fpottier/publis/fpottier-caf-2009.pdf Three comments on the anti-frame rule. Unpublished, July 2009.

[27]

Brian Reistad and David K. Gifford. http://doi.acm.org/10.1145/182409.182439 Static dependent costs for estimating execution time. In ACM Symposium on Lisp and Functional Programming (LFP), pages 65--78, 1994.

Digital Library

[28]

Fred B. Schneider. On Concurrent Programming. Springer, 1997.

Digital Library

[29]

Frederick Smith, David Walker, and Greg Morrisett. http://www.cs.cornell.edu/talc/papers/alias.pdf Alias types. In European Symposium on Programming (ESOP), volume 1782 of Lecture Notes in Computer Science, pages 366--381. Springer, March 2000.

Digital Library

[30]

Eijiro Sumii. http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/poly-ref.pdf A complete characterization of observational equivalence in polymorphic lambda-calculus with general references. In Computer Science Logic, volume 5771 of Lecture Notes in Computer Science, pages 455--469. Springer, September 2009.

Digital Library

[31]

Robert~Endre Tarjan. http://dx.doi.org/10.1137/0606031 Amortized computational complexity. SIAM Journal on Algebraic and Discrete Methods, 6(2):306--318, 1985.

Digital Library

[32]

Hongwei Xi. http://www.cs.bu.edu/~hwxi/academic/papers/JFPdml.pdf Dependent ML: an approach to practical programming with dependent types. Journal of Functional Programming, 17(2):215--286, 2007.

Digital Library

Cited By

Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
Pottier FGuéneau AJourdan JMével G(2024)Thunks and Debits in Separation Logic with Time CreditsProceedings of the ACM on Programming Languages10.1145/36328928:POPL(1482-1508)Online publication date: 5-Jan-2024
https://doi.org/10.1145/3632892
Arasu ARamananandro TRastogi ASwamy NFromherz AHietala KParno BRamamurthy RKrebbers RTraytel DPientka BZdancewic S(2023)FastVer2: A Provably Correct Monitor for Concurrent, Key-Value StoresProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575687(30-46)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575687
Show More Cited By

Index Terms

The essence of monotonic state
1. Theory of computation
  1. Logic
    1. Programming logic
  2. Semantics and reasoning
    1. Program constructs
      1. Type structures
    2. Program reasoning

Recommendations

Should your specification language be typed

Most specification languages have a type system. Type systems are hard to get right, and getting them wrong can lead to inconsistencies. Set theory can serve as the basis for a specification language without types. This possibility, which has been widely ...
Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect
OOPSLA '16

First-class functions dramatically increase expressiveness, at the expense of static guarantees. In ALGOL or PASCAL, functions could be passed as arguments but never escape their defining scope. Therefore, function arguments could serve as temporary ...
ML^F for everyone (users, implementers, and designers)
ML '07: Proceedings of the 2007 workshop on Workshop on ML

ML^F is an alternative to ML that permits second-order polymorphism as in System F but retains (partial) type inference a la ML. Type annotations are requested only on parameters of functions that are used polymorphically. Type abstractions and type ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

TLDI '11: Proceedings of the 7th ACM SIGPLAN workshop on Types in language design and implementation

January 2011

94 pages

ISBN:9781450304849

DOI:10.1145/1929553

General Chair:
Stephanie Weirich
University of Pennsylvania
,
Program Chair:
Derek Dreyer
MPI-SWS, Germany

Copyright © 2011 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

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '11

Sponsor:

SIGPLAN

POPL '11: The 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

January 25, 2011

Texas, Austin, USA

Acceptance Rates

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

25
Total Citations
View Citations
113
Total Downloads

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

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Campion MDalla Preda MGiacobazzi RUrban C(2024)Monotonicity and the Precision of Program AnalysisProceedings of the ACM on Programming Languages10.1145/36328978:POPL(1629-1662)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632897
Pottier FGuéneau AJourdan JMével G(2024)Thunks and Debits in Separation Logic with Time CreditsProceedings of the ACM on Programming Languages10.1145/36328928:POPL(1482-1508)Online publication date: 5-Jan-2024
https://doi.org/10.1145/3632892
Arasu ARamananandro TRastogi ASwamy NFromherz AHietala KParno BRamamurthy RKrebbers RTraytel DPientka BZdancewic S(2023)FastVer2: A Provably Correct Monitor for Concurrent, Key-Value StoresProceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3573105.3575687(30-46)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3573105.3575687
Sun KChen SWang MHao D(2023)What Types Are Needed for Typing Dynamic Objects? A Python-Based Empirical StudyProgramming Languages and Systems10.1007/978-981-99-8311-7_2(24-45)Online publication date: 21-Nov-2023
https://doi.org/10.1007/978-981-99-8311-7_2
Timany ABirkedal LHriţcu CPopescu A(2021)Reasoning about monotonicity in separation logicProceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3437992.3439931(91-104)Online publication date: 17-Jan-2021
https://dl.acm.org/doi/10.1145/3437992.3439931
Charguéraud APottier F(2019)Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time CreditsJournal of Automated Reasoning10.1007/s10817-017-9431-762:3(331-365)Online publication date: 1-Mar-2019
https://dl.acm.org/doi/10.1007/s10817-017-9431-7
Guéneau ACharguéraud APottier F(2018)A Fistful of Dollars: Formalizing Asymptotic Complexity Claims via Deductive Program VerificationProgramming Languages and Systems10.1007/978-3-319-89884-1_19(533-560)Online publication date: 14-Apr-2018
https://doi.org/10.1007/978-3-319-89884-1_19
Ahman DFournet CHriţcu CMaillard KRastogi ASwamy N(2017)Recalling a witness: foundations and applications of monotonic stateProceedings of the ACM on Programming Languages10.1145/31581532:POPL(1-30)Online publication date: 27-Dec-2017
https://dl.acm.org/doi/10.1145/3158153
Krebbers RTimany ABirkedal L(2017)Interactive proofs in higher-order concurrent separation logicACM SIGPLAN Notices10.1145/3093333.300985552:1(205-217)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009855
Gordon CErnst MGrossman DParkinson M(2017)Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement TypesACM Transactions on Programming Languages and Systems10.1145/306485039:3(1-54)Online publication date: 10-May-2017
https://dl.acm.org/doi/10.1145/3064850
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