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.
Team: Juliana Franco; Vasco T. Vasconcelos; Dimitris Mostrous