Formalization of Concurrency

Reading about lambda calculus led to an interest in how concurrent processes could be explicated formally. I read Concurrent Lambda Calculus with Futures by Niehren, Schwinghammer (cool name), and Smolka. Futures seem considerably nicer than some of the synchronization primitives that I'm familiar with elsewhere. Looking further afield, I found papers and articles on describing various process calculi. Most date from the late 90s to early 2000s (Ambient calculus seems very much a product of the early 2000s). It seems like that field of research has died off since. Have there been any more recent attempts or should I simply content myself with what I've found?

Apologies as I'm smooth of the brain but if I understand you correctly you're talking about a form of notation that makes concurrent functional processes easier to write and understand? Does it account for branchings and synchronisations of arbitrary amounts and mixtures? And do you have some examples that could help someone like me get an entry understanding what's this about?

>>43836 This likely won't be as concrete as you'd like but I'll try my best. Process calculi attempt to represent concurrent processes as lambda calculus represents processes. They provide models with which to reason about concurrent processes using algebraic laws. Barring implementation errors, this verifies the formal correctness of a program's concurrency. Communicating Sequential Processes is probably the most well-known process calculus. From Hoare, it pretty quickly found a home in Bell Labs, where it shaped the concurrency model of Plan 9 and consequently Go. This link (https://swtch.com/~rsc/thread/) contains a good history of that from someone who worked on Plan 9. Plan 9 is a good resource for seeing CSP (again, a process calculus) in action.

>>43831 >ost date from the late 90s to early 2000s Maybe it's because of the failure of the transputer. >Have there been any more recent attempts The Go programming language, maybe. That said, writing a proof using an effective procedure (i.e. a static checker) to make sure some invariant holds is quite hard because you might have many shared resources, and many events performing operations over these resources. In most cases, the number of operations needed to ensure the invariant holds is quadratic because it needs to check each pair of events.

>>43831 You should look at TLA+, as I understand it it's used industrially for formal verification of distributed systems, and the same concepts mostly apply to multithreaded programs in a single CPU though I imagine that's a bit less popular.