Formalismes en programmation simultanée et / ou distribuée?

Mes antécédents provenaient de langages impératifs, principalement C, C ++ et Python. J'ai repris Scala, Erlang et un peu de Haskell quelques années plus tard et depuis, je me suis beaucoup intéressé à la programmation fonctionnelle et aux formalismes qui la sous-tendent.

Je m'intéresse également à la programmation simultanée et distribuée et j'ai étudié les formalismes derrière cela, en particulier ceux qui ont vu au moins une infime partie de la "lumière du jour" (par exemple, une utilisation réelle ou au moins une implémentation quelque part). Jusqu'à présent, je connais les processus de communication séquentiels, le modèle d'acteur, l'algèbre des processus de communication et le calcul des systèmes de communication. Parmi ceux-ci, je sais que le modèle d'acteur s'est réalisé dans des langues comme Erlang, Scala et Haskell.

Je me demande s'il y a des fondations que je devrais apprendre et pratiquer avant d'aborder ces domaines, s'il y en a un "classique" que je devrais étudier en premier, et s'il y en a d'autres populaires que j'ai pu manquer?

Le formalisme le plus largement utilisé est le -calculus de Milner, Parrow et Walker. Il s'agit d'une extension de CCS et se décline en de nombreuses variantes, dont certaines (le -calcul asynchrone ) tentent d'être une formalisation du modèle d'acteur. Il existe maintenant de nombreuses disciplines de frappe pour -calculi, dont les plus simples sont probablement les types de session de Honda. De tels types se diffusent lentement des articles de recherche aux implémentations de recherche.$\pi$$\pi$$\pi$