A π-calculus with linear types ensures the privacy and safety of concurrent communication. Allowing shared (unlimited) communication however is key to model real-world services. To implement a decision procedure that type checks a π-calculus process with both linear and shared types one can either rely on user-provided type annotations, or infer the types of the channels created within the process. We choose to reduce the burden on the user by following the latter approach. If we limit ourselves to the shared π-calculus, we can traverse a process bottom-up and eagerly solve typing constraints into substitutions and apply them to the typing context. However, in a setting with both linear and shared types, typing constraints do not always come with a most general solution, and thus cannot always be eagerly solved.

We provide a co-contextual typing inference algorithm that traverses processes bottom-up and, in addition to the typing context, collects a set of typing constraints. We then solve those constraints that have a most general solution (by using well-known unification algorithms) while deferring the rest until more information becomes available. We state clear soundness and completeness theorems separating both these phases, and a progress theorem that ensures that only those constraints without a most general solution are deferred. This work is being mechanised in Agda.