References for Main Topics

All the literature can be obtained from the author's home pages. A local copy can be found here.

• Cristiano Calcago, Samin Ishtiaq, Peter O'Hearn: ``Semantic Analysis of Pointer Aliasing, Allocation and Disposal in Hoare Logic'' Proceedings of PPDP'00.
• Cristiano Calcagno, Peter O'Hearn: ``On Garbage and Program Logic.'' Proceedings of FOSSACS'01.
• Cristiano Calcagno, Peter W. O'Hearn, Richard Bornat: ``Program Logic and Equivalence in the Presence of Garbage Collection''. Submitted, July 2001.
• Cristiano Calcagno, Hongseok Yang, Peter O'Hearn: ``Computability and Complexity Results for a Spatial Assertion Language for Data Structures.'' Submitted for publication.
• Samin Ishtiaq, Peter O'Hearn: ``BI as an Assertion Language for Mutable Data Structures.'' Proceedings of POPL'01.
• G. Morrisett and D. Walker: ``Alias Types for Recursive Data Structures.'' In 2000 ACM SIGPLAN Workshop on Types in Compilation, Montreal, Canada, September 2000.
• G. Morrisett, F. Smith, and D. Walker: ``Alias Types.'' In the European Symposium on Programming, Berlin, Germany, March 2000.
• Peter O'Hearn: ``On Bunched Typing.'' Submitted for publication, June 2000.
• P.W. O'Hearn and D. J. Pym: ``The logic of bunched implications'' Bulletin of Symbolic Logic , 5(2), June 1999, pp 215-244.
• Peter O'Hearn, David Pym, Hongseok Yang: ``Possible worlds and resources: The semantics of BI'' Submitted, October 2000
• Peter O'Hearn, John Reynolds, Hongseok Yang: ``Local Reasoning about Programs that Alter Data Structures.'' To appear, Proceedings of CSL'01.
• Peter O'Hearn and Hongseok Yang: ``Petri Net Semantics of Bunched Implications.'' Unpublished Manuscript, 14 Oct, 1999.
• D.J. Pym: ``The Semantics and Proof Theory of the Logic of Bunched Implications'', Draft Monograph, February 02, 2001.
• John C. Reynolds: ``The Essence of Algol,'' Proceedings of the International Symposium on Algorithmic Languages, 1981.
• John C. Reynolds: ``Syntactic Control of Interference,'' Conference Record of the Fifth Annual ACM Symposium on Principles of Programming, 1978
• John C. Reynolds: ``Intuitionistic Reasoning about Shared Mutable Automata, Languages and Programming, 16th International Colloquium, 1989.
• John C. Reynolds: ``Intuitionistic Reasoning about Shared Mutable Data Structure.'' Symp. in Celebration of the Work of C.A.R. Hoare. February 2000.
• John C. Reynolds: ``Lectures on Reasoning about Shared Mutable Data Structures.'' Slides from series of lectures at Aarhus University. June 2001.
• John C. Reynolds: ``Further Reasoning about Shared Mutable Data Structures'' Slides from talk at Cambridge University. 2001.
• D. Walker: ``Typed Memory Management.'' Ph.D. thesis. Cornell University. January 2001.
• D. Walker and K. Watkins: ``On Regions and Linear Types''. SPACE workshop 2000.
• H. Yang: ``Local Reasoning for Stateful Programs'', Ph.D. thesis, University of Illinois at Urbana-Champaign, 2001. Introduction and Part II.