Formalności w programowaniu współbieżnym i / lub rozproszonym?

Moje tło wywodzi się z języków imperatywnych, głównie C, C ++ i Python. Kilka lat później wybrałem Scalę, Erlanga i trochę Haskella i od tego czasu bardzo zainteresowałem się programowaniem funkcjonalnym i formalizacjami.

Interesuje mnie również współbieżne i rozproszone programowanie i zastanawiam się nad formalizmami, szczególnie tymi, które widziały choć trochę „światła dziennego” (np. Zastosowanie w prawdziwym świecie lub przynajmniej gdzieś wdrożenie). Jak dotąd znam się na komunikowaniu procesów sekwencyjnych, modelu aktora, algebrze procesów komunikowania i rachunku systemów komunikacyjnych. Wśród nich wiem, że model Actor zrealizował się w takich językach jak Erlang, Scala i Haskell.

Zastanawiam się, czy istnieją podstawy, które powinienem nauczyć się i ćwiczyć przed zajęciem się tymi dziedzinami, czy istnieje „klasyczny”, który powinienem najpierw zbadać, i czy są jakieś inne popularne, których mogłem przegapić?

Najczęściej stosowanym formalizmem jest -calculus Milnera, Parrowa i Walkera. Jest rozszerzeniem CCS i występuje w wielu wariantach, z których niektóre (asynchroniczne -calculus) próbują być formalizacją modelu aktora. Istnieje wiele dyscyplin pisania dla -calculi, z których najprostszymi są prawdopodobnie typy sesji Hondy. Takie typy powoli rozprzestrzeniają się od prac badawczych do realizacji badań.$\pi$$\pi$$\pi$