Ensuring termination by typability
 
                 Yuxin Deng and Davide Sangiorgi


 A term terminates if all its reduction sequences are of finite
 length. We show four type systems that ensure termination of
 well-typed $\pi$-calculus  processes. The systems are obtained by
 successive refinements of the types of the simply typed $\pi$-calculus.
 For all (but one of) the type systems we also present upper bounds to the
 number of steps well-typed processes take to terminate. The
 termination proofs use techniques from term rewriting systems. 

 We show the usefulness of the type systems on some non-trivial
 examples: the encodings of primitive recursive functions, the protocol
 for encoding separate choice in terms of parallel composition, a
 symbol table implemented as a dynamic chain of cells.