15-818A4 Current Research on Separation Logic
(6 units)
Spring 2007
John C. Reynolds
Second Half of Spring Semester 2007
University Units: 6 (minicourse)
Time: MW 1:30-2:50 WeH 4615A
Course Description
We will study and discuss recent papers on separation logic,
grainless semantics, and related topics. The following is a
list of likely papers:
Berdine, Calcagno, and O'Hearn,
"A Decidable Fragment of Separation Logic" (FSTTCS 2004)
O'Hearn, Yang, and Reynolds,
"Separation and Information Hiding" (POPL 2004)
Mijajlovic, Torp-Smith, and O'Hearn,
"Refinement and Separation Contexts" (FSTTCS 2004)
O'Hearn,
"Resources, Concurrency, and Local Reasoning" (CONCUR 2004)
Brookes,
"A Semantics for Concurrent Separation Logic" (CONCUR 2004)
Brookes,
A Grainless Semantics for Parallel Programs with Shared Mutable Data
(MFPS2005)
Reynolds,
"Towards A Grainless Semantics for Shared-Variable Concurrency" (FSTTCS 2004)
Bornat, Calcagno, O'Hearn, and Parkinson,
"Permission Accounting in Separation Logic" (POPL 2005)
Bornat,
"Variables as Resource in Separation Logic" (MFPS2005)
Birkedal, Torp-Smith, and Reynolds,
"Local Reasoning about a Copying Garbage Collector" (TOPLAS, accepted)
Birkedal, Torp-Smith, and Yang,
"Semantics of Separation Logic Typing and Higher-order Frame Rules"
(LICS2005)
PREREQUISITES: An introductory course on separation logic.
TEXTS: Papers distributed in class.
METHOD OF EVALUATION: Each creditor will be required to lecture on one of
the selected papers.