The session type !Int.?String.end describes a channel endpoint. What does a process holding this endpoint do?
AIt receives an Int, then sends a String, then closes
BIt sends an Int, then receives a String, then closes
CIt sends both an Int and a String simultaneously
DIt either sends an Int or receives a String
The ! prefix means 'send' and ? means 'receive.' The dot sequences the operations. So !Int.?String.end means: first send an integer on the channel, then receive a string from the channel, then the session is complete. The dual endpoint (held by the other process) has the complementary type ?Int.!String.end — it receives the Int and sends the String. Session types enforce that both endpoints agree on the protocol.
Question 2 Short Answer
If one endpoint has session type S, the other endpoint must have the dual type S-bar (complement). For !Int.?Bool.end, what is the dual?
Think about your answer, then reveal below.
Model answer: ?Int.!Bool.end — every send becomes a receive and vice versa. The dual ensures that when one process sends, the other receives, and the message types match at each step.
Duality is the fundamental mechanism ensuring communication safety. If process A has type !Int.?Bool.end and process B has the dual ?Int.!Bool.end, then: A sends an Int while B receives an Int (types match), then A receives a Bool while B sends a Bool (types match), then both close. Any mismatch in the protocol would result in a type error. This duality requirement is checked statically, guaranteeing protocol compliance without runtime verification.
Question 3 True / False
Session types can guarantee deadlock freedom in concurrent programs.
TTrue
FFalse
Answer: True
Advanced session type systems guarantee deadlock freedom by imposing structural constraints on how sessions are composed. Linear session types ensure each channel is used exactly once (preventing interference), and session type systems with progress guarantees ensure that well-typed programs always advance — no set of processes can be mutually waiting for each other. This is achieved by requiring certain orderings on channel usage or by restricting the topology of communication. The guarantee is not universal (some systems only ensure type safety, not deadlock freedom), but it is a major research achievement in session type theory.
Question 4 Short Answer
Why do session type systems typically require linearity — that each channel endpoint is used exactly once?
Think about your answer, then reveal below.
Model answer: Linearity ensures that a channel endpoint is not shared between multiple processes or used at different protocol stages simultaneously. If two processes could both hold the same endpoint, one might send when the protocol expects only one send, corrupting the session. Linearity also prevents a process from using an endpoint after closing it or abandoning it mid-session. These constraints are essential for the type system to track the channel's protocol state accurately.
This connects session types to linear types more broadly. A linear channel endpoint is a resource that must be used exactly once: you send/receive on it according to the session type, and you eventually close it. You cannot duplicate it (that would create two senders where the protocol expects one), and you cannot discard it (that would abandon the session). This resource discipline is what makes static protocol verification possible.