Implicit typing `a la ML for the join-calculus

We adapt the Damas-Milner typing discipline to the join-calculus. The main result is a new generalization criterion that extends the polymorphism of ML to join-definitions. We prove the correctness of our typing rules with regard to a chemical semantics. We also relate typed extensions of the core join-calculus to functional languages. 1 Introduction The distributed implementation of concurrent calculi with message passing raises the problem of implementing communication channels, which finally reduces to the specification of channel managers. In order to reflect this need in the language itself, a new formalism has been recently introduced : the join-calculus [2]. This calculus is similar to Milner’s asynchronous ß-calculus, except that the operations of restriction, reception and replication are all combined into a single receptor definition.