August 8, 2025
SIGFPT Process Calculi: CCS, Pi Calculus, and Protocol Formalization
Participants: _vgr, ediblebadger, simpalaxy, timber1997, giovanni.merlino, plague_year, sachbenny, stevebeans., nattfrosten
The SIGFPT group studied process calculi as formal tools for protocol theory, focusing on the Calculus of Communicating Systems (CCS) by Mantis Cheng as the primary reading. The discussion connected CCS to lambda calculus as the concurrent analogue, explored how linear logic's resource-sensitive semantics map onto typed pi calculus communication primitives, and examined more expressive formalisms like interaction nets and bigraphs that enable channel sharing and protocol evolution. Members worked through handwashing and handshakes as minimal model systems to test their formalization approaches, discovering a tension between modeling low-level automata versus capturing the higher-level protocol structure involving resource exhaustion and causality ordering.
Key tensions emerged around expressivity versus tractability: while CCS is limited, adding features like channel sharing enables richer protocols but requires substantial syntactic sugar (analogous to how Haskell is built on lambda calculus). The group questioned whether handwashing definitions should be necessary-and-sufficient or merely sufficient (like a family of equivalent paths in homotopy theory), and recognized that their current CCS models were capturing mimicked actions rather than the essential protocol semantics of state transitions and resource constraints. The conversation highlighted the need for multiple future sessions to fully grasp the material and develop more sophisticated formalizations incorporating temporal/causal ordering.
- Pi calculus relates to concurrent systems as lambda calculus relates to sequential computation; linearly typed pi calculus enforces one-to-one channel communication as a resource restriction.
- Linear logic's negative/positive formula distinction maps directly onto pi calculus send/receive primitives, enabling both server and client perspectives with different notions of choice and control.
- CCS provides a limited but tractable foundation; more expressive formalisms (pi calculus with channel sharing, interaction nets, bigraphs) enable protocol evolution but require syntactic sugar for practical use.
- Handwashing protocols are best modeled as families of behavioral paths rather than necessary-and-sufficient definitions, similar to homotopy equivalence classes of solutions to reaching the same goal state.
- The distinction between modeling automata that mimic actions versus capturing the essential resource-sensitive and causality-ordered aspects of protocolization remains a key open question.