## 15-818A4 Current Research on Separation Logic
(6 units)
Spring 2005

### John C. Reynolds

Second Half of Spring Semester 2005
University Units: 6 (minicourse)

Mondays and Wednesdays, noon-1:50 pm Wean Hall 4615A

### Course Description

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)

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 (guest lectures by the author),
"A Semantics for Concurrent Separation Logic" (CONCUR 2004)

Reynolds,
"Towards A Grainless Semantics for Shared-Variable Concurrency" (FSTTCS 2004)

Bornat, Calcagno, O'Hearn, and Parkinson,
"Permission Accounting in Separation Logic" (POPL 2005)

In addition, Aleks Nanevski gave two lectures on his current work on
implementing separation logic in Isabelle.
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