An interaction-based language and its typing system

We present a small language $$\mathcal{L}$$ and its typing system, starting from the idea of interaction, one of the important notions in parallel and distributed computing. $$\mathcal{L}$$ is based on, apart from such constructs as parallel composition and process creation, three pairs of communication primitives which use the notion of a session, a semantically atomic chain of communication actions which can interleave with other such chains freely, for high-level abstraction of interactionbased computing. The three primitives enable programmers to elegantly describe complex interactions among processes with a rigorous type discipline similar to ML [4]. The language is given formal operational semantics and a type inference system, regarding which we prove that if a program is well-typed in the typing system, it never causes run-time error due to type inconsistent communication patterns, offering a new foundation for type discipline in parallel programming languages.