Machine-Checked Semantic Session Typing (CPP 2021 - Certified Programs and Proofs) - POPL 2021
Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021
Online
Attending
Venue: Online (How to POPL in 2021)
Supporting POPL
Student Volunteers
Code of Conduct
Registration
FAQ
Program
POPL Program
Your Program
Sun 17 Jan
Mon 18 Jan
Tue 19 Jan
Wed 20 Jan
Thu 21 Jan
Fri 22 Jan
Tracks
POPL 2021
POPL
Artifact Evaluation
Workshops and Co-located Events
TutorialFest
Student Research Competition
Student Volunteers
POPL Meetups
Co-hosted Conferences
CPP
CPP
CPP
Lightning Talks
PLMW
VMCAI
Workshops
CoqPL
LAFI
PEPM
PriSC
Co-hosted Symposia
PADL
Organization
POPL 2021 Committees
Organizing Committee
Track Committees
POPL
Artifact Evaluation
TutorialFest
Student Research Competition
Student Volunteers
Contributors
People Index
Co-hosted Conferences
CPP
Organization Committee
Program Committee
Steering Committee
PLMW
Invited Speakers
Panelists
Organizing Committee
VMCAI
Invited Speakers
Organizing Committee
Program Committee
Artifact Evaluation Committee
Workshops
CoqPL
Invited speaker
Organizing Committee
Program Committee
LAFI
Organizing Committee
Program Committee
Steering Committee
PEPM
Organizing Committee
Program Committee
Steering Committee
PriSC
Program Committee
Steering Committee
Co-hosted Symposia
PADL
Programme Chairs
Programme Committee
Series
Series
POPL 2027
POPL 2026
POPL 2025
POPL 2024
POPL 2023
POPL 2022
POPL 2021
POPL 2020
POPL 2019
POPL 2018
POPL 2017
POPL 2016
POPL 2021
series
) /
CPP 2021 (
series
) /
Certified Programs and Proofs
Machine-Checked Semantic Session Typing
Distinguished Paper Award
Who
Jonas Kastberg Hinrichsen
Daniël Louwrink
Robbert Krebbers
Jesper Bengtson
Track
CPP 2021
Program Display Configuration
Close
When
Mon 18 Jan 2021 18:30 - 18:45 at
CPP
Semantics
Chair(s):
Yannick Zakowski
Abstract
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.
Link to Preprint
Jonas Kastberg
Hinrichsen
IT University of Copenhagen
Denmark
Daniël Louwrink
University of Amsterdam
Robbert Krebbers
Radboud University Nijmegen
Jesper Bengtson
IT University of Copenhagen
Long presentation
Short presentation
Program Display Configuration
Close
Session Program
Mon 18 Jan
Displayed time zone:
Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna
change
18:00 - 18:45
Semantics
CPP
at
CPP
Chair(s):
Yannick Zakowski
Inria
Streamed session:
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 Typing
Distinguished 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
Sat 25 Apr 03:45