Session Type Providers (STP)
STP is a type provider in F# that generates APIs from protocol specifications.
Consider the following protocol, between a client and a server. The protocol below specifies that a client sends a message tagged as DIV (stands for division operation), containing two payloads. Then the Server replies with a message RES (stands for result) with one integer payload.
Scribble protocol:
DIV(x:int, y:int) from C to S;
RES(z:int) from S to C;
F# program
s = STP<"Protocol.scr", C>
let z = Buf<int>()
s.send(S, Div, 4, 2).receive(S, Res, z)
Support for interaction refinements
The tool supports also checks of payload constraints. For example, we can augment the protocol below to specify that the second argument of a divition cannot be zero.
DIV(x:int, y:int) from C to S; @{y!=0}
RES(z:int) from S to C;
Then the geenrated code for sending will explicitly contain the specified check.