Authors — Vasco T. Vasconcelos, Simon J. Gay b, António Ravara
DOI — 10.1016/j.tcs.2006.06.028
File — behavioral/session-types/10.1016_j.tcs.2006.06.028.pdf
Notes about Section 2 (Session Types) are written in [session-types].
Most language aspects are illustrated in Section 2, the remaining are now discussed.
An aspect regarding channels which was not discussed is that channels are runtime entities,
created when a request meets a accept.
To define their operational semantics we need to distinguish between channel ends.
Consider a channel y, each end is attributed a polarity +/-,
a polarized channel is denoted as yp where p is either + or -.
Duality on polarities is represented ~p which exchanges + and -.
Threads comprise stacks of expressions waiting for evaluation,
possibly with occurrences of the fork primitive.
They also establish new sessions (creating new channels through request/accept) by synchronizing on shared names.
Configurations have four forms:
<t> — A single thread.(C1 | C2) — A parallel collection of threads.(vx: [S])C — The declaration of a typed name.(vy)C — The declaration of a channel.The declaration of typed names shows up during the reduction of new expressions,
it can also be used at top-level to give a more realistic model of the example in
[session-types#sharing-names].
The configuration below arises during reduction of the thread <system>.
Defining it in this way represents a situation in which the clients and server are defined as separate components which already shared the name n.
systemConf = (vn: [&<add: ..., neg: ..., eval: ...>])
(<negClient n> | <negClient n> | <server n>)
T — Term typeD — Data typeS — Session typeZ — Channel environmentThe type Chan a represents the type of the channel with identity a;
the session type associated with a is recorded separately in a channel environment Z.
During reduction program variables may be replaced by channels,
implying that Chan c may become Chan y+.
Among data types we have channel-state annotated functional types Z; T -> T; Z and
types for names [S] capable of establishing sessions of type S.
The paper refers to Cyclone, which is now defunct. Its spiritual successor, Rust is highly relevant nowadays.
The Vault system adds annotations to C code which the compiler then statically checks, enforcing the protocol.
“Adoption and Focus” is a type system which tracks changes to the state of objects, handles aliasing and includes a form of function polymorphism.
Type and effect systems can be used to prove properties of protocols. Furthermore, one can add correspondence assertions to session types, increasing the expressiveness of the system. It makes possible to specify and check that interactions between participants respect the protocol, and furthermore, the integrity and correctness of data propagation are verifiable.
The authors outline four main lines of future work:
For the full language syntax, refer to the original paper.
Interesting References