Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Fri 22 Jan 2021 15:55 - 16:05 at POPL-B - Concurrency (Message Passing)

Step-indexed logical relations are an extremely useful technique for building operational-semantics-based models and program logics for realistic, richly-typed programming languages. They have proven to be indispensable for modeling features like higher-order state, which many languages support but which were difficult to accommodate using traditional denotational models. However, the conventional wisdom is that, because they only support reasoning about finite traces of computation, (unary) step-indexed models are only good for proving safety properties like “well-typed programs don’t go wrong”. There has consequently been very little work on using step-indexing to establish liveness properties, in particular termination.

In this paper, we show that step-indexing can in fact be used to prove termination of well-typed programs—even in the presence of dynamically-allocated, shared, mutable, higher-order state—so long as one’s type system enforces disciplined use of such state. Specifically, we consider a language with asynchronous channels, inspired by promises in JavaScript, in which higher-order state is used to implement communication, and linearity is used to ensure termination. The key to our approach is to generalize from natural number step-indexing to transfinite step-indexing, which enables us to compute termination bounds for program expressions in a compositional way. Although transfinite step-indexing has been proposed previously, we are the first to apply this technique to reasoning about termination in the presence of higher-order state.

Fri 22 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:45 - 16:45
Concurrency (Message Passing)POPL at POPL-B
15:45
10m
Talk
On Algebraic Abstractions for Concurrent Separation Logics
POPL
František Farka IMDEA Software Institute, Spain, Aleksandar Nanevski IMDEA Software Institute, Anindya Banerjee IMDEA Software Institute, Germán Andrés Delbianco Nomadic Labs, Ignacio Fábregas Universidad Complutense de Madrid
Link to publication DOI
15:55
10m
Talk
Transfinite Step-Indexing for Termination
POPL
Simon Spies MPI-SWS and University of Cambridge, Neel Krishnaswami Computer Laboratory, University of Cambridge, Derek Dreyer MPI-SWS
Link to publication DOI
16:05
10m
Talk
Precise Subtyping for Asynchronous Multiparty Sessions
POPL
Silvia Ghilezan University of Novi Sad, Mathematical Institute SASA, Jovanka Pantović University of Novi Sad, Ivan Prokić University of Novi Sad, Alceste Scalas Technical University of Denmark, Nobuko Yoshida Imperial College London
Link to publication DOI Media Attached
16:15
10m
Talk
A Separation Logic for Effect Handlers
POPL
Link to publication DOI
16:25
10m
Talk
Distributed Causal Memory: Modular Specification and Verification in Higher-Order Distributed Separation Logic
POPL
Léon Gondelman Aarhus University, Simon Oddershede Gregersen Aarhus University, Abel Nieto Aarhus University, Amin Timany Aarhus University, Lars Birkedal Aarhus University
Link to publication DOI
16:35
10m
Talk
PerSeVerE: Persistency Semantics for Verification under Ext4
POPL
Michalis Kokologiannakis MPI-SWS, Germany, Ilya Kaysin National Research University Higher School of Economics, JetBrains Research, Azalea Raad Imperial College London, Viktor Vafeiadis MPI-SWS
Link to publication DOI