PSPL on Saturday, July 10th

09:00‑10:00 Session 1
Location: AT 2.14
09:00 Invited Talk: Viktor Vafeiadis
Recent developments in concurrent program logics
10:30‑12:30 Session 2
Location: AT 2.14
10:30 Luís Caires, Carla Ferreira and António Ravara
A simple proof system for lock-free concurrency

Concurrent algorithms classically relied on locks to guarantee the absence of interference when accessing shared resources. The massive use of distributed systems and of new multi-core architectures makes this approach unfeasible, and novel techniques are needed. Lock-Free algorithms have thus gained momentum. We define a core imperative calculus, equipped with concurrency and low level lock-free synchronization primitives, based on the Load-Link/Store-Conditional model. We propose a Hoare-Separation-style system to prove correct lock-free algorithms implemented in this language. Judgements distinguish local from global state, transfering knowledge between the worlds in the rules for loading and copying variables. We present a simple yet illustrative example of a proof for a concurrent data structure.

11:00 Giuseppe Primiero
A multi-modal dependent type theory for representing data accessibility in a network

In the present paper we explore the use of a newly formulated polymorphic modal type theory for a computational interpretation of programs in the context of distributed processing. The initial language define judgemental modalities with a the standard constructor for necessity interpreted as the presentation of instructions for a program terminating at runtime and an independent constructor for the possibility judgement as a representation of a process of partial evaluation. In order to interpret distributed and localised computing, we propose an extension in terms of multi-modalities, to express programs equipped with locations and data accessibility. Besides localised accessibility formalised by the different signed modalities, we develop further the language by prioritising these modalities, which implement seriality or staging annotations in the program structure.

11:30 Sungwoo Park and Jonghyun Park
Towards a Cut-free Sequent Calculus for Boolean BI

(The attached document contains the abstract of this submission.)

12:00 Holger Gast
A Developer-oriented Hoare Logic

We present a Hoare logic and verification system designed to be understandable by developers. We discuss both the underlying considerations on the design of the system, and the formal and technical background of the tools. We show that the goals have been achieved by typical examples.

14:00‑15:00 Session 3
Location: AT 2.14
14:00 Invited Talk: André Platzer
Proof Systems for Hybrid System Logics
15:30‑17:00 Session 4
Location: AT 2.14
15:30 Matteo Mio
A Proof System for Reasoning about Probabilistic Concurrent Processes

A Proof System for Reasoning about Probabilistic Concurrent Processes

16:00 Discussion Session: Peter O'Hearn and Alex Simpson
Challenge topics in PSPL