{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:00:32Z","timestamp":1773478832643,"version":"3.50.1"},"publisher-location":"Boston","reference-count":19,"publisher":"Kluwer Academic Publishers","isbn-type":[{"value":"1402081405","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8141-3_47","type":"book-chapter","created":{"date-parts":[[2006,2,21]],"date-time":"2006-02-21T15:15:11Z","timestamp":1140534911000},"page":"619-632","source":"Crossref","is-referenced-by-count":6,"title":["Ensuring Termination by Typability"],"prefix":"10.1007","author":[{"given":"Yuxin","family":"Deng","sequence":"first","affiliation":[]},{"given":"Davide","family":"Sangiorgi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"47_CR1","unstructured":"M. Bezem. Mathematical background. In M. Bezem, J. Klop, and R. de Vrijer, editors, Term Rewriting Systems, pages 790\u2013825. Cambridge University Press, 2003."},{"key":"47_CR2","first-page":"60","volume":"2701","author":"G. Boudol","year":"2003","unstructured":"G. Boudol. On strong normalization in the intersection type discipline. LNCS, 2701:60\u201374, 2003.","journal-title":"LNCS"},{"issue":"2","key":"47_CR3","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/0304-3975(94)00275-4","volume":"142","author":"N. Dershowitz","year":"1995","unstructured":"N. Dershowitz and C. Hoot. Natural termination. Theoretical Computer Science, 142(2): 179\u2013207, 1995.","journal-title":"Theoretical Computer Science"},{"key":"47_CR4","first-page":"243","volume-title":"Hand-book of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Hand-book of Theoretical Computer Science, chapter 6, pages 243\u2013320. North-Holland, Amsterdam, 1990."},{"issue":"8","key":"47_CR5","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1145\/359138.359142","volume":"22","author":"N. Dershowitz","year":"1979","unstructured":"N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465\u2013476, 1979.","journal-title":"Communications of the ACM"},{"key":"47_CR6","volume-title":"PhD thesis","author":"C. Fournet","year":"1998","unstructured":"C. Fournet. The Join-Calculus: A Calculus for Distributed Mobile Programming. PhD thesis, Ecole Polytechnique, Paris, France, 1998."},{"key":"47_CR7","unstructured":"R. O. Gandy. Proofs of strong normalization. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980."},{"key":"47_CR8","doi-asserted-by":"crossref","unstructured":"C. Jones. A \u03c0-Calculus semantics for an object-based design notation. In E. Best, editor, Proc. CONCUR\u2019 93, volume 715 of LNCS, pages 158\u2013172. Springer, 1993.","DOI":"10.1007\/3-540-57208-2_12"},{"key":"47_CR9","unstructured":"R. Loader. Notes on simply typed lambda calculus. TechnicalReport 381, LFCS, University of Edinburgh, 1998."},{"issue":"2","key":"47_CR10","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1017\/S0960129500001407","volume":"2","author":"R. Milner","year":"1992","unstructured":"R. Milner. Functions as processes. Journal of Mathematical Structures in Computer Science, 2(2):119\u2013141, 1992.","journal-title":"Journal of Mathematical Structures in Computer Science"},{"key":"47_CR11","doi-asserted-by":"crossref","unstructured":"R. Milner. The polyadic \u03c0-Calculus A tutorial. In F. L. Bauer, W. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification, volume 94 of Series F. NATO ASI, Springer, 1993.","DOI":"10.1007\/978-3-642-58041-3_6"},{"key":"47_CR12","unstructured":"R. Milner. Communicating and Mobile Systems: the \u03c0-Calculus Cambridge University Press, May 1999."},{"key":"47_CR13","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1006\/inco.1999.2822","volume":"156","author":"U. Nestmann","year":"2000","unstructured":"U. Nestmann. What is a \u2018good\u2019 encoding of guarded choice? Journal of Information and Computation, 156:287\u2013319, 2000.","journal-title":"Journal of Information and Computation"},{"key":"47_CR14","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1017\/S0960129503004043","volume":"13","author":"C. Palamidessi","year":"2003","unstructured":"C. Palamidessi. Comparing the expressive power of the synchronous and asynchronous \u03c0-Calculi, Mathematical Structures in Computer Science, 13:685\u2013719, 2003.","journal-title":"Mathematical Structures in Computer Science"},{"key":"47_CR15","doi-asserted-by":"crossref","unstructured":"D. Sangiorgi. The typed \u03c0-Calculus at work: A proof of Jones\u2019sparallelisation theorem on concurrent objects. Theory and Practice of Object-Oriented Systems, 5(1), 1999.","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<25::AID-TAPO3>3.0.CO;2-A"},{"key":"47_CR16","unstructured":"D. Sangiorgi. Termination of processes, Dec. 2001. Available from ftp:\/\/ftp-sop.inria.fr\/mimosa\/personnel\/davides ."},{"key":"47_CR17","unstructured":"D. Sangiorgi and D. Walker. The \u03c0-Calculus: a Theory of Mobile Processes. Cambridge University Press, 2001."},{"issue":"1","key":"47_CR18","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"R. Statman. The typed \u03bb-calculus is not elementary recursive. Theoretical Computer Science, 9(1):73\u201381, 1979.","journal-title":"Theoretical Computer Science"},{"key":"47_CR19","doi-asserted-by":"crossref","unstructured":"N. Yoshida, M. Berger, and K. Honda. Strong normalisation in the pi-calculus. In Logic in Computer Science, pages 311\u2013322, 2001.","DOI":"10.1109\/LICS.2001.932507"}],"container-title":["IFIP International Federation for Information Processing","Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8141-3_47.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T20:45:35Z","timestamp":1736282735000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8141-3_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081405"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8141-3_47","relation":{},"subject":[]}}