Models and Logics
for Reasoning about
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:
K. Svendsen, and L. Birkedal.
Impredicative Concurrent Abstract Predicates.ESOP 2014. [homepage]
L. Birkedal, R. E. Møgelberg, J. Schwinghammer, and
First Steps in Synthetic Guarded Domain Theory: Step-indexing 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:
|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
|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:
- 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 spin-lock 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 simply-typed
lambda calculus in Section 4.3 of Barendregt's