{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T19:09:44Z","timestamp":1725995384871},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"5","funder":[{"DOI":"10.13039\/501100001691","name":"Kakenhi","doi-asserted-by":"crossref","award":["2.02E+15"],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["231620"],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2010,5]]},"abstract":"We propose a type system for lock-freedom in the \u03c0-calculus, which guarantees that certain communications will eventually succeed. Distinguishing features of our type system are: it can verify lock-freedom of concurrent programs that have sophisticated recursive communication structures; it can be fully automated; it is hybrid, in that it combines a type system for lock-freedom with local reasoning about deadlock-freedom, termination, and confluence analyses. Moreover, the type system is parameterized by deadlock-freedom\/termination\/confluence analyses, so that any methods (e.g. type systems and model checking) can be used for those analyses. A lock-freedom analysis tool has been implemented based on the proposed type system, and tested for nontrivial programs.<\/jats:p>","DOI":"10.1145\/1745312.1745313","type":"journal-article","created":{"date-parts":[[2010,5,25]],"date-time":"2010-05-25T13:08:17Z","timestamp":1274792897000},"page":"1-49","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["A hybrid type system for lock-freedom of mobile processes"],"prefix":"10.1145","volume":"32","author":[{"given":"Naoki","family":"Kobayashi","sequence":"first","affiliation":[{"name":"Tohoku University, Miyagi, Japan"}]},{"given":"Davide","family":"Sangiorgi","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Bologna, Bologna, Italy"}]}],"member":"320","published-online":{"date-parts":[[2008,5,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.08.017"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180475.1180480"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.09.014"},{"key":"e_1_2_2_4_1","volume-title":"Proceedings of CONCUR'98","volume":"1466","author":"Bodei C."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2755"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/582419.582440"},{"key":"e_1_2_2_7_1","volume-title":"Proceedings of CONCUR","volume":"962","author":"Brinksma E.","year":"1995"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770730.1770733"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00137-8"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503278"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250771"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0072"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the Conference on Trusted Global Computing (TGC'08)","volume":"4912","author":"Demangeon R."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.03.002"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.01.005"},{"key":"e_1_2_2_17_1","unstructured":"Holzmann G. J. 2003. The SPIN Model Checker: Premier and Reference Manual. Addison-Wesley Reading MA. Holzmann G. J. 2003. The SPIN Model Checker: Premier and Reference Manual. Addison-Wesley Reading MA."},{"key":"e_1_2_2_18_1","volume-title":"Proceedings of the European Symposium on Programming (ESOP'00)","volume":"1782","author":"Honda K."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1286821.1286822"},{"key":"e_1_2_2_20_1","unstructured":"Hugo Vieira L. C. and Viegas R. 2005. The spatial logic model checker user's manual v1.0. TR-DI\/FCT\/UNL-05 http:\/\/ctp.di.fct.unl.pt\/SLMC\/. Hugo Vieira L. C. and Viegas R. 2005. The spatial logic model checker user's manual v1.0. TR-DI\/FCT\/UNL-05 http:\/\/ctp.di.fct.unl.pt\/SLMC\/."},{"key":"e_1_2_2_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of CONCUR'93","author":"Jones C."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(02)93171-8"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0179-x"},{"key":"e_1_2_2_24_1","unstructured":"Kobayashi N. 2005b. TyPiCal: A type-based static analyzer for the pi-calculus. Tool available at http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/typical\/. Kobayashi N. 2005b. TyPiCal: A type-based static analyzer for the pi-calculus. Tool available at http:\/\/www.kb.ecei.tohoku.ac.jp\/~koba\/typical\/."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"Kobayashi N. Suenaga K. and Wischik L. 2006. Resource usage analysis for the pi-calculus. Logic. Meth. Comput. Sci. 2 3:4 1--42. Kobayashi N. Suenaga K. and Wischik L. 2006. Resource usage analysis for the pi-calculus. Logic. Meth. Comput. Sci. 2 3:4 1--42.","DOI":"10.2168\/LMCS-2(3:4)2006"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003683"},{"key":"e_1_2_2_29_1","volume-title":"Logic and Algebra of Specification","author":"Milner R."},{"key":"e_1_2_2_30_1","volume-title":"Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP'95)","volume":"944","author":"Natarajan V."},{"key":"e_1_2_2_31_1","volume-title":"Pict: A programming language based on the pi-calculus. In Proof, Language and Interaction: Essays in Honour of Robin Milner","author":"Pierce B. C.","year":"2000"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00040-7"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004810"},{"key":"e_1_2_2_35_1","unstructured":"Sangiorgi D. and Walker D. 2001. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press Cambridge MA. Sangiorgi D. and Walker D. 2001. The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press Cambridge MA."},{"key":"e_1_2_2_36_1","volume-title":"Proceedings of ESOP","volume":"4421","author":"Suenaga K.","year":"2007"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387676"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.004"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1745312.1745313","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T18:56:48Z","timestamp":1672340208000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1745312.1745313"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5,24]]},"references-count":38,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,5]]}},"alternative-id":["10.1145\/1745312.1745313"],"URL":"https:\/\/doi.org\/10.1145\/1745312.1745313","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,5,24]]},"assertion":[{"value":"2008-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-05-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}