15-818A4 Current Research on Separation Logic
(6 units)
Spring 2007
John C. Reynolds
Second Half of Spring Semester 2007
University Units: 6 (minicourse)
Mondays and Wednesdays, 1:30-2:50 pm Wean Hall 4615A,
starting Monday, March 19
Course Description
We will study and discuss recent papers on separation logic
and related topics. I will begin with:
O'Hearn, Yang, and Reynolds,
"Separation and Information Hiding" (POPL 2004)
and continue with:
O'Hearn,
"Resources, Concurrency, and Local Reasoning" (CONCUR 2004)
Bornat, Calcagno, O'Hearn, and Parkinson,
"Permission Accounting in Separation Logic" (POPL 2005)
Bornat, Calcagno, and Yang,
"Variables as Resource in Separation Logic" (MFPS 2005)
There will also be guest lectures by Steve Brookes and Stephen Magill:
Brookes,
"A Semantics for Concurrent Separation Logic" (CONCUR 2004)
Magill, Nanevski, Clarke, and Lee,
"Inferring Invariants in Separation Logic for Imperative List-processing Programs" (SPACE 2006)
In addition, each creditor will be required to lecture on a paper chosen by
them and the instructor.
The only texts will be papers distributed in class.
Last updated: March 18, 2007