Lecture Plan

All the literature can be obtained from the author's home pages, see the list of references below. Besides the mentioned literature, also look at the slides of talks given by Reynolds, O'Hearn, et. al.

1. August 31, Lars Birkedal Intuitionistic Reasoning about Shared Mutable Data Structure Literature: The paper by Reynolds with that title.
2. September 07, Martin Elsman BI as an Assertion Language for Mutable Data Structures Literature: The paper by Ishtiaq and O'Hearn with that title.
3. September 14, Noah Torp-Smith & Thomas Hildebrandt The Logic of Bunched Implications, I. Literature: The paper O'Hearn and Pym with that title and O'Hearn, Pym, Yang: Possible Worlds and Resources: The Semantics of BI. For additional material, see Pym's monograph: The Semantics and Proof Theory of the Logic of Bunched Implications. Regarding semantics: focus on the sharing interpretation and on the basic correspondence with doubly closed categories.
4. September 21, Noah Torp-Smith & Thomas Hildebrandt The Logic of Bunched Implications, II. Literature: as above.
5. September 28, Jens Chr. Godskesen Completeness of Frame Axiom Introduction. Chapters 5 and 6 of Yang's Ph.D. thesis (+ the introduction).
6. October 05, Andzrej Wasowski Example: The Schorr-Waite Graph Marking Algorithm. Chapter 7 of Yang's Ph.D. thesis.
7. October 12, Peter Sestoft Semantic Analysis of Pointer Aliasing and Disposal in Hoare Logic Literature: The paper by Calcagno, Ishtiaq and O'Hearn with that title.
8. October 26 Program Logic and Equivalence in the presence of Garbage Collection Literature: The paper by Calcagno, O'Hearn, and Bornat with that title and the paper by Calcagno and O'Hearn ``On Garbage and Program Logic'' (a conference version of the former paper).
9. November 02, Michael Florentin Pointer Arithmetic and Local Reasoning Literature: O'Hearn, Reynolds, Yang: Local Reasoning about Programs that Alter Data Structures.
10. November 09, Andrzej Filinski Alias Types for Recursive Data Structures Literature: The paper by Morrisett and Walker with that title and Class Notes of Walker for Reynolds' course at CMU.
11. November 16 On Bunched Typing and Syntactic Control of Interference, I Literature: The paper by O'Hearn ``On Bunched Typing'' and papers by Reynols on ``Syntactic Control of Interference'' (part I and II) and by Reynolds on ``The Essence of Algol.''
12. November 23 On Bunched Typing and Syntactic Control of Interference, I Literature: as above.
13. November 30 Open
14. December 07 Open
15. December 14 Open

Possible Additional topics:

1. Semantics of BI, including Day's construction, and Petri nets.
2. Computability and Complexity Results. Chapter 8 of Yang's Ph.D. thesis and paper by Calcagno, Yand, and O'Hearn.
3. Linear Logic and Linear Typing (term calculi for linear logic). Relation to Bunched Typing.
4. Regions and Linear Types (Walker and Watkins).
5. Local reasoning for programs with procedures and pointers. Part I and III of Yang's thesis, papers by Reynolds, O'Hearn, Tennent.