{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:29:01Z","timestamp":1750307341909,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2011,7,20]],"date-time":"2011-07-20T00:00:00Z","timestamp":1311120000000},"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":[],"published-print":{"date-parts":[[2011,7,20]]},"DOI":"10.1145\/2003476.2003500","type":"proceedings-article","created":{"date-parts":[[2011,7,20]],"date-time":"2011-07-20T12:34:54Z","timestamp":1311165294000},"page":"173-182","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Linearity and recursion in a typed Lambda-calculus"],"prefix":"10.1145","author":[{"given":"Sandra","family":"Alves","sequence":"first","affiliation":[{"name":"Faculty of Science - University of Porto, Porto, Portugal"}]},{"given":"Maribel","family":"Fern\u00e1ndez","sequence":"additional","affiliation":[{"name":"King's College London, London, United Kingdom"}]},{"given":"M\u00e1rio","family":"Florido","sequence":"additional","affiliation":[{"name":"Faculty of Science - University of Porto, Porto, Portugal"}]},{"given":"Ian","family":"Mackie","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique, Paris, France"}]}],"member":"320","published-online":{"date-parts":[[2011,7,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391276.2391287"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.11.014"},{"key":"e_1_3_2_1_5_1","volume-title":"Linear recursion. CoRR, abs\/1001.3368","author":"Alves S.","year":"2010","unstructured":"S. Alves , M. Fern\u00e1ndez , M. Florido , and I. Mackie . Linear recursion. CoRR, abs\/1001.3368 , 2010 . S. Alves, M. Fern\u00e1ndez, M. Florido, and I. Mackie. Linear recursion. CoRR, abs\/1001.3368, 2010."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.005"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504081"},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","first-page":"27","volume-title":"Proc. FOSSACS'04","author":"Baillot P.","year":"2004","unstructured":"P. Baillot and V. Mogbil . Soft lambda-calculus: a language for polynomial time computation . In Proc. FOSSACS'04 , volume 2987 of LNCS , pages 27 -- 41 . Springer-Verlag , 2004 . P. Baillot and V. Mogbil. Soft lambda-calculus: a language for polynomial time computation. In Proc. FOSSACS'04, volume 2987 of LNCS, pages 27--41. Springer-Verlag, 2004."},{"key":"e_1_3_2_1_9_1","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt H. P.","year":"1984","unstructured":"H. P. Barendregt . The Lambda Calculus: Its Syntax and Semantics , volume 103 of Studies in Logic and the Foundations of Mathematics . North-Holland , 1984 . H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984."},{"key":"e_1_3_2_1_10_1","series-title":"Synthese Library 316","first-page":"57","volume-title":"the Scope of Logic, Methodology and Philosophy of Science","author":"Berger U.","year":"2002","unstructured":"U. Berger . Minimisation vs. recursion on the partial continuous functionals . In In the Scope of Logic, Methodology and Philosophy of Science , volume 1 of Synthese Library 316 , pages 57 -- 64 . Kluwer , 2002 . U. Berger. Minimisation vs. recursion on the partial continuous functionals. In In the Scope of Logic, Methodology and Philosophy of Science, volume 1 of Synthese Library 316, pages 57--64. Kluwer, 2002."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54487-9"},{"key":"e_1_3_2_1_12_1","first-page":"70","volume-title":"Workshop on Higher Order Operational Techniques in Semantics","volume":"41","author":"Bierman G. M.","year":"2000","unstructured":"G. M. Bierman , A. M. Pitts , and C. V. Russo . Operational properties of Lily, a polymorphic linear lambda calculus with recursion . In Workshop on Higher Order Operational Techniques in Semantics , volume 41 of ENTCS, pages 70 -- 88 . Elsevier , 2000 . G. M. Bierman, A. M. Pitts, and C. V. Russo. Operational properties of Lily, a polymorphic linear lambda calculus with recursion. In Workshop on Higher Order Operational Techniques in Semantics, volume 41 of ENTCS, pages 70--88. Elsevier, 2000."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129599002893"},{"key":"e_1_3_2_1_14_1","series-title":"Lecture Notes in Computer Science","first-page":"31","volume-title":"Computer Science Logic, 8th International Workshop, CSL'94, Kazimierz, Poland","author":"Bra\u00fcner T.","year":"1994","unstructured":"T. Bra\u00fcner . The Girard translation extended with recursion . In Computer Science Logic, 8th International Workshop, CSL'94, Kazimierz, Poland , volume 933 of Lecture Notes in Computer Science , pages 31 -- 45 . Springer , 1994 . T. Bra\u00fcner. The Girard translation extended with recursion. In Computer Science Logic, 8th International Workshop, CSL'94, Kazimierz, Poland, volume 933 of Lecture Notes in Computer Science, pages 31--45. Springer, 1994."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90230-Y"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.52"},{"key":"e_1_3_2_1_17_1","volume-title":"23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7--11, 2009. Proceedings","volume":"5771","author":"Egger J.","year":"2009","unstructured":"J. Egger , R. E. M\u00f8gelberg , and A. Simpson . Enriching an effect calculus with linear types. In Computer Science Logic , 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7--11, 2009. Proceedings , volume 5771 of Lecture Notes in Computer Science, pages 240--254. Springer , 2009 . J. Egger, R. E. M\u00f8gelberg, and A. Simpson. Enriching an effect calculus with linear types. In Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7--11, 2009. Proceedings, volume 5771 of Lecture Notes in Computer Science, pages 240--254. Springer, 2009."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00392-X"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004633"},{"issue":"6","key":"e_1_3_2_1_20_1","first-page":"393","article-title":"Lambda-calculus with director strings. Applicable Algebra in Engineering","volume":"15","author":"Fern\u00e1ndez M.","year":"2005","unstructured":"M. Fern\u00e1ndez , I. Mackie , and F.-R. Sinot . Lambda-calculus with director strings. Applicable Algebra in Engineering , Communication and Computing , 15 ( 6 ): 393 -- 437 , 2005 . M. Fern\u00e1ndez, I. Mackie, and F.-R. Sinot. Lambda-calculus with director strings. Applicable Algebra in Engineering, Communication and Computing, 15(6):393--437, 2005.","journal-title":"Communication and Computing"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.03.035"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190269"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/092\/1003197"},{"key":"e_1_3_2_1_26_1","volume-title":"Proofs and Types","author":"Girard J.-Y.","year":"1989","unstructured":"J.-Y. Girard , Y. Lafont , and P. Taylor . Proofs and Types . Cambridge Tracts in Theor. Comp. Sci. Cambridge University Press , 1989 . J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge Tracts in Theor. Comp. Sci. Cambridge University Press, 1989."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887654.1887684"},{"key":"e_1_3_2_1_29_1","volume-title":"An Introduction to Lambda Calculi for Computer Scientists","author":"Hankin C.","year":"2004","unstructured":"C. Hankin . An Introduction to Lambda Calculi for Computer Scientists , volume 2 . College Publications , 2004 . ISBN 0--9543006--5--3. C. Hankin. An Introduction to Lambda Calculi for Computer Scientists, volume 2. College Publications, 2004. ISBN 0--9543006--5--3."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788962"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_2_1_32_1","first-page":"13","volume-title":"Proc. of the Workshop on Implementation of Lazy Functional Languages","author":"Holmstr\u00f6m S.","year":"1988","unstructured":"S. Holmstr\u00f6m . Linear functional programming . In Proc. of the Workshop on Implementation of Lazy Functional Languages , pages 13 -- 32 , 1988 . S. Holmstr\u00f6m. Linear functional programming. In Proc. of the Workshop on Implementation of Lazy Functional Languages, pages 13--32, 1988."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/646728.703349"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.3.411"},{"key":"e_1_3_2_1_35_1","unstructured":"J. W. Klop. Combinatory Reduction Systems. PhD thesis Mathematisch Centrum Amsterdam 1980.  J. W. Klop. Combinatory Reduction Systems. PhD thesis Mathematisch Centrum Amsterdam 1980."},{"key":"e_1_3_2_1_36_1","volume-title":"Reflections on Type Theory","author":"Klop J. W.","year":"2007","unstructured":"J. W. Klop . New fixpoint combinators from old . Reflections on Type Theory , 2007 . J. W. Klop. New fixpoint combinators from old. Reflections on Type Theory, 2007."},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90091-7"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237804"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90100-4"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.018"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001131"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199483"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_3_2_1_44_1","series-title":"LNCS","first-page":"202","volume-title":"PARLE'91","author":"N\u00f6cker E.","year":"1991","unstructured":"E. N\u00f6cker , J. Smetsers , M. van Eekelen , and M. Plasmeijer . Concurrent clean . In PARLE'91 , volume 506 of LNCS , pages 202 -- 219 . Springer , 1991 . E. N\u00f6cker, J. Smetsers, M. van Eekelen, and M. Plasmeijer. Concurrent clean. In PARLE'91, volume 506 of LNCS, pages 202--219. Springer, 1991."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389462"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2001.932498"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539703432165"},{"key":"e_1_3_2_1_49_1","first-page":"347","volume-title":"Concepts and Methods","author":"Wadler P.","year":"1990","unstructured":"P. Wadler . Linear types can change the world! In IFIP TC 2 Conf. on Progr . Concepts and Methods , pages 347 -- 359 . North Holland , 1990 . P. Wadler. Linear types can change the world! In IFIP TC 2 Conf. on Progr. Concepts and Methods, pages 347--359. North Holland, 1990."},{"key":"e_1_3_2_1_50_1","first-page":"3","volume-title":"Topics in Types and Progr. Languages","author":"Walker D.","year":"2005","unstructured":"D. Walker . Substructural type systems. In Adv . Topics in Types and Progr. Languages , chapter 1, pages 3 -- 43 . MIT Press , Cambridge , 2005 . D. Walker. Substructural type systems. In Adv. Topics in Types and Progr. Languages, chapter 1, pages 3--43. MIT Press, Cambridge, 2005."},{"key":"e_1_3_2_1_51_1","volume-title":"Proc. ACM SIGPLAN Workshop on Types in Compilation. ACM Press","author":"Wansbrough K.","year":"2000","unstructured":"K. Wansbrough and S. P. Jones . Simple usage polymorphism . In Proc. ACM SIGPLAN Workshop on Types in Compilation. ACM Press , 2000 . K. Wansbrough and S. P. Jones. Simple usage polymorphism. In Proc. ACM SIGPLAN Workshop on Types in Compilation. ACM Press, 2000."},{"key":"e_1_3_2_1_52_1","first-page":"417","volume-title":"LNCS","author":"Yoshida N.","year":"2002","unstructured":"N. Yoshida , K. Honda , and M. Berger . Linearity and bisimulation. In FoSSaCS , LNCS , pages 417 -- 434 . Springer-Verlag , 2002 . N. Yoshida, K. Honda, and M. Berger. Linearity and bisimulation. In FoSSaCS, LNCS, pages 417--434. Springer-Verlag, 2002."}],"event":{"name":"PPDP '11: Symposium on Principles and Practices of Declarative Programming","sponsor":["University of Southern Denmark","Danish Agency for Science Technology and Innovation DASTI","SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Odense Denmark","acronym":"PPDP '11"},"container-title":["Proceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2003476.2003500","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2003476.2003500","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:06:22Z","timestamp":1750244782000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2003476.2003500"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7,20]]},"references-count":51,"alternative-id":["10.1145\/2003476.2003500","10.1145\/2003476"],"URL":"https:\/\/doi.org\/10.1145\/2003476.2003500","relation":{},"subject":[],"published":{"date-parts":[[2011,7,20]]},"assertion":[{"value":"2011-07-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}