Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages

Lars Birkedal; Noah Torp-Smith; Hongseok Yang

doi:10.2168/LMCS-2(5:1)2006

Lars Birkedal ; Noah Torp-Smith ; Hongseok Yang - Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages

lmcs:2232 - Logical Methods in Computer Science, November 3, 2006, Volume 2, Issue 5 - https://doi.org/10.2168/LMCS-2(5:1)2006

Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like LanguagesArticle

Authors: Lars Birkedal ; Noah Torp-Smith ; Hongseok Yang

We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame rules, allowing for local reasoning.

https://doi.org/10.2168/LMCS-2(5:1)2006

Source: arXiv.org:cs/0610081

Volume: Volume 2, Issue 5

Published on: November 3, 2006

Submitted on: December 21, 2005

Keywords: Computer Science - Logic in Computer Science,F.3,D.3

Licence: arXiv.org - Assumed non-exclusive license to distribute

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

32 Documents citing this article

Alejandro Gadea;Emmanuel Gunther;Miguel Pagano, 2020, Mechanization of coherence and adequacy: Being extrinsic extended to subtyping, Science of Computer Programming, 197, pp. 102512, 10.1016/j.scico.2020.102512, https://doi.org/10.1016/j.scico.2020.102512.

Arthur Charguéraud, 2020, Separation logic for sequential programs (functional pearl), Proceedings of the ACM on Programming Languages, 4, ICFP, pp. 1-34, 10.1145/3408998, https://doi.org/10.1145/3408998.

Lars Birkedal;Guilhem Jaber;Filip Sieczkowski;Jacob Thamsborg, 2016, A Kripke logical relation for effect-based program transformations, Information and Computation, 249, pp. 160-189, 10.1016/j.ic.2016.04.003.

Paul-André Melliès;Noam Zeilberger, 2015, Functors are Type Refinement Systems, 50, 1, pp. 3-16, 10.1145/2775051.2676970, https://hal.inria.fr/hal-01096910.

Bernhard Reus;Nathaniel Charlton;Ben Horsfall, 2014, Symbolic Execution Proofs for Higher Order Store Programs, Sussex Research Online (University of Sussex), 54, 3, pp. 199-284, 10.1007/s10817-014-9319-8, http://sro.sussex.ac.uk/id/eprint/53364/2/paper.pdf.

Paul-André Melliès;Noam Zeilberger, Functors are Type Refinement Systems, 2014, Mumbai India, 10.1145/2676726.2676970, https://hal.inria.fr/hal-01096910.

Anindya Banerjee;David A. Naumann, 2013, Local Reasoning for Global Invariants, Part II, Journal of the ACM, 60, 3, pp. 1-73, 10.1145/2485981, https://doi.org/10.1145/2485981.

Jonas B. Jensen;Nick Benton;Andrew Kennedy, Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, High-level separation logic for low-level code, 2013, Rome Italy, 10.1145/2429069.2429105.

Jonas B. Jensen;Nick Benton;Andrew Kennedy, 2013, High-level separation logic for low-level code, ACM SIGPLAN Notices, 48, 1, pp. 301-314, 10.1145/2480359.2429105.

Thomas Dinsdale-Young;Lars Birkedal;Philippa Gardner;Matthew Parkinson;Hongseok Yang, 2013, Views, ACM SIGPLAN Notices, 48, 1, pp. 287-300, 10.1145/2480359.2429104.

Chung-Kil Hur;Derek Dreyer;Georg Neis;Viktor Vafeiadis, 2012, The marriage of bisimulations and Kripke logical relations, CiteSeer X (The Pennsylvania State University), 47, 1, pp. 59-72, 10.1145/2103621.2103666, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.296.8570.

David Costanzo;Zhong Shao, CiteSeer X (The Pennsylvania State University), A Case for Behavior-Preserving Actions in Separation Logic, pp. 332-349, 2012, 10.1007/978-3-642-35182-2_24, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.407.2754.

FRANÇOIS POTTIER, 2012, Syntactic soundness proof of a type-and-capability system with hidden state, Journal of Functional Programming, 23, 1, pp. 38-144, 10.1017/s0956796812000366, https://doi.org/10.1017/s0956796812000366.

JAN SCHWINGHAMMER;LARS BIRKEDAL;FRANÇOIS POTTIER;BERNHARD REUS;KRISTIAN STØVRING;et al., 2012, A step-indexed Kripke model of hidden state, 23, 1, pp. 1-54, 10.1017/s0960129512000035, https://inria.hal.science/hal-00772757.

Jean-Baptiste Jeannin;Dexter Kozen, CiteSeer X (The Pennsylvania State University), Capsules and Separation, pp. 425-430, 2012, Dubrovnik, Croatia, 10.1109/lics.2012.52, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.228.5151.

Jonas Braband Jensen;Lars Birkedal, Lecture notes in computer science, Fictional Separation Logic, pp. 377-396, 2012, 10.1007/978-3-642-28869-2_19, https://doi.org/10.1007/978-3-642-28869-2_19.

Nathaniel Charlton;Ben Horsfall;Bernhard Reus, OPAL (Open@LaTrobe) (La Trobe University), Crowfoot: A Verifier for Higher-Order Store Programs, pp. 136-151, 2012, 10.1007/978-3-642-27940-9_10, https://figshare.com/articles/chapter/Crowfoot_a_verifier_for_higher-order_store_programs/23378063.

Alexandre Buisse;Lars Birkedal;Kristian Støvring, 2011, Step-Indexed Kripke Model of Separation Logic for Storable Locks, Electronic Notes in Theoretical Computer Science, 276, pp. 121-143, 10.1016/j.entcs.2011.09.018, https://doi.org/10.1016/j.entcs.2011.09.018.

Jacob Thamsborg;Lars Birkedal, 2011, A kripke logical relation for effect-based program transformations, ACM SIGPLAN Notices, 46, 9, pp. 445-456, 10.1145/2034574.2034831.

Jacob Thamsborg;Lars Birkedal, Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, A kripke logical relation for effect-based program transformations, 2011, Tokyo Japan, 10.1145/2034773.2034831.

Jan Schwinghammer;Lars Birkedal;Kristian St ø vring, Lecture notes in computer science, A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces, pp. 305-319, 2011, 10.1007/978-3-642-19805-2_21, https://doi.org/10.1007/978-3-642-19805-2_21.

Lars Birkedal;Bernhard Reus;Jan Schwinghammer;Kristian Støvring;Jacob Thamsborg;et al., 2011, Step-indexed kripke models over recursive worlds, Oxford University Research Archive (ORA) (University of Oxford), 46, 1, pp. 119-132, 10.1145/1925844.1926401, https://ora.ox.ac.uk/objects/uuid:f2d38299-0326-4633-b77e-6f5d3e7ee2ac.

Nathaniel Charlton;Bernhard Reus, Lecture notes in computer science, Specification Patterns and Proofs for Recursion through the Store, pp. 310-321, 2011, 10.1007/978-3-642-22953-4_27.

David A. Naumann;Anindya Banerjee, Lecture notes in computer science, Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions, pp. 2-22, 2010, 10.1007/978-3-642-11957-6_2, https://doi.org/10.1007/978-3-642-11957-6_2.

Derek Dreyer;Georg Neis;Andreas Rossberg;Lars Birkedal, 2010, A relational modal logic for higher-order stateful ADTs, ACM SIGPLAN Notices, 45, 1, pp. 185-198, 10.1145/1707801.1706323.

Jan Schwinghammer;Hongseok Yang;Lars Birkedal;François Pottier;Bernhard Reus, Lecture notes in computer science, A Semantic Foundation for Hidden State, pp. 2-17, 2010, 10.1007/978-3-642-12032-9_2, https://doi.org/10.1007/978-3-642-12032-9_2.

Matthew Parkinson, Lecture notes in computer science, The Next 700 Separation Logics, pp. 169-182, 2010, 10.1007/978-3-642-15057-9_12.

Jan Schwinghammer;Lars Birkedal;Bernhard Reus;Hongseok Yang, arXiv (Cornell University), Nested Hoare Triples and Frame Rules for Higher-Order Store, pp. 440-454, 2009, 10.1007/978-3-642-04027-6_32, http://arxiv.org/abs/1109.3031.

ROBERT ATKEY, 2009, Parameterised notions of computation, Journal of Functional Programming, 19, 3-4, pp. 335-376, 10.1017/s095679680900728x, https://doi.org/10.1017/s095679680900728x.

Francois Pottier, Proceedings - Symposium on Logic in Computer Science, Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule, pp. 331-340, 2008, Pittsburgh, PA, USA, 10.1109/lics.2008.16.

Lars Birkedal;Bernhard Reus;Jan Schwinghammer;Hongseok Yang, Lecture notes in computer science, A Simple Model of Separation Logic for Higher-Order Store, pp. 348-360, 2008, 10.1007/978-3-540-70583-3_29.

David A. Naumann, 2006, On assertion-based encapsulation for object invariants and simulations, Formal Aspects of Computing, 19, 2, pp. 205-224, 10.1007/s00165-006-0020-5, https://doi.org/10.1007/s00165-006-0020-5.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 2438 times.

This article's PDF has been downloaded 364 times.