Synthesis of certified distributed mobile programs using proof assistants and monadic types

One of the most interesting features of type-theory based proof assistants is the possibility of synthesizing certified programs from proofs of their specifications. A property proved in the proof assistant (e.g., a precise specification) will be satisfied by the extracted program. However, the actual extraction mechanisms are restricted to functional programs, e.g. in Haskell or Objective CaML, but there are other paradigms, such as distributed concurrent programs, in which programming is difficult and error-prone. These scenarios would benefit from similar mechanisms for extraction and automatic synthesis of certified programs. In this seminar we will present a methodology for using existing proof assistants, namely Coq, for the synthesis of certified programs in Erlang. The basic idea is that the proof assistant’s type theory can be extended with suitable "monadic types", covering the specific non-functional computational aspect. These monadic types can be used to provide the specification of distributed (non-functional) programs; these propositions can be proved constructively as usual, and from these proofs we can extract functional programs (e.g., in Haskell) by taking advantage of the standard Coq extraction facility. Finally, these functional programs can be translated into real distributed programs in Erlang by means of a “back-end” compiler from Haskell to Erlang. Overall, we obtain a system in which we can give a formal specification of a distributed program, prove its soundness, and from this proof we can obtain automatically the Erlang programs satisfying the given specification.