~/talk

Fair Termination of Binary Sessions

on YouTube 21m
Talkat POPL 2022 · 2022-01-16..01-22· [concurrency]

speakers

name:Luca Ciccone
links:none on file
name:Luca Padovani
links:none on file

resources

video:https://youtu.be/dl0zJjtYqqM
slides:none on file

summary

Claims the first type system ensuring fair termination of binary sessions and a liveness-preserving fair subtyping relation that rejects unsafe substitutions the standard subtype allows. Uses a combined inductive/coinductive characterization of subtyping and a concrete measure pairing a rank bound on casts with an effort metric; proves subject reduction and soundness (well typed implies fair termination). Implements a checker, formalizes proofs in the supplementary artifacts, and the implementation is available and evaluated.

AI-written summary · about

chapters (6)

  1. 0:00Fair termination of binary sessions
  2. 2:39Fair termination assumptions
  3. 7:16Fair subtyping for liveness
  4. 13:08Soundness proof
  5. 16:41Higher-order session types
  6. 19:27Question and answer session

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.