15-818A4 Current Research on Separation Logic
John C. Reynolds
Second Half of Spring Semester 2005
University Units: 6 (minicourse)
Mondays and Wednesdays, noon-1:50 pm Wean Hall 4615A
The following recent papers on separation logic and related topics
were covered in detail:
Berdine, Calcagno, and O'Hearn,
"A Decidable Fragment of Separation Logic" (FSTTCS 2004)
In addition, Aleks Nanevski gave two lectures on his current work on
implementing separation logic in Isabelle.
O'Hearn, Yang, and Reynolds,
"Separation and Information Hiding" (POPL 2004)
Mijajlovic, Torp-Smith, and O'Hearn,
"Refinement and Separation Contexts" (FSTTCS 2004)
"Resources, Concurrency, and Local Reasoning" (CONCUR 2004)
Brookes (guest lectures by the author),
"A Semantics for Concurrent Separation Logic" (CONCUR 2004)
"Towards A Grainless Semantics for Shared-Variable Concurrency" (FSTTCS 2004)
Bornat, Calcagno, O'Hearn, and Parkinson,
"Permission Accounting in Separation Logic" (POPL 2005)
PREREQUISITES: An introductory course on separation logic.
TEXTS: Papers distributed in class.
METHOD OF EVALUATION: Each creditor was required to lecture on one of
the selected papers.
Last updated: June 6, 2005