Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 18:30 - 18:45 at CPP - Semantics Chair(s): Yannick Zakowski

Session types—a family of type systems for message-passing concurrency—have been subject to many extensions, where each extension comes with a separate proof of type safety. These extensions cannot be readily combined, and their proofs of type safety are generally not machine checked, making their correctness less trustworthy. We overcome these shortcomings with a semantic approach to binary asynchronous affine session types, by developing a logical relations model in Coq using the Iris program logic. We demonstrate the power of our approach by combining various forms of polymorphism and recursion, asynchronous subtyping, references, and locks/mutexes. As an additional benefit of the semantic approach, we demonstrate how to manually prove typing judgements of racy, but safe, programs that cannot be type checked using only the rules of the type system.

Mon 18 Jan

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

18:00 - 18:45
SemanticsCPP at CPP
Chair(s): Yannick Zakowski Inria

Streamed session: https://youtu.be/Qak5mK92etU

18:00
15m
Talk
A Coq Formalization of Data Provenance
CPP
Véronique Benzaken Université Paris Saclay, Sarah Cohen-Boulakia LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay, Evelyne Contejean CNRS, Chantal Keller LRI, Univ. Paris-Sud, Rébecca Zucchini LRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay
Pre-print Media Attached
18:15
15m
Talk
Developing and certifying Datalog optimizations in Coq/MathComp
CPP
Pierre-Léo Bégay Orange Labs & Verimag, Pierre Crégut Orange Labs, Jean-François Monin Verimag
Pre-print Media Attached
18:30
15m
Talk
Machine-Checked Semantic Session TypingDistinguished Paper Award
CPP
Jonas Kastberg Hinrichsen IT University of Copenhagen, Daniël Louwrink University of Amsterdam, Robbert Krebbers Radboud University Nijmegen, Jesper Bengtson IT University of Copenhagen
Pre-print Media Attached