A Formal Theory of Choreographic Programming in Coq

Dataset

Description

A formalisation in Coq of: a choreographic programming language (CC.v) a calculus of stateful processes (SP.v) a certified compiler for the choreographic language to the process calculus (EPP.v, EPPTheorem.v) Coq version: 8.13.2
Date made available5. Sept 2022
PublisherZenodo
  • Certifying Choreography Compilation

    Cruz-Filipe, L., Montesi, F. & Peressotti, M., 2021, Theoretical Aspects of Computing – ICTAC 2021 : 18th International Colloquium. Cerone, A. & Olveczky, P. C. (eds.). Springer Science+Business Media, p. 115-133 (Lecture Notes in Computer Science, Vol. 12819 LNCS).

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Cite this