@inproceedings{e34d61665c31450fb10e81e83ae0486a,
title = "Ensuring termination by typability",
abstract = "A term terminates if all its reduction sequences are of finite length. We show four type systems that ensure termination of well-typed π-calculas processes. The systems are obtained by successive refinements of the types of the simply typed π-calculas. 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.",
keywords = "Concurrency, Termination, The π-calculas, Type system",
author = "Yuxin Deng and Davide Sangiorgi",
year = "2004",
doi = "10.1007/1-4020-8141-3\_47",
language = "英语",
isbn = "1402081405",
series = "IFIP Advances in Information and Communication Technology",
publisher = "Springer New York LLC",
pages = "619--632",
booktitle = "Exploring New Frontiers of Theoretical Informatics - IFIP 18th World Computer Congress TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004",
note = "IFIP 18th World Computer Congress, TC1 and 3rd International Conference on Theoretical Computer Science, TCS 2004 ; Conference date: 22-08-2004 Through 27-08-2004",
}