A Formalisation of a Turing-Complete Choreographic Language in Coq

A formalisation in Coq of: a choreographic programming language (CC.v) Kleene's theory of partial recursive functions (Kleene.v) an encoding of Kleene's RPFs as choreographies and the proof of its correctness (Implementation.v) a calculus of stateful processes (SP.v) a certified compiler for the choreographic language to the process calculus (EPP.v, Merge.v, Pruning.v