Resources cited in this volume

An extended related work section on the history of Separation Logic may be found in the paper [Charguéraud 2020], available from:
A subset of the references most relevant to the contents of the course appears 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 2020] Arthur Charguéraud. Separation Logic for Sequential Programs. In Internation Conference on Function Programming (ICFP).
[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.
[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 July 2001
[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).
(* 2021-01-25 13:22 *)