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

Imported 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

33 Documents citing this article

Andrew Wagner;Zachary Eisbach;Amal Ahmed, 2024, Realistic Realizability: Specifying ABIs You Can Count On, Proceedings of the ACM on Programming Languages, 8, OOPSLA2, pp. 1249-1278, 10.1145/3689755, https://doi.org/10.1145/3689755.

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.

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, ACM SIGPLAN Notices, 50, 1, pp. 3-16, 10.1145/2775051.2676970.

Bernhard Reus;Nathaniel Charlton;Ben Horsfall, 2014, Symbolic Execution Proofs for Higher Order Store Programs, Journal of Automated Reasoning, 54, 3, pp. 199-284, 10.1007/s10817-014-9319-8.

Paul-André Melliès;Noam Zeilberger, 2014, Functors are Type Refinement Systems, pp. 3-16, 10.1145/2676726.2676970, https://inria.hal.science/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, 2013, High-level separation logic for low-level code, Research Portal (King's College London), pp. 301-314, 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, ACM SIGPLAN Notices, 47, 1, pp. 59-72, 10.1145/2103621.2103666.

David Costanzo;Zhong Shao, 2012, A Case for Behavior-Preserving Actions in Separation Logic, Lecture notes in computer science, pp. 332-349, 10.1007/978-3-642-35182-2_24.

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, Mathematical Structures in Computer Science, 23, 1, pp. 1-54, 10.1017/s0960129512000035.

Jean-Baptiste Jeannin;Dexter Kozen, 2012, Capsules and Separation, 2012 27th Annual IEEE Symposium on Logic in Computer Science, 2303, pp. 425-430, 10.1109/lics.2012.52.

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

Nathaniel Charlton;Ben Horsfall;Bernhard Reus, 2012, Crowfoot: A Verifier for Higher-Order Store Programs, Lecture notes in computer science, pp. 136-151, 10.1007/978-3-642-27940-9_10.

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, Proceedings of the 16th ACM SIGPLAN international conference on Functional programming, pp. 445-456, 10.1145/2034773.2034831.

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.

Jan Schwinghammer;Lars Birkedal;Kristian St ø vring, 2011, A Step-Indexed Kripke Model of Hidden State via Recursive Properties on Recursively Defined Metric Spaces, Lecture notes in computer science, pp. 305-319, 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, ACM SIGPLAN Notices, 46, 1, pp. 119-132, 10.1145/1925844.1926401.

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

David A. Naumann;Anindya Banerjee, 2010, Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions, Lecture notes in computer science, pp. 2-22, 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, 2010, A Semantic Foundation for Hidden State, Lecture notes in computer science, pp. 2-17, 10.1007/978-3-642-12032-9_2, https://doi.org/10.1007/978-3-642-12032-9_2.

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

Jan Schwinghammer;Lars Birkedal;Bernhard Reus;Hongseok Yang, 2009, Nested Hoare Triples and Frame Rules for Higher-Order Store, Lecture notes in computer science, pp. 440-454, 10.1007/978-3-642-04027-6_32.

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, 2008, Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule, Proceedings - Symposium on Logic in Computer Science, pp. 331-340, 10.1109/lics.2008.16.

Lars Birkedal;Bernhard Reus;Jan Schwinghammer;Hongseok Yang, 2008, A Simple Model of Separation Logic for Higher-Order Store, Lecture notes in computer science, pp. 348-360, 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 3766 times.

This article's PDF has been downloaded 477 times.