Honda's pioneering papers on session types (and on everything else for that matter) are always worth reading. Yes, replicated input is !x(v1).P in pi-calculus,

Honda's pioneering papers on session types (and on everything else for that matter) are always worth reading. Yes, replicated input is !x(v1).P in pi-calculus, and Milner was directly inspired by linear logic's replication. > Still, overall I think I'm more optimistic about the possibility of capturing most reasonable forms of concurrent programming in a deadlock & race-free manner. I don't think you can, or indeed want to excise all forms of race condition from concurrent programs, for if you do that, there would be little concurrency left. You could only do deterministic concurrency, which is not what you want in many cases, e.g when you use concurrency to mask latency. For example how would you define a lock or mutex if all races are forbidden? You need race conditions, but you want them in homeopathic doses, you want them constrained and tightly controlled. I also doubt that concurrent programming patterns like dynamic deadlock detection and removal are amenable to a type-theoretic analysis in linear-logic based systems such as Caires & Pfenning's.