 |
 |
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)2006Semantics of Separation-Logic Typing and Higher-order Frame Rules
for<br> Algol-like LanguagesArticle
Authors: Lars Birkedal ; Noah Torp-Smith ; Hongseok Yang NULL##NULL##NULLLars 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.
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
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 (Print), 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 & Computation, 249, pp. 160-189, 10.1016/j.ic.2016.04.003. - MellièsPaul-André;ZeilbergerNoam, 2015, Functors are Type Refinement Systems, 50, 1, pp. 3-16, 10.1145/2775051.2676970, https://hal.inria.fr/hal-01096910.
- Paul-André Melliès;Noam Zeilberger, Functors are Type Refinement Systems, 2015, Mumbai India, 10.1145/2676726.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.
- 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, SIGPLAN notices, 48, 1, pp. 301-314, 10.1145/2480359.2429105.
- 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.
- Thomas Dinsdale-Young;Lars Birkedal;Philippa Gardner;Matthew Parkinson;Hongseok Yang, 2013, Views, 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.8127.
- 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 (Print), 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, 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, Sussex Research Online (University of Sussex), Crowfoot: A Verifier for Higher-Order Store Programs, pp. 136-151, 2012, 10.1007/978-3-642-27940-9_10, http://sro.sussex.ac.uk/id/eprint/31151/1/REUS_crowfoot.pdf.
- 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, 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, 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.
- F. Pottier, Proceedings - Symposium on Logic in Computer Science, Hiding Local State in Direct Style: A Higher-Order Anti-Frame Rule, 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, 2007, 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.
Share and export
Consultation statistics
This page has been seen 1942 times.
This article's PDF has been downloaded 307 times.