Resources cited in this volume

An extended related work section on the history of Separation Logic may be found in the companion course notes, available from:
The references most relevant to the contents of the course appear below.
[Birkedal, Torp-Smith and Yang 2006] Lars Birkedal, Noah Torp-smith, and Hongseok Yang. Semantics of separation-logic typing and higher-order frame rules for algol-like languages. In Logical Methods in Computer Science.
[Burstall 1972] R. M. Burstall. Some Techniques for Proving Correctness of Programs which Alter Data Structures. In Machine Intelligence 7, Edinburgh University Press.
[Charguéraud 2010] Arthur Charguéraud. Characteristic Formulae for Mechanized Program Verification. PhD thesis, Université Paris Diderot, December 2010.
[Charguéraud 2011] Arthur Charguéraud. Characteristic Formulae for the Verification of Imperative Programs. In International Conference on Functional Programming (ICFP).
[Charguéraud 2020] Arthur Charguéraud. Separation Logic for Sequential Programs. In Internation Conference on Function Programming (ICFP).
[Charguéraud et al 2023] Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter. Omnisemantics: Smoother Handling of Nondeterminism (TOPLAS).
[Chlipala et al 2009] Adam Chlipala, Gregory Malecha, Greg Morrisett, Avraham Shinnar, and Ryan Wisnesky. Effective Interactive Proofs for Higher-Order Imperative Programs. In International Conference on Functional Programming (ICFP). See also the other papers:
[Guéneau, Jourdan, Charguéraud, and Pottier 2019] Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In Interactive Theorem Proving (ITP).
[Guéneau, Myreen, Kumar and Norrish 2017] Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish. Verified Characteristic Formulae for CakeML. In European Symposium on Programming (ESOP).
[Dijstra 1975] Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM.
[Gordon 1989] Michael J. C. Gordon. Mechanizing Programming Logics in Higher Order Logic. Springer-Verlag, Berlin, Heidelberg,
[Krishnaswami, Birkedal, and Aldrich 2010] Neel R. Krishnaswami, Lars Birkedal, and Jonathan Aldrich. Verifying Event-Driven Programs Using Ramified Frame Properties. In Workshop on Types in Language Design and Implementation (TLDI).
[Hennessy and Milner 1985] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32.
[Honda, Berger, and Yoshida 2006] Kohei Honda, Martin Berger, and Nobuko Yoshida. Descriptive and relative completeness of logics for higher-order functions. International Colloquium on Automata, Languages and Programming (ICALP).
[Hobor and Villard 2013] Aquinas Hobor and Jules Villard. The Ramifications of Sharing in Data Structures. In Symposium on Principles of Programming Languages (POPL).
[Ishtiaq and O'Hearn 2001] Samin S. Ishtiaq and Peter W. O’Hearn. BI as an Assertion Language for Mutable Data Structures. SIGPLAN Notice 36.
[Jung et al 2018] Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale{\v{s}} Bizjak, Lars Birkedal, Derek Dreyer. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming.
[O'Hearn and Pym 1999] Peter W. O’Hearn and David J. Pym. The Logic of Bunched Implications. The Bulletin of Symbolic Logic 5.
[O'Hearn, Reynolds, and Yang 2001] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. Local Reasoning about Programs that Alter Data Structures. Workshop on Computer Science Logic (CSL).
[Reynolds 2002] John C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. Annual IEEE Symposium on Logic in Computer Science (LICS). 10.1109/LICS.2002.1029817
[Reynolds 2000] John C. Reynolds. Intuitionistic Reasoning about Shared Mutable Data Structure
[Schäfer et al 2016] Steven Schäfer, Sigurd Schneider, Gert Smolka. Axiomatic Semantics for Compiler Verification. In Conference on Certified Programs and Proofs (CPP).
[Tuerk 2010] Thomas Tuerk. Local Reasoning about While-Loops. In International Conference on Verified Software: Theories, Tools and Experiments (VSTTE).
[Weber 2004] Tjark Weber. Towards Mechanized Program Verification with Separation Logic. In Computer Science Logic (CSL)
[Yu, Hamid, and Shao 2003] Dachuan Yu, Nadeem A. Hamid, and Zhong Shao. Building Certified Libraries for PCC: Dynamic Storage Allocation. European Symposium on Programming (ESOP).
(* 2024-01-03 14:19 *)