Channel-Dependent Session Types
Session types provide a discipline for statically reasoning about communicating systems. However, we cannot presently use session types to reason about individual messages carried by a channel. This prevents us from capturing more precise invariants about communicating processes, in particular, invariants that constrain what a process may send based on what it has so far received. Fundamentally, the problem is that binary session types do not capture the flow of information through a system or the environment in which in which a channel is used.
In this talk, we present preliminary results on channel-dependent session types (CDSTs). CDSTs use a restricted form of concurrent type-level computation to capture a richer class of communication protocols than allowed by traditional binary session types. In particular, CDSTs can observe communications on other channels used by a process and then use these observations to restrict the communications permitted on session-typed channels. We show how to use CDSTs to specify communication protocols with various desirable causal and temporal properties.