We present Most, a language for protocols using message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communication protocols that vary based on messages observed on other channels. Hence, Most allows us to express global invariants about processes, rather than just local invariants, in a bottom-up, compositional way. We give Most a semantic foundation using traces with binding, a semantic approach for compositionally reasoning about traces in the presence of name generation. We use this semantics to prove type soundness and compositionality for Most processes. We see this as a significant step towards capturing message-dependencies and providing more precise guarantees about processes.
Wed 23 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:40 | Formal Methods 2OOPSLA 2024 at San Gabriel Chair(s): Bor-Yuh Evan Chang University of Colorado Boulder & Amazon | ||
16:00 20mTalk | A Constraint Solving Approach to Parikh Images of Regular Languages OOPSLA 2024 DOI | ||
16:20 20mTalk | Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing OOPSLA 2024 Wenjia Ye National University of Singapore, Yaozhu Sun University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong DOI | ||
16:40 20mTalk | Inductive diagrams for causal reasoning OOPSLA 2024 Jonathan Castello University of California, Santa Cruz, Patrick Redmond University of California at Santa Cruz, Lindsey Kuper University of California, Santa Cruz DOI Pre-print | ||
17:00 20mTalk | Message-Observing Sessions OOPSLA 2024 DOI | ||
17:20 20mTalk | Plume: Efficient and Complete Black-box Checking of Weak Isolation Levels OOPSLA 2024 Si Liu ETH Zurich, Long Gu State Key Laboratory for Novel Software Technology, Nanjing University, Hengfeng Wei State Key Laboratory for Novel Software Technology, Nanjing University, David Basin ETH Zurich DOI |