Formalizing a relational model of concurrent programs in a dependently typed environment

Sequential programming languages have already been formalized in dependently typed programming languages, but the computer based formalization of concurrent programs is still in its early days. The goal of our research is to formalize a relational model that describes the behavior of distributed concurrent programs in a theorem prover system. Our long term goals include the verification of the material of the subject titled ”Specification and Implementation of Distributed Systems”