The generalisation of Curry-Howard to parallelism was outlined in early interpretations of linear logic, I think Abramsky's [1] was the first, there has been a

The generalisation of Curry-Howard to parallelism was outlined in early interpretations of linear logic, I think Abramsky's [1] was the first, there has been a lot more work in this direction since. A good place to start to understand the relationship between functional and concurrent computation is Milner's Functions as Processes [2], it's incredibly simple, my mind was blown when I understood it (if you understand CPS transforms, you will find it natural, indeed, I'd say the Milner translation is the essence of CPS, see also [4]). A Curry-Howard correspondence of sorts has now been produced for linear logic and session-typable name passing processes [3]. [1] S. Abramsky, Computational Interpretations of Linear Logic. https://www.sciencedirect.com/science/article/pii/030439759390181R https://www.sciencedirect.com/science/article/pii/0304397593... [2] R. Milner, Functions as Processes. https://hal.inria.fr/inria-00075405/document https://hal.inria.fr/inria-00075405/document [3] L. Caires, F. Pfenning, Session Types as Intuitionistic Linear Propositions. https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.220.3453&rep=rep1&type=pdf https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.22... [4] H. Thielecke, Continuations, functions and jumps. https://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf https://www.cs.bham.ac.uk/~hxt/research/Logiccolumn8.pdf