~/talk

Validating IoT Devices with Rate-Based Session Types

on YouTube 18m
Talkat OOPSLA 2023 · 2023-10-23..10-27· [embedded-and-hardware]

speakers

name:Grant Iraci
links:none on file
name:Cheng-En Chuang
links:none on file
name:Raymond Hu
links:none on file
name:Lukasz Ziarek
links:none on file

resources

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

summary

Framework formalizes rate-based session types by adding a periodic recursion Omega that records per-channel periods, proves preservation and rate error freedom, and defines compatibility via expansion to a common superperiod (LCM of periods). Implements a Rust embedding that type-checks by computing superperiods, supports binary channels only, disallows nested periods, and evaluates on an open-source smartwatch heart-rate pipeline with a working artifact running on a wrist.

AI-written summary · about

chapters (7)

  1. 0:00Introduction
  2. 1:47Session types need rate info
  3. 4:16Periodic tasks with session types
  4. 8:10Rate-based session type Omega
  5. 10:58Expansion relation for validation
  6. 13:24Rust implementation demo
  7. 14:49Q&A

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.