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.

Conference Day
Mon 18 Jan

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

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

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

18:00
15m
Talk
A Coq Formalization of Data Provenance
CPP
Véronique BenzakenUniversité Paris Saclay, Sarah Cohen-BoulakiaLRI, Université de Paris Sud, CNRS (UMR8623) - Université Paris Saclay, Evelyne ContejeanCNRS, Chantal KellerLRI, Univ. Paris-Sud, Rébecca ZucchiniLRI, 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égayOrange Labs & Verimag, Pierre CrégutOrange Labs, Jean-François MoninVerimag
Pre-print Media Attached
18:30
15m
Talk
Machine-Checked Semantic Session TypingDistinguished Paper Award
CPP
Jonas Kastberg HinrichsenIT University of Copenhagen, Daniël LouwrinkUniversity of Amsterdam, Robbert KrebbersRadboud University Nijmegen, Jesper BengtsonIT University of Copenhagen
Pre-print Media Attached