Machine-Checked Semantic Session TypingDistinguished Paper Award
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 Times are displayed in 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 - 18:15 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 - 18:30 Talk | Developing and certifying Datalog optimizations in Coq/MathComp CPP Pre-print Media Attached | ||
18:30 - 18:45 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 |