Next: References for Main Topics
Up: Reasoning about Resources Seminar:
Previous: Challenges
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.
- August 31, Lars Birkedal
Intuitionistic Reasoning about Shared Mutable Data Structure
Literature: The paper by Reynolds with that title.
- September 07, Martin Elsman
BI as an Assertion Language for Mutable Data Structures
Literature: The paper by Ishtiaq and O'Hearn with that title.
- 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.
- September 21, Noah Torp-Smith & Thomas Hildebrandt
The Logic of Bunched Implications, II.
Literature: as above.
- September 28, Jens Chr. Godskesen
Completeness of Frame Axiom Introduction. Chapters 5 and 6 of
Yang's Ph.D. thesis (+ the introduction).
- October 05, Andzrej Wasowski
Example: The Schorr-Waite Graph Marking Algorithm.
Chapter 7 of Yang's Ph.D. thesis.
- 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.
- 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).
- November 02, Michael Florentin
Pointer Arithmetic and Local Reasoning Literature: O'Hearn,
Reynolds, Yang: Local Reasoning about Programs that Alter Data
Structures.
- 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.
- 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.''
- November 23
On Bunched Typing and Syntactic Control of Interference, I
Literature: as above.
- November 30 Open
- December 07 Open
- December 14 Open
Possible Additional topics:
- Semantics of BI, including Day's construction, and Petri nets.
- Computability and Complexity Results. Chapter 8 of Yang's Ph.D.
thesis and paper by Calcagno, Yand, and O'Hearn.
- Linear Logic and Linear Typing (term calculi for linear logic).
Relation to Bunched Typing.
- Regions and Linear Types (Walker and Watkins).
- Local reasoning for programs with procedures and pointers.
Part I and III of Yang's thesis, papers by Reynolds, O'Hearn, Tennent.
Next: References for Main Topics
Up: Reasoning about Resources Seminar:
Previous: Challenges
Lars Birkedal
2001-09-03