A theorem prover plugin for Essential Multiparty Session Types

A theorem prover plugin for Essential Multiparty Session Types

The STG group at TU Darmstadt has formalised the calculus of structured interactions (CoSI) and the type theory of Essential Multiparty Session Types (EMST) to describe and statically validate safe and deadlock free interactions. Multiparty session types is a well-established type theory that is highly attracting the attention of the programming language and software engineering communities.

The CoSI and EMST aim to establish the foundations of session types and their transition to practice. The fundamental properties of typed CoSI processes such as subject reduction, communication safety, and progress are established and proved.

In this project, the bachelor or master student will participate in the design and prototyping of a plugin for a well-established theorem prover (preferably Isabelle or Coq) to assist the formal proofs of soundness for EMST. The plugin will consist in modelling the formal definition of CoSI and its type system in the preferable theorem prover. A test of the plugin will be developed, using the current proofs of soundness of Essential Multiparty Session Types.

The ideal student has taken a course or has prior industry or research experience in interactive theorem provers (proof assistants) and formal proofs.