{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:08:50Z","timestamp":1770278930022,"version":"3.49.0"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030341749","type":"print"},{"value":"9783030341756","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-34175-6_9","type":"book-chapter","created":{"date-parts":[[2019,11,17]],"date-time":"2019-11-17T19:01:29Z","timestamp":1574017289000},"page":"159-180","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Factorization and Normalization, Essentially"],"prefix":"10.1007","author":[{"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[]},{"given":"Claudia","family":"Faggian","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0469-4279","authenticated-orcid":false,"given":"Giulio","family":"Guerrieri","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,18]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: 23rd International Conference on Rewriting Techniques and Applications, RTA 2012. LIPIcs, vol. 15, pp. 6\u201321 (2012). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.RTA.2012.6","DOI":"10.4230\/LIPIcs.RTA.2012.6"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Accattoli, B., Dal Lago, U.: (Leftmost-Outermost) Beta-reduction is invariant, indeed. Logical Methods Comput. Sci. 12(1) (2016). \nhttps:\/\/doi.org\/10.2168\/LMCS-12(1:4)2016","DOI":"10.2168\/LMCS-12(1:4)2016"},{"key":"9_CR3","unstructured":"Accattoli, B., Faggian, C., Guerrieri, G.: Factorization and normalization, essentially (extended version). CoRR abs\/1902.05945 (2019). \nhttp:\/\/arxiv.org\/abs\/1908.11289"},{"key":"9_CR4","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"The Lambda Calculus - Its Syntax and Semantics","author":"HP Barendregt","year":"1984","unstructured":"Barendregt, H.P.: The Lambda Calculus - Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, vol. 103. North-Holland, Amsterdam (1984)"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1016\/j.tcs.2017.01.025","volume":"672","author":"E Bonelli","year":"2017","unstructured":"Bonelli, E., Kesner, D., Lombardi, C., R\u00edos, A.: On abstract normalisation beyond neededness. Theor. Comput. Sci. 672, 36\u201363 (2017). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2017.01.025","journal-title":"Theor. Comput. Sci."},{"issue":"20","key":"9_CR6","doi-asserted-by":"publisher","first-page":"1884","DOI":"10.1016\/j.tcs.2010.12.017","volume":"412","author":"D Carvalho de","year":"2011","unstructured":"de Carvalho, D., Pagani, M., de Falco, L.T.: A semantic measure of the execution time in linear logic. Theor. Comput. Sci. 412(20), 1884\u20131902 (2011). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2010.12.017","journal-title":"Theor. Comput. Sci."},{"key":"9_CR7","unstructured":"Crary, K.: A simple proof of call-by-value standardization. Technical report, CMU-CS-09-137, Carnegie Mellon University (2009)"},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Guerrieri, G.: Head reduction and normalization in a call-by-value lambda-calculus. In: 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation, WPTE 2015. OASICS, vol. 46, pp. 3\u201317 (2015). \nhttps:\/\/doi.org\/10.4230\/OASIcs.WPTE.2015.3","DOI":"10.4230\/OASIcs.WPTE.2015.3"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Guerrieri, G., Paolini, L., Ronchi Della Rocca, S.: Standardization of a Call-By-Value Lambda-Calculus. In: 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015. LIPIcs, vol. 38, pp. 211\u2013225 (2015). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.TLCA.2015.211","DOI":"10.4230\/LIPIcs.TLCA.2015.211"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Guerrieri, G., Paolini, L., Ronchi Della Rocca, S.: Standardization and conservativity of a refined call-by-value lambda-calculus. Logical Methods Comput. Sci. 13(4) (2017). \nhttps:\/\/doi.org\/10.23638\/LMCS-13(4:29)2017","DOI":"10.23638\/LMCS-13(4:29)2017"},{"key":"9_CR11","unstructured":"Hindley, J.: The Church-Rosser property and a result in combinatory logic. Ph.D. thesis, University of Newcastle-upon-Tyne (1964)"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Hirokawa, N., Middeldorp, A., Moser, G.: Leftmost outermost revisited. In: 26th International Conference on Rewriting Techniques and Applications, RTA 2015. LIPIcs, vol. 36, pp. 209\u2013222 (2015). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.RTA.2015.209","DOI":"10.4230\/LIPIcs.RTA.2015.209"},{"key":"9_CR13","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1016\/j.tcs.2018.06.003","volume":"747","author":"K Ishii","year":"2018","unstructured":"Ishii, K.: A proof of the leftmost reduction theorem for $$\\lambda $$$$\\beta $$$$\\eta $$-calculus. Theor. Comput. Sci. 747, 26\u201332 (2018). \nhttps:\/\/doi.org\/10.1016\/j.tcs.2018.06.003","journal-title":"Theor. Comput. Sci."},{"key":"9_CR14","doi-asserted-by":"publisher","first-page":"58","DOI":"10.4204\/EPTCS.49.5","volume":"49","author":"Delia Kesner","year":"2011","unstructured":"Kesner, D., Lombardi, C., R\u00edos, A.: A standardisation proof for algebraic pattern calculi. In: 5th International Workshop on Higher-Order Rewriting, HOR 2010. EPTCS, vol. 49, pp. 58\u201372 (2010). \nhttps:\/\/doi.org\/10.4204\/EPTCS.49.5","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9_CR15","unstructured":"Klop, J.W.: Combinatory reduction systems. Ph.D. thesis, Utrecht University (1980)"},{"key":"9_CR16","series-title":"Ellis Horwood Series in Computers and Their Applications","volume-title":"Lambda-Calculus","author":"J Krivine","year":"1993","unstructured":"Krivine, J.: Lambda-Calculus. Ellis Horwood Series in Computers and Their Applications. Masson, Types and Models. Ellis Horwood (1993)"},{"issue":"3\u20134","key":"9_CR17","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/BFb0026981","volume":"23","author":"J McKinna","year":"1999","unstructured":"McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. J. Autom. Reasoning 23(3\u20134), 373\u2013409 (1999). \nhttps:\/\/doi.org\/10.1007\/BFb0026981","journal-title":"J. Autom. Reasoning"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/BFb0026981","volume-title":"Category Theory and Computer Science","author":"P-A Melli\u00e8s","year":"1997","unstructured":"Melli\u00e8s, P.-A.: A factorisation theorem in rewriting theory. In: Moggi, E., Rosolini, G. (eds.) CTCS 1997. LNCS, vol. 1290, pp. 49\u201368. Springer, Heidelberg (1997). \nhttps:\/\/doi.org\/10.1007\/BFb0026981"},{"issue":"1\u20132","key":"9_CR19","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1002\/malq.19790250104","volume":"25","author":"G Mitschke","year":"1979","unstructured":"Mitschke, G.: The standardization theorem for $$\\lambda $$-calculus. Math. Logic Q. 25(1\u20132), 29\u201331 (1979). \nhttps:\/\/doi.org\/10.1002\/malq.19790250104","journal-title":"Math. Logic Q."},{"issue":"2","key":"9_CR20","doi-asserted-by":"publisher","first-page":"223","DOI":"10.2307\/1968867","volume":"43","author":"M Newman","year":"1942","unstructured":"Newman, M.: On theories with a combinatorial definition of \u201cEquivalence\u201d. Ann. Math. 43(2), 223\u2013243 (1942)","journal-title":"Ann. Math."},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-540-73449-9_24","volume-title":"Term Rewriting and Applications","author":"V Oostrom","year":"2007","unstructured":"Oostrom, V.: Random descent. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 314\u2013328. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-3-540-73449-9_24"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"van Oostrom, V., Toyama, Y.: Normalisation by random descent. In: 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016. LIPIcs, vol. 52, pp. 32:1\u201332:18 (2016). \nhttps:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2016.32","DOI":"10.4230\/LIPIcs.FSCD.2016.32"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-642-10672-9_17","volume-title":"Programming Languages and Systems","author":"M Pagani","year":"2009","unstructured":"Pagani, M., Tranquilli, P.: Parallel reduction in resource lambda-calculus. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol. 5904, pp. 226\u2013242. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-10672-9_17"},{"issue":"6","key":"9_CR24","doi-asserted-by":"publisher","first-page":"939","DOI":"10.1017\/S0960129515000456","volume":"27","author":"M Pagani","year":"2017","unstructured":"Pagani, M., Tranquilli, P.: The conservation theorem for differential nets. Math. Struct. Comput. Sci. 27(6), 939\u2013992 (2017). \nhttps:\/\/doi.org\/10.1017\/S0960129515000456","journal-title":"Math. Struct. Comput. Sci."},{"issue":"1","key":"9_CR25","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/j.ic.2003.08.003","volume":"189","author":"L Paolini","year":"2004","unstructured":"Paolini, L., Ronchi Della Rocca, S.: Parametric parameter passing lambda-calculus. Inf. Comput. 189(1), 87\u2013106 (2004). \nhttps:\/\/doi.org\/10.1016\/j.ic.2003.08.003","journal-title":"Inf. Comput."},{"issue":"2","key":"9_CR26","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0304-3975(75)90017-1","volume":"1","author":"G.D. Plotkin","year":"1975","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. 1(2), 125\u2013159 (1975). \nhttps:\/\/doi.org\/10.1016\/0304-3975(75)90017-1","journal-title":"Theoretical Computer Science"},{"key":"9_CR27","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-10394-4","volume-title":"The Parametric Lambda Calculus - A Metamodel for Computation","author":"S Ronchi Della Rocca","year":"2004","unstructured":"Ronchi Della Rocca, S., Paolini, L.: The Parametric Lambda Calculus - A Metamodel for Computation. TTCS. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-662-10394-4"},{"issue":"1","key":"9_CR28","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1006\/inco.1995.1057","volume":"118","author":"M Takahashi","year":"1995","unstructured":"Takahashi, M.: Parallel reductions in $$\\lambda $$-calculus. Inf. Comput. 118(1), 120\u2013127 (1995). \nhttps:\/\/doi.org\/10.1006\/inco.1995.1057","journal-title":"Inf. Comput."},{"key":"9_CR29","unstructured":"Terese: Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press, Cambridge (2003)"},{"issue":"3\u20134","key":"9_CR30","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/s00153-007-0042-6","volume":"46","author":"K Terui","year":"2007","unstructured":"Terui, K.: Light affine lambda calculus and polynomial time strong normalization. Arch. Math. Log. 46(3\u20134), 253\u2013280 (2007). \nhttps:\/\/doi.org\/10.1007\/s00153-007-0042-6","journal-title":"Arch. Math. Log."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-34175-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,17]],"date-time":"2019-11-17T19:04:24Z","timestamp":1574017464000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-34175-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030341749","9783030341756"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-34175-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"18 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Nusa Dua, Bali","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Indonesia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 December 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 December 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2019","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}