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: http://www.chargueraud.org/research/2020/seq_seplogic/seq_seplogic.pdf 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). https://doi.org/10.1145/2034773.2034828 [Charguéraud 2020] Arthur Charguéraud. Separation Logic for Sequential Programs. In Internation Conference on Function Programming (ICFP). https://dl.acm.org/doi/abs/10.1145/3408998 [Charguéraud et al 2022] Arthur Charguéraud, Adam Chlipala, Andres Erbsen, and Samuel Gruetter. Omnisemantics: Smoother Handling of Nondeterminism (Draft). http://www.chargueraud.org/research/2022/omnisemantics/omnisemantics.pdf. [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). https://doi.org/10.1145/1596550. See also the other papers: https://ynot.cs.harvard.edu/ [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). https://doi.org/10.4230/LIPIcs.ITP.2019.18 [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). https://doi.org/10.1007/978-3-662-54434-1_22 [Dijstra 1975] Edsger W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM. https://doi.org/10.1145/360933.360975 [Gordon 1989] Michael J. C. Gordon. Mechanizing Programming Logics in Higher Order Logic. Springer-Verlag, Berlin, Heidelberg, https://doi.org/10.1007/978-1-4612-3658-0_10 [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). https://doi.org/10.1145/1708016.1708025 [Hennessy and Milner 1985] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32. https://dl.acm.org/doi/10.1145/2455.2460 [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). https://doi.org/10.1007/11787006_31 [Hobor and Villard 2013] Aquinas Hobor and Jules Villard. The Ramifications of Sharing in Data Structures. In Symposium on Principles of Programming Languages (POPL). https://doi.org/10.1145/2429069.2429131 [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. https://doi.org/10.1145/373243.375719 [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. https://doi.org/10.1017/S0956796818000151 [O'Hearn and Pym 1999] Peter W. O’Hearn and David J. Pym. The Logic of Bunched Implications. The Bulletin of Symbolic Logic 5. https://doi.org/10.2307/421090 [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). https://doi.org/10.1007/3-540-44802-0_1 [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 http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.11.5999&rep=rep1&type=pdf [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). https://dl.acm.org/doi/10.1145/2854065.2854083 [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) https://doi.org/10.1007/978-3-540-30124-0_21 [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). https://doi.org/10.1007/3-540-36575-3_25