{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:36:01Z","timestamp":1750221361659,"version":"3.41.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,1,31]],"date-time":"2018-01-31T00:00:00Z","timestamp":1517356800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,1,31]]},"abstract":"<jats:p>We show characterisation results for normalisation, head-normalisation, and strong normalisation for \u03bb \u03bc using intersection types. We reach these results for a strict notion of type assignment for \u03bb \u03bc that is the natural restriction of the domain-based system of van Bakel et al. (2011) for \u03bb \u03bc by limiting the type inclusion relation to just intersection elimination. We show that this system respects \u03b2 \u03bc-equality, by showing both soundness and completeness results. We then define a notion of reduction on derivations that corresponds to cut-elimination, and show that this is strongly normalisable.<\/jats:p>\n          <jats:p>We use this strong normalisation result to show an approximation result, and through that a characterisation of head-normalisation. Using the approximation result, we show that there is a very strong relation between the system of van Bakel et al. (2011) and ours.<\/jats:p>\n          <jats:p>We then introduce a notion of type assignment that eliminates \u03c9 as an assignable type, and show, using the strong normalisation result for derivation reduction, that all terms typeable in this system are strongly normalisable as well, and show that all strongly normalisable terms are typeable.<\/jats:p>\n          <jats:p>We conclude by adding type variables to our system, and show that system essentially is that of van Bakel (2010b).<\/jats:p>","DOI":"10.1145\/3149823","type":"journal-article","created":{"date-parts":[[2018,2,16]],"date-time":"2018-02-16T16:07:08Z","timestamp":1518797228000},"page":"1-47","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Characterisation of Normalisation Properties for \u03bb\u03bc using Strict Negated Intersection Types"],"prefix":"10.1145","volume":"19","author":[{"given":"Steffen Van","family":"Bakel","sequence":"first","affiliation":[{"name":"Department of Computing, Imperial College London, 180 Queen\u2019s Gate, London SW7 2BZ, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,2,15]]},"reference":[{"volume":"2719","volume-title":"Proceedings of the 30th International Colloquium on Automata, Languages and Programming (ICALP\u201903)","author":"Ariola Z. M.","key":"e_1_2_1_1_1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90297-S"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00073-6"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.020"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.04.010"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of 5th International Workshop Intersection Types and Related Systems (ITRS\u201910)","volume":"45","author":"van Bakel S.","year":"2010"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1922649.1922657"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2012-770"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"S. van Bakel. 2016. Approximation and (Head) normalisation for \u03bb&mu; using strict intersection types (Electronic Proceedings in Theoretical Computer Science) Vol. 242. http:\/\/www.doc.ic.ac.uk\/&sim;svb\/Research\/Papers\/Lmu-Strict.pdf.  S. van Bakel. 2016. Approximation and (Head) normalisation for \u03bb&mu; using strict intersection types (Electronic Proceedings in Theoretical Computer Science) Vol. 242. http:\/\/www.doc.ic.ac.uk\/&sim;svb\/Research\/Papers\/Lmu-Strict.pdf.","DOI":"10.4204\/EPTCS.242.4"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21691-6_18"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of 6th International Workshop on Intersection Types and Related Systems (ITRS\u201912)","volume":"121","author":"van Bakel S.","year":"2012"},{"key":"e_1_2_1_12_1","unstructured":"S. van Bakel F. Barbanera and U. de\u2019Liguoro. 2017. Intersection types for \u03bb&mu;. Logical Methods in Computer Science (2017). To appear.  S. van Bakel F. Barbanera and U. de\u2019Liguoro. 2017. Intersection types for \u03bb&mu;. Logical Methods in Computer Science (2017). To appear."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560586_8"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006762"},{"volume":"164","volume-title":"Proceedings of 6th International Workshop on Classical Logic and Computation 2014 (CL8C\u201914) (Electronic Proceedings in Theoretical Computer Science)","author":"van Bakel S.","key":"e_1_2_1_15_1"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"e_1_2_1_17_1","unstructured":"H. Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics (revised ed.). North-Holland Amsterdam.  H. Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics (revised ed.). North-Holland Amsterdam."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_19_1","unstructured":"C. B\u00f6hm. 1968. Alcune propiet\u00e1 delle forme \u03b2&eta;-normali nel \u03bbk-calcolo. Pubblicazioni 696 Instituto Nazionale per le Applicazioni del Calcolo. Roma (1968).  C. B\u00f6hm. 1968. Alcune propiet\u00e1 delle forme \u03b2&eta;-normali nel \u03bb k -calcolo. Pubblicazioni 696 Instituto Nazionale per le Applicazioni del Calcolo. Roma (1968)."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.2307\/2269326"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"e_1_2_1_22_1","doi-asserted-by":"crossref","unstructured":"M. Coppo M. Dezani-Ciancaglini F. Honsell and G. Longo. 1984. Extended type structures and filter lambda models. In Logic Colloquium 82 G. Lolli G. Longo and A. Marcja (Eds.). North-Holland Amsterdam the Netherlands 241--262.  M. Coppo M. Dezani-Ciancaglini F. Honsell and G. Longo. 1984. Extended type structures and filter lambda models. In Logic Colloquium 82 G. Lolli G. Longo and A. Marcja (Eds.). North-Holland Amsterdam the Netherlands 241--262.","DOI":"10.1016\/S0049-237X(08)71819-6"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351262"},{"key":"e_1_2_1_24_1","unstructured":"H. B. Curry and R. Feys. 1958. Combinatory Logic. Vol. 1. North-Holland Amsterdam.  H. B. Curry and R. Feys. 1958. Combinatory Logic. Vol. 1. North-Holland Amsterdam."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of 5th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201994)","volume":"822","author":"de Groote Ph.","year":"1994"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"C. A. Gunter and D. S. Scott. 1990. Semantic domains. In Handbook of Theoretical Computer Science J. van Leeuwen (Ed.). North-Holland 633--674.   C. A. Gunter and D. S. Scott. 1990. Semantic domains. In Handbook of Theoretical Computer Science J. van Leeuwen (Ed.). North-Holland 633--674.","DOI":"10.1016\/B978-0-444-88074-1.50017-2"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"J. R. Hindley. 1997. Basic Simple Type Theory. Cambridge University Press.   J. R. Hindley. 1997. Basic Simple Type Theory. Cambridge University Press.","DOI":"10.1017\/CBO9780511608865"},{"volume":"8858","volume-title":"Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS\u201914)","author":"Kikuchi K.","key":"e_1_2_1_29_1"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82619-2"},{"key":"e_1_2_1_31_1","unstructured":"U. de\u2019Liguoro. 2016. The approximation theorem for the \u039b&mu;-calculus. Mathematical Structures in Computer Science FirstView (2016) 1--21.  U. de\u2019Liguoro. 2016. The approximation theorem for the \u039b&mu;-calculus. Mathematical Structures in Computer Science FirstView (2016) 1--21."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263722"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of 3rd International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR\u201992)","volume":"624","author":"Parigot M.","year":"1992"},{"volume-title":"To H. B. Curry, Essays in Combinatory Logic, Lambda-Calculus and Formalism","author":"Pottinger G.","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","unstructured":"W. Py. 1998. Confluence en \u03bb&mu;-Calcul. Th\u00e8se de Doctorat. Universit\u00e9 de Savoie.  W. Py. 1998. Confluence en \u03bb&mu;-Calcul. Th\u00e8se de Doctorat. Universit\u00e9 de Savoie."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90069-5"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_11"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003141"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205036"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3149823","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3149823","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:26:18Z","timestamp":1750213578000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3149823"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,31]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1,31]]}},"alternative-id":["10.1145\/3149823"],"URL":"https:\/\/doi.org\/10.1145\/3149823","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,1,31]]},"assertion":[{"value":"2017-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-02-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}