Models and Logics
for Reasoning about
HigherOrder Imperative
Concurrency
Seminar
What? The aim of this seminar is to learn about recent research on models and logics for formal modular reasoning about higherorder imperative concurrent programs.
How? We will read relatively few papers, but will take the time to dive into sufficient detail in those we do read to actually understand the techniques involved.
We will concentrate on the following papers:

K. Svendsen, and L. Birkedal.
Impredicative Concurrent Abstract Predicates. ESOP 2014. [homepage] 
L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and
K. Støvring.
First Steps in Synthetic Guarded Domain Theory: Stepindexing in the Topos of Trees. LMCS. [PDF]
When?/Where? Mondays, 12–2 PM; room Nygaard 295.
The schedule for the first few weeks is as follows:
Date  Topic  Person responsible  Notes/Reading  

Monday, 15.04  Introduction, modelling guarded recursion.  LB  Intro to Topos of Trees, up to Theorem 2.4 (p.7) of the paper  
Thursday, 18.04  Talk by Aaron Turon, 13:00–14:00  Aaron Turon, LB  Aaron Turon and Derek Dreyer visit Wd–Fr that week  
Monday, 22.04  Modelling MLstyle references with guarded recursion.  FS (Lars away)  Intro to interpreting languages in the internal logic; Sections 3.1–3.3 and start of 3.4 in the paper. See note for extra pointers on relational reasoning  
Monday, 29.04  Modelling MLstyle references, pt. 2.  FS  Logical relations argument: interpretation of types, interpretation of open terms, fundamental theorem. Section 3.4 and Appendices A.3–A.6 in the paper.  
Monday, 06.05  Cancelled!  Lars in Copenhagen  
Monday, 13.05  Internal language  LB  Definitions of logical connectives, "later" operator, contractiveness and Banach's FixedPoint Theorem, recursive domain equations. The rest of Section 2 (pp. 7 – 11).  
Monday, 20.05  No seminar  Holiday!  
Monday, 27.05  Intro to iCAP  LB  Spinlock in iCAP. Higherorder specification of a lock, protocol and definitions of abstract predicates, proof of spinlock constructor. Most of Section 2 of the iCAP paper (pp. 3–4).  
Monday, 03.06  Intro to iCAP pt. 2  LB  Proofs of acquire and release
methods. The remainder of Section 2 of the iCAP paper. 

Monday, 10.06  Model of iCAP  LB  Overview of the model of iCAP in the topos of trees (Section 3 in the iCAP paper). This ends the seminar. 
Potential topics for iCAPrelated projects:
 Stability: variant of iCAP with stability baked into the definition of propositions (assertions).
 Permissions model: consider iCAP with simpler or more expressive model of permissions.
 Clients: prove client programs of spinlock example to better understand the logic.
The list is tentative, more stuff may be added in the course of the seminar.
Extra reading: intro to relational reasoning.
If after today's seminar you feel like you could use some
gentler introduction to the kind of reasoning we were doing, a
good start is the proof of strong normalisation for simplytyped
lambda calculus in Section 4.3 of Barendregt's