We develop a session types framework for implementing and validating rate-based message passing systems in Internet of Things (IoT) domains. To model the indefinite repetition present in many embedded and IoT systems, we introduce a timed process calculus with a periodic recursion primitive. This allows us to model rate-based computations and communications inherent to these application domains. We introduce a definition of rate-based session types in a binary session types setting and a new compatibility relationship, which we call rate compatibility . Programs which type-check enjoy the standard session types guarantees as well as rate error freedom—meaning processes which exchanges messages do so at the same rate . Rate compatibility is defined through a new notion of type expansion, a relation that allows communication between processes of differing periods by synthesizing and checking a common superperiod type. We prove type preservation and rate error freedom for our system and show a decidable method for type checking based on computing superperiods for a collection of processes. We implement a prototype of our type system including rate compatibility via an embedding into the native type system of Rust. We apply this framework to a range of examples from our target domain such as Android software sensors, wearable devices, and sound processing. Our framework is used to implement a heart rate sensor application that runs on a commercially available smartwatch.

@article{IraciCHZ25,
  title = {Rate-Based Session Types for IoT Systems},
  author = {Grant Iraci and Cheng-En Chuang and Raymond Hu and Lukasz Ziarek},
  journal = {ACM Transactions on Programming Languages and Systems},
  volume = {47},
  number = {3},
  year = {2025},
  doi = {10.1145/3754449}
}