Mondays and Wednesdays, 1 to 2:30pm, in Wean Hall 4615A (beginning January 22)
There will be no textbook. The course will cover at least the following research papers:
Reynolds, J. C., Intuitionistic Reasoning about Shared Mutable Data Structure (in gzip-encoded postscript) or (in gzip-encoded dvi format)
Ishtiaq, S. and O'Hearn, P. W., BI as an Assertion Language for Mutable Data Structure (in pdf)
Reynolds, J. C., Lectures on Reasoning about Shared Mutable Data Structures (Tandil Lectures) (in gzip-encoded postscript) or (in gzip-encoded dvi format)
Reynolds, J. C. and O'Hearn, P. W., Reasoning about Shared Mutable Data Structure (in gzip-encoded postscript) or (in gzip-encoded dvi format)
Yang, Hongseok, An Example of Local Reasoning in BI Pointer Logic: The Schorr-Waite Graph Marking Algorithm (in postscript)
Walker, D. and Morrisett, G., Alias Types for Recursive Data Structures (in postscript)
O'Hearn, P. W., Reynolds, J. C., and Yang, Hongseok, Local Reasoning about Shared Mutable Data Structure (in postscript)
Also there are the following class notes:
Reynolds, J. C., 15-819A3 Class notes 1 (in postscript)
Reynolds, J. C., 15-819A3 Class notes 2 (in postscript)
Reynolds, J. C., 15-819A3 Class notes 3 (in postscript)
Reynolds, J. C., 15-819A3 Class notes 4 (in postscript)
Walker, David, 15-819A3 Class notes (in postscript)