Models and Logics
for Reasoning about
Higher-Order Imperative Concurrency

What? The aim of this seminar is to learn about recent research on models and logics for formal modular reasoning about higher-order 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:

The second of these papers (the topos of trees one) will provide us with metalogic in which we will model the semantics and logic for reasoning about concurrency (the iCAP paper).

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 ML-style 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 ML-style 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 Fixed-Point 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 Spin-lock in iCAP. Higher-order 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 iCAP-related projects:

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 simply-typed lambda calculus in Section 4.3 of Barendregt's Lambda Calculi and Types (PDF available here). Also, Bob Harper and Amal Ahmed gave a very nice series of talks on the subject during 2011 OPLSS; the videos are available here, start with the Type Theory Foundations one, since Logical Relations assumes it.