Type inference for the (TODO: linear) π-calculus with product and sum types (TODO: and recursion/replication).
Type inference here is "co-contextual": given a process P, we try to infer Γ such that Γ ⊢ P.
The context Γ is built from the usages in P.
The soundness of type inference is intrinsic.
TODO: show that type inference is complete.