{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T21:47:09Z","timestamp":1743025629846,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031177149"},{"type":"electronic","value":"9783031177156"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-17715-6_7","type":"book-chapter","created":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T09:02:27Z","timestamp":1664701347000},"page":"78-95","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Quantitative Weak Linearisation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8840-5587","authenticated-orcid":false,"given":"Sandra","family":"Alves","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5141-0438","authenticated-orcid":false,"given":"Daniel","family":"Ventura","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,3]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679682000012X","volume":"30","author":"B Accattoli","year":"2020","unstructured":"Accattoli, B., Graham-Lengrand, S., Kesner, D.: Tight typings and split bounds, fully developed. J. Funct. Program. 30, e14 (2020)","journal-title":"J. Funct. Program."},{"key":"7_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-030-02768-1_3","volume-title":"Programming Languages and Systems","author":"B Accattoli","year":"2018","unstructured":"Accattoli, B., Guerrieri, G.: Types of fireballs. In: Ryu, S. (ed.) APLAS 2018. LNCS, vol. 11275, pp. 45\u201366. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-02768-1_3"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-030-17184-1_15","volume-title":"Programming Languages and Systems","author":"B Accattoli","year":"2019","unstructured":"Accattoli, B., Guerrieri, G., Leberle, M.: Types by need. In: Caires, L. (ed.) ESOP 2019. LNCS, vol. 11423, pp. 410\u2013439. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17184-1_15"},{"unstructured":"Alves, S.: Linearisation of the lambda calculus. Ph.D. thesis, University of Porto (2007)","key":"7_CR4"},{"doi-asserted-by":"crossref","unstructured":"Alves, S., Fern\u00e1ndez, M., Florido, M., Mackie, I.: Linearity and recursion in a typed lambda-calculus. In: Proceedings of the 13th ACM SIGPLAN Symposium on Principles and Practices of Declarative Programming, pp. 173\u2013182. ACM (2011)","key":"7_CR5","DOI":"10.1145\/2003476.2003500"},{"issue":"1","key":"7_CR6","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.tcs.2005.06.005","volume":"342","author":"S Alves","year":"2005","unstructured":"Alves, S., Florido, M.: Weak linearization of the lambda calculus. Theor. Comput. Sci. 342(1), 79\u2013103 (2005)","journal-title":"Theor. Comput. Sci."},{"unstructured":"Alves, S., Kesner, D., Ventura, D.: A quantitative understanding of pattern matching. In: 25th International Conference on Types for Proofs and Programs. LIPIcs, vol. 175, pp. 3:1\u20133:36. Schloss Dagstuhl (2019)","key":"7_CR7"},{"issue":"2","key":"7_CR8","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/0304-3975(94)00279-7","volume":"142","author":"A Asperti","year":"1995","unstructured":"Asperti, A., Laneve, C.: Paths, computations and labels in the $$\\lambda $$-calculus. Theor. Comput. Sci. 142(2), 277\u2013297 (1995)","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Balabonski, T., Barenbaum, P., Bonelli, E., Kesner, D.: Foundations of strong call by need. Proc. ACM Program. Lang. 1(ICFP), 20:1\u201320:29 (2017)","key":"7_CR9","DOI":"10.1145\/3110264"},{"unstructured":"Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundation of Mathematics, vol. 103. North-Holland (1984)","key":"7_CR10"},{"doi-asserted-by":"crossref","unstructured":"Barendregt, H.P., Bergstra, J., Klop, J.W., Volken, H.: Degrees, reductions and representability in the lambda calculus. Technical Report Preprint no.22, University of Utrecht, Department of Mathematics (1976)","key":"7_CR11","DOI":"10.1016\/S1385-7258(76)80001-7"},{"issue":"4","key":"7_CR12","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1093\/jigpal\/jzx018","volume":"25","author":"A Bucciarelli","year":"2017","unstructured":"Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL 25(4), 431\u2013464 (2017)","journal-title":"Log. J. IGPL"},{"doi-asserted-by":"crossref","unstructured":"Bucciarelli, A., Lorenzis, S.D., Piperno, A., Salvo, I.: Some computational properties of intersection types. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, 2\u20135 July 1999, pp. 109\u2013118 (1999)","key":"7_CR13","DOI":"10.1109\/LICS.1999.782598"},{"issue":"4","key":"7_CR14","doi-asserted-by":"publisher","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","volume":"21","author":"M Coppo","year":"1980","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the $$\\lambda $$-calculus. Notre Dame J. Form. Log. 21(4), 685\u2013693 (1980)","journal-title":"Notre Dame J. Form. Log."},{"key":"7_CR15","doi-asserted-by":"publisher","first-page":"584","DOI":"10.1073\/pnas.20.11.584","volume":"20","author":"HB Curry","year":"1934","unstructured":"Curry, H.B.: Functionality in combinatory logic. Proc. Natl. Acad. Sci. U.S.A. 20, 584\u2013590 (1934)","journal-title":"Proc. Natl. Acad. Sci. U.S.A."},{"unstructured":"de Carvalho, D.: S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Ph.D. thesis, Universit\u00e9 Aix-Marseille II (2007)","key":"7_CR16"},{"issue":"5","key":"7_CR17","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1017\/S0956796803004970","volume":"14","author":"M Florido","year":"2004","unstructured":"Florido, M., Damas, L.: Linearization of the lambda-calculus and its relation with intersection type systems. J. Funct. Program. 14(5), 519\u2013546 (2004)","journal-title":"J. Funct. Program."},{"key":"7_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"555","DOI":"10.1007\/3-540-57887-0_115","volume-title":"Theoretical Aspects of Computer Software","author":"P Gardner","year":"1994","unstructured":"Gardner, P.: Discovering needed reductions using type theory. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 555\u2013574. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57887-0_115"},{"doi-asserted-by":"crossref","unstructured":"Ghica, D.R.: Geometry of synthesis: a structured approach to VLSI design. In: Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 363\u2013375. ACM (2007)","key":"7_CR19","DOI":"10.1145\/1190215.1190269"},{"doi-asserted-by":"crossref","unstructured":"Ghica, D.R., Smith, A.: Geometry of synthesis III: resource management through type inference. In: Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 345\u2013356. ACM (2011)","key":"7_CR20","DOI":"10.1145\/1925844.1926425"},{"key":"7_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J Girard","year":"1987","unstructured":"Girard, J.: Linear logic. Theor. Comput. Sci. 50, 1\u2013102 (1987)","journal-title":"Theor. Comput. Sci."},{"key":"7_CR22","first-page":"29","volume":"146","author":"JR Hindley","year":"1969","unstructured":"Hindley, J.R.: The principal type-scheme of an object in combinatory logic. Trans. Am. Math. Soc. 146, 29\u201360 (1969)","journal-title":"Trans. Am. Math. Soc."},{"key":"7_CR23","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511608865","volume-title":"Basic Simple Type Theory","author":"JR Hindley","year":"1997","unstructured":"Hindley, J.R.: Basic Simple Type Theory. Cambridge University Press, Cambridge (1997)"},{"issue":"1","key":"7_CR24","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1017\/S0960129517000111","volume":"29","author":"D Kesner","year":"2019","unstructured":"Kesner, D., Ventura, D.: A resource aware semantics for a focused intuitionistic calculus. Math. Struct. Comput. Sci. 29(1), 93\u2013126 (2019)","journal-title":"Math. Struct. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Kesner, D., Vial, P.: Consuming and persistent types for classical logic. In: Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 619\u2013632. ACM (2020)","key":"7_CR25","DOI":"10.1145\/3373718.3394774"},{"unstructured":"Kesner, D., Vial, P.: Non-idempotent types for classical calculi in natural deduction style. Log. Methods Comput. Sci. 16(1) (2020)","key":"7_CR26"},{"issue":"3","key":"7_CR27","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1093\/logcom\/10.3.411","volume":"10","author":"A Kfoury","year":"2000","unstructured":"Kfoury, A.: A linearization of the lambda-calculus and consequences. J. Log. Comput. 10(3), 411\u2013436 (2000)","journal-title":"J. Log. Comput."},{"key":"7_CR28","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(88)90100-4","volume":"59","author":"Y Lafont","year":"1988","unstructured":"Lafont, Y.: The linear abstract machine. Theor. Comput. Sci. 59, 157\u2013180 (1988)","journal-title":"Theor. Comput. Sci."},{"unstructured":"L\u00e9vy, J.-J.: R\u00e9ductions correctes et optimales dans le lambda-calcul. Ph.D. thesis, \u00c9diteur inconnu (1978)","key":"7_CR29"},{"doi-asserted-by":"crossref","unstructured":"Mackie, I.: The geometry of interaction machine. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1995, pp. 198\u2013208. ACM Press (1995)","key":"7_CR30","DOI":"10.1145\/199448.199483"},{"issue":"6","key":"7_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3158094","volume":"2","author":"D Mazza","year":"2018","unstructured":"Mazza, D., Pellissier, L., Vial, P.: Polyadic approximations, fibrations and intersection types. Proc. ACM Program. Lang. 2(6), 1\u201328 (2018)","journal-title":"Proc. ACM Program. Lang."},{"issue":"2","key":"7_CR32","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1006\/inco.1998.2750","volume":"149","author":"F van Raamsdonk","year":"1999","unstructured":"van Raamsdonk, F., Severi, P., S\u00f8rensen, M.H., Xi, H.: Perpetual reductions in lambda-calculus. Inf. Comput. 149(2), 173\u2013225 (1999)","journal-title":"Inf. Comput."},{"doi-asserted-by":"crossref","unstructured":"Walker, D.: Substructural type systems. In: Advanced Topics in Types and Programming Languages, chapter 1, pp. 3\u201343. MIT Press, Cambridge (2005)","key":"7_CR33","DOI":"10.7551\/mitpress\/1104.003.0003"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2022"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17715-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,5]],"date-time":"2024-10-05T02:59:26Z","timestamp":1728097166000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17715-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031177149","9783031177156"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17715-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"3 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/viam.science.tsu.ge\/clas2022\/ictac\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}