SePi is a concurrent, message-passing programming language based on
the pi-calculus. The language features synchronous, bi-directional
channel-based communication.

Programs use primitives to send and receive messages as well as offer
and select choices. Channel interactions are statically verified against
session types describing the kind and order of messages exchanged, as
well as the number of processes that may share a channel.

In order to facilitate a more precise control of program properties,
SePi includes assume and assert primitives at the process level and
refinements at the type level. Refinements are treated linearly,
allowing a finer, resource-oriented use of predicates: each assumption
made supports exactly one an assertion.