@ARTICLE{DengSangiorgi06,
  title = {{Ensuring Termination by Typability}},
  author = {{Yuxin} {Deng} and {Davide} {Sangiorgi}},
  journal = {Information and Computation},
  pages = {1045-1082},
  abstract = {A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed π-calculus processes. The systems are obtained by successive refinements of the types of the simply typed π-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. },
  publisher = {Elsevier},
  volume = {204},
  number = {7},
  year = {2006},
  url = {http://www.cs.unibo.it/~sangio/DOC_public/ter_typeFULL.ps.gz},
  doi = {10.1016/j.ic.2006.03.002},
  invited = {N},
  partner = {UNIBO},
  status = {public},
  task = {T3.2},
}