{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T12:57:07Z","timestamp":1743080227046,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030992521"},{"type":"electronic","value":"9783030992538"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We introduce a call-by-name lambda-calculus<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda J$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>J<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>with generalized applications which integrates a notion of distant reduction that allows to unblock<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\beta $$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mi>\u03b2<\/mml:mi><\/mml:math><\/jats:alternatives><\/jats:inline-formula>-redexes without resorting to the permutative conversions of generalized applications. We show strong normalization of simply typed terms, and we then fully characterize strong normalization by means of a quantitative typing system. This characterization uses a non-trivial inductive definition of strong normalization \u2013that we relate to others in the literature\u2013, which is based on a weak-head normalizing strategy. Our calculus relates to explicit substitution calculi by means of a translation between the two formalisms which is faithful, in the sense that it preserves strong normalization. We show that our calculus<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda J$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>J<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>and the well-know calculus<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varLambda J$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u039b<\/mml:mi><mml:mi>J<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>determine equivalent notions of strong normalization. As a consequence,<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\varLambda J$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u039b<\/mml:mi><mml:mi>J<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>inherits a faithful translation into explicit substitutions, and its strong normalization can be characterized by the quantitative typing system designed for<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\lambda J$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\"><mml:mrow><mml:mi>\u03bb<\/mml:mi><mml:mi>J<\/mml:mi><\/mml:mrow><\/mml:math><\/jats:alternatives><\/jats:inline-formula>, despite the fact that quantitative subject reduction fails for permutative conversions.<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_15","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"285-304","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6348-5653","authenticated-orcid":false,"given":"Jos\u00e9 Esp\u00edrito","family":"Santo","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4254-3129","authenticated-orcid":false,"given":"Delia","family":"Kesner","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1398-7460","authenticated-orcid":false,"given":"Lo\u00efc","family":"Peyrot","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"key":"15_CR1","unstructured":"Accattoli, B.: An abstract factorization theorem for explicit substitutions. In: Tiwari, A. (ed.) 23rd International Conference on Rewriting Techniques and Applications (RTA\u201912) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan. LIPIcs, vol.\u00a015, pp. 6\u201321. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"15_CR2","unstructured":"Accattoli, B., Kesner, D.: The structural $$\\lambda $$-calculus. In: Dawar, A., Veith, H. (eds.) Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06247, pp. 381\u2013395. Springer (2010)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito\u00a0Santo, J., Frade, M.J., Pinto, L.: Structural proof theory as rewriting. In: Pfenning, F. (ed.) Term Rewriting and Applications. pp. 197\u2013211. Lecture Notes in Computer Science, Springer (2006)","DOI":"10.1007\/11805618_15"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito\u00a0Santo, J.: Delayed substitutions. In: Lecture Notes in Computer Science, pp. 169\u2013183. Springer Berlin Heidelberg (2007)","DOI":"10.1007\/978-3-540-73449-9_14"},{"key":"15_CR5","unstructured":"Esp\u00edrito Santo, J.: The call-by-value lambda-calculus with generalized applications. In: CSL. LIPIcs, vol.\u00a0152, pp. 35:1\u201335:12. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"15_CR6","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito Santo, J., Kesner, D., Peyrot, L.: A faithful and quantitative notion of distant reduction for generalized applications. CoRR abs\/2201.04156 (2022)","DOI":"10.1007\/978-3-030-99253-8_15"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito\u00a0Santo, J., Pinto, L.: Permutative conversions in intuitionistic multiary sequent calculi with cuts. In: Hofmann, M. (ed.) Typed Lambda Calculi and Applications. pp. 286\u2013300. Lecture Notes in Computer Science, Springer (2003)","DOI":"10.1007\/3-540-44904-3_20"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"Joachimski, F., Matthes, R.: Standardization and confluence for a lambda calculus with generalized applications. In: Rewriting Techniques and Applications, pp. 141\u2013155. Springer Berlin Heidelberg (2000)","DOI":"10.1007\/10721975_10"},{"key":"15_CR9","unstructured":"Kesner, D., Vial, P.: Non-idempotent types for classical calculi in natural deduction style. Log. Methods Comput. Sci. 16(1) (2020)"},{"key":"15_CR10","unstructured":"Matthes, R.: Characterizing strongly normalizing terms of a calculus with generalized applications via intersection types. In: Rolim, J.D.P., Broder, A.Z., Corradini, A., Gorrieri, R., Heckel, R., Hromkovic, J., Vaccaro, U., Wells, J.B. (eds.) ICALP Workshops 2000, Proceedings of the Satelite Workshops of the 27th International Colloquium on Automata, Languages and Programming, Geneva, Switzerland, July 9-15, 2000. pp. 339\u2013354. Carleton Scientific, Waterloo, Ontario, Canada (2000)"},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"von Plato, J.: Natural deduction with general elimination rules. Arch. Math. Log. 40(7), 541\u2013567 (2001)","DOI":"10.1007\/s001530100091"},{"key":"15_CR12","unstructured":"van Raamsdonk, F.: Confluence and normalisation for higher-order rewriting. Ph.D. thesis, Vrije Universiteit Amsterdam (May 1996)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Regnier, L.: Une \u00e9quivalence sur les lambda-termes. Theor. Comput. Sci. 126(2), 281\u2013292 (1994)","DOI":"10.1016\/0304-3975(94)90012-4"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99253-8_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,30]],"date-time":"2023-01-30T13:51:23Z","timestamp":1675086683000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_15","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":"29 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/fossacs","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"77","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}