{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,27]],"date-time":"2026-09-27T01:08:11Z","timestamp":1790471291044,"version":"4.1.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"Inria\/JSPS EA","award":["CRECOGI"],"award-info":[{"award-number":["CRECOGI"]}]},{"DOI":"10.13039\/501100005304","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-14-CE25-0005, ANR-16-CE25-0011"],"award-info":[{"award-number":["ANR-14-CE25-0005, ANR-16-CE25-0011"]}],"id":[{"id":"10.13039\/501100005304","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n            We introduce a type system for the \u03c0-calculus which is designed to guarantee that typable processes are\n            <jats:italic>well-behaved<\/jats:italic>\n            , namely they never produce a run-time error and, even if they may diverge, there is always a chance for them to \u201cfinish their work\u201d, i.e., to reduce to an idle process. The introduced type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is \u03a0\n            <jats:sub>2<\/jats:sub>\n            <jats:sup>0<\/jats:sup>\n            -complete, there is a way to show that the system is\n            <jats:italic>complete<\/jats:italic>\n            , i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.\n          <\/jats:p>","DOI":"10.1145\/3290320","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Intersection types and runtime errors in the pi-calculus"],"prefix":"10.1145","volume":"3","author":[{"given":"Ugo","family":"Dal Lago","sequence":"first","affiliation":[{"name":"University of Bologna, Italy \/ Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Marc","family":"de Visme","sequence":"additional","affiliation":[{"name":"University of Lyon, France \/ ENS Lyon, France \/ CNRS, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Damiano","family":"Mazza","sequence":"additional","affiliation":[{"name":"CNRS, France \/ University of Paris 13, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Akira","family":"Yoshimizu","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236789"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01386340"},{"key":"e_1_2_2_3_1","unstructured":"Henk P. Barendregt. 1984. The Lambda Calculus (revised ed.). North Holland.  Henk P. Barendregt. 1984. The Lambda Calculus (revised ed.). North Holland."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236968"},{"key":"e_1_2_2_5_1","doi-asserted-by":"crossref","unstructured":"Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions See { Gastin and Laroussinie 2010 } 222\u2013236.   Lu\u00eds Caires and Frank Pfenning. 2010. Session Types as Intuitionistic Linear Propositions See { Gastin and Laroussinie 2010 } 222\u2013236.","DOI":"10.1007\/978-3-642-15375-4_16"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_21"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19810270205"},{"key":"e_1_2_2_10_1","volume-title":"Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8, 4","author":"Lago Ugo Dal","year":"2011","unstructured":"Ugo Dal Lago and Marco Gaboardi . 2011. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8, 4 ( 2011 ). Ugo Dal Lago and Marco Gaboardi. 2011. Linear Dependent Types and Relative Completeness. Logical Methods in Computer Science 8, 4 (2011)."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005112"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_2_2_13_1","unstructured":"Marc de Visme and Damiano Mazza. 2017. On the Concurrent Meaning of Logical Correctness. (2017). Unpublished manuscript. Available on the second author\u2019s web page.  Marc de Visme and Damiano Mazza. 2017. On the Concurrent Meaning of Logical Correctness. (2017). Unpublished manuscript. Available on the second author\u2019s web page."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.07.007"},{"key":"e_1_2_2_15_1","doi-asserted-by":"crossref","unstructured":"Romain Demangeon Daniel Hirschkoff and Davide Sangiorgi. 2010b. Termination in Impure Concurrent Languages See { Gastin and Laroussinie 2010 } 328\u2013342.   Romain Demangeon Daniel Hirschkoff and Davide Sangiorgi. 2010b. Termination in Impure Concurrent Languages See { Gastin and Laroussinie 2010 } 328\u2013342.","DOI":"10.1007\/978-3-642-15375-4_23"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_39"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.06.005"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/113445.113468"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)70271-4"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.01.028"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/645392.651876"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328472"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_2_28_1","volume-title":"An Analysis of the Core-ML Language: Expressive Power and Type Reconstruction. In Proc. of ICALP 1994 (Lecture Notes in Computer Science)","volume":"820","author":"Kanellakis Paris C.","unstructured":"Paris C. Kanellakis , Gerd G. Hillebrand , and Harry G. Mairson . 1994 . An Analysis of the Core-ML Language: Expressive Power and Type Reconstruction. In Proc. of ICALP 1994 (Lecture Notes in Computer Science) , Vol. 820 . Springer, 83\u2013105. Paris C. Kanellakis, Gerd G. Hillebrand, and Harry G. Mairson. 1994. An Analysis of the Core-ML Language: Expressive Power and Type Reconstruction. In Proc. of ICALP 1994 (Lecture Notes in Computer Science), Vol. 820. Springer, 83\u2013105."},{"key":"e_1_2_2_29_1","volume-title":"TimeBoundedness. In Proc. of IFIP TCS 2000","author":"Kobayashi Naoki","year":"2000","unstructured":"Naoki Kobayashi . 2000 . Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom , TimeBoundedness. In Proc. of IFIP TCS 2000 , Sendai, Japan , August 17-19, 2000. 365\u2013389. Naoki Kobayashi. 2000. Type Systems for Concurrent Processes: From Deadlock-Freedom to Livelock-Freedom, TimeBoundedness. In Proc. of IFIP TCS 2000, Sendai, Japan, August 17-19, 2000. 365\u2013389."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/330249.330251"},{"key":"e_1_2_2_32_1","unstructured":"Jean-Louis Krivine. 1993. Lambda-calculus types and models. Masson.   Jean-Louis Krivine. 1993. Lambda-calculus types and models. Masson."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158094"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001407"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2594832.2594841"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647323.721503"},{"key":"e_1_2_2_39_1","volume-title":"The Pi-Calculus - a theory of mobile processes","author":"Sangiorgi Davide","unstructured":"Davide Sangiorgi and David Walker . 2001. The Pi-Calculus - a theory of mobile processes . Cambridge University Press . Davide Sangiorgi and David Walker. 2001. The Pi-Calculus - a theory of mobile processes. Cambridge University Press."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_17"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762219"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"},{"key":"e_1_2_2_43_1","volume-title":"Proc. of LICS","author":"Wells J. B.","year":"1994","unstructured":"J. B. Wells . 1994 . Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable . In Proc. of LICS 1994. IEEE Computer Society, 176\u2013185. J. B. Wells. 1994. Typability and Type-Checking in the Second-Order lambda-Calculus are Equivalent and Undecidable. In Proc. of LICS 1994. IEEE Computer Society, 176\u2013185."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.004"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290320","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290320","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290320"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":44,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290320"],"URL":"https:\/\/doi.org\/10.1145\/3290320","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}