SENSORIA All Publications |
|
Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
Ensuring Termination by Typability @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}, }
|