Effpi: Verified Message-Passing Programs in Dotty
summary
Effpi provides a Scala 3 DSL plus a Dotty compiler plugin that encodes behavioral (session-like) types as dependent types, checks program-to-protocol conformance at compile time and exports the type model to the mCRL2 model checker for properties like deadlock‑freedom. Examples: dining philosophers is detected as deadlocking until one philosopher’s fork order is flipped; verification usually runs interactively but some queries take minutes (one forwarding check ~20 minutes). Runtime performance is comparable to Akka; code and papers are on GitHub.
AI-written summary · about
chapters (7)
- 0:00Effpi introduction
- 5:37Process calculi background
- 15:40Effpi DSL
- 25:18Dependent types for protocols
- 32:38Model checking deadlock freedom
- 41:56Actors and process calculi
- 46:16Performance benchmarks
