{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:29:26Z","timestamp":1750307366645,"version":"3.41.0"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2010,7,1]],"date-time":"2010-07-01T00:00:00Z","timestamp":1277942400000},"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":[[2010,7]]},"abstract":"<jats:p>\n            \u039b\u03bc-calculus is a B\u00f6hm-complete extension of Parigot's \u039b\u03bc-calculus closely related with delimited control in functional programming. In this article, we investigate the meta-theory of untyped \u039b\u03bc-calculus by proving confluence of the calculus and characterizing the basic observables for the Separation theorem,\n            <jats:italic>canonical normal forms<\/jats:italic>\n            . Then, we define \u039b\n            <jats:sub>\n              <jats:italic>s<\/jats:italic>\n            <\/jats:sub>\n            , a new type system for \u039b\u03bc-calculus that contains a special type construction for streams, and prove that strong normalization and type preservation hold. Thanks to the new typing discipline of \u039b\n            <jats:sub>\n              <jats:italic>s<\/jats:italic>\n            <\/jats:sub>\n            , new computational behaviors can be observed, which were forbidden in previous type systems for \u03bb\u03bc-calculi. Those new typed computational behaviors witness the stream interpretation of \u039b\u03bc-calculus.\n          <\/jats:p>","DOI":"10.1145\/1805950.1805958","type":"journal-article","created":{"date-parts":[[2010,7,15]],"date-time":"2010-07-15T12:48:46Z","timestamp":1279198126000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Typing streams in the \u039b\u03bc-calculus"],"prefix":"10.1145","volume":"11","author":[{"given":"Alexis","family":"Saurin","sequence":"first","affiliation":[{"name":"INRIA Saclay and \u00c9cole Polytechnique, Cedex, France"}]}],"member":"320","published-online":{"date-parts":[[2010,7,20]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9006-0"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Baba K. Hirokawa S. and Fujita K.-E. 2001. Parallel reduction in type free lambda\/mu-calculus. Electron. Notes Theoret. Comput. Sci. 42.  Baba K. Hirokawa S. and Fujita K.-E. 2001. Parallel reduction in type free lambda\/mu-calculus. Electron. Notes Theoret. Comput. Sci. 42.","DOI":"10.1016\/S1571-0661(04)80878-8"},{"key":"e_1_2_1_3_1","unstructured":"B\u00f6hm C. 1968. Alcune propriet\u00e0 delle forme \u03b2 &eta;-normali nel \u03bbK-calcolo. Publicazioni dell'Istituto per le Applicazioni del Calcolo 696.  B\u00f6hm C. 1968. Alcune propriet\u00e0 delle forme \u03b2 &eta;-normali nel \u03bbK-calcolo. Publicazioni dell'Istituto per le Applicazioni del Calcolo 696."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"David R. and Py W. 2001. \u03bb&mu;-calculus and B\u00f6hm's theorem. J. Symb. Logic.  David R. and Py W. 2001. \u03bb&mu;-calculus and B\u00f6hm's theorem. J. Symb. Logic.","DOI":"10.2307\/2694930"},{"volume-title":"Proceedings of the LPAR'94","series-title":"Lecture Notes in Articifial Intelligence","author":"de Groote P.","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002667"},{"key":"e_1_2_1_7_1","first-page":"1","article-title":"The maximality of the typed lambda caluclus and of cartesian closed categories","volume":"68","author":"Do\u0161en K.","year":"2000","journal-title":"Publications de l'Institut Math\u00e9matique"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00168-9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328484"},{"key":"e_1_2_1_14_1","unstructured":"Howard W. A. 1980. The formulae-as-type notion of construction 1969. In To H. B. Curry: Essays in Combinatory Logic Lambda Calculus and Formalism J. P. Seldin and R. Hindley Eds. Academic Press New York 479--490.  Howard W. A. 1980. The formulae-as-type notion of construction 1969. In To H. B. Curry: Essays in Combinatory Logic Lambda Calculus and Formalism J. P. Seldin and R. Hindley Eds. Academic Press New York 479--490."},{"key":"e_1_2_1_15_1","unstructured":"Joly T. 2000. Codages s\u00e9parabilit\u00e9 et repr\u00e9sentation de fonctions en \u03bb-calcul simplement typ\u00e9 et dans d'autres syst\u00e8mes de types. Ph.D. dissertation Universit\u00e9 Paris VII.  Joly T. 2000. Codages s\u00e9parabilit\u00e9 et repr\u00e9sentation de fonctions en \u03bb-calcul simplement typ\u00e9 et dans d'autres syst\u00e8mes de types. Ph.D. dissertation Universit\u00e9 Paris VII."},{"key":"e_1_2_1_16_1","unstructured":"Krivine J.-L. 1993. Lambda-calculus Types and Models. Ellis Horwood.   Krivine J.-L. 1993. Lambda-calculus Types and Models. Ellis Horwood."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1992.185523"},{"volume-title":"Proceedings of the IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","year":"1996","author":"Ong L.","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","unstructured":"Pagani M. and Saurin A. 2008. Stream associative nets and \u039b&mu;-calculus. Tech. rep. 6431 INRIA.  Pagani M. and Saurin A. 2008. Stream associative nets and \u039b&mu;-calculus. Tech. rep. 6431 INRIA."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the Russian Conference on Logic Programming. Lecture Notes in Articifial Intelligence","volume":"592","author":"Parigot M.","year":"1991"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/645706.663989"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287602"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.2307\/2275652"},{"key":"e_1_2_1_24_1","unstructured":"Py W. 1998. Confluence en \u03bb&mu;-calcul. Ph.D. dissertation Universit\u00e9 de Savoie.  Py W. 1998. Confluence en \u03bb&mu;-calcul. Ph.D. dissertation Universit\u00e9 de Savoie."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.48"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_13"},{"key":"e_1_2_1_27_1","unstructured":"Saurin A. 2008b. Une \u00e9tude logique du contr\u00f4le appliqu\u00e9e \u00e0 la programmation fonctionnelle et logique. Ph.D. dissertation \u00c9cole Polytechnique.  Saurin A. 2008b. Une \u00e9tude logique du contr\u00f4le appliqu\u00e9e \u00e0 la programmation fonctionnelle et logique. Ph.D. dissertation \u00c9cole Polytechnique."},{"key":"e_1_2_1_28_1","first-page":"1","article-title":"\u03bb-definable functionals and \u03b2&eta; conversion","volume":"22","author":"Statman R.","year":"1983","journal-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1805950.1805958","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1805950.1805958","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:22:42Z","timestamp":1750245762000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1805950.1805958"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,7]]},"references-count":28,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2010,7]]}},"alternative-id":["10.1145\/1805950.1805958"],"URL":"https:\/\/doi.org\/10.1145\/1805950.1805958","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2010,7]]},"assertion":[{"value":"2008-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-07-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}