{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:44:18Z","timestamp":1782953058856,"version":"3.54.5"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227294","type":"print"},{"value":"9783032227300","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22730-0_13","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T16:25:13Z","timestamp":1776270313000},"page":"262-284","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Lambda Galore"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3341-0941","authenticated-orcid":false,"given":"Mariangiola","family":"Dezani-Ciancaglini","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4754-4163","authenticated-orcid":false,"given":"Besik","family":"Dundua","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8937-1892","authenticated-orcid":false,"given":"Furio","family":"Honsell","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"13_CR1","doi-asserted-by":"publisher","unstructured":"Abramsky, S.: Domain theory in logical form. Annals of Pure and Applied Logic 51(1-2), 1\u201377 (1991). https:\/\/doi.org\/10.1016\/0168-0072(91)90065-T","DOI":"10.1016\/0168-0072(91)90065-T"},{"key":"13_CR2","doi-asserted-by":"publisher","unstructured":"Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Information and Computation 105(2), 159\u2013267 (1993). https:\/\/doi.org\/10.1006\/INCO.1993.1044","DOI":"10.1006\/INCO.1993.1044"},{"key":"13_CR3","doi-asserted-by":"publisher","unstructured":"Alessi, F.: An irregular filter model. Theoretical Computer Science 398(1-3), 129\u2013149 (2008). https:\/\/doi.org\/10.1016\/J.TCS.2008.01.047","DOI":"10.1016\/J.TCS.2008.01.047"},{"key":"13_CR4","doi-asserted-by":"publisher","unstructured":"Alessi, F., Barbanera, F., Dezani-Ciancaglini, M.: Intersection types and lambda models. Theoretical Computer Science 355(2), 108\u2013126 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.01.004","DOI":"10.1016\/j.tcs.2006.01.004"},{"key":"13_CR5","doi-asserted-by":"publisher","unstructured":"Alves, S., Kesner, D., Ramos, M.: Extending the quantitative pattern-matching paradigm. In: Kiselyov, O. (ed.) APLAS. LNCS, vol. 15194, pp. 84\u2013105. Springer (2024). https:\/\/doi.org\/10.1007\/978-981-97-8943-6_5","DOI":"10.1007\/978-981-97-8943-6_5"},{"key":"13_CR6","unstructured":"Azevedo\u00a0de Amorim, A., Gaboardi, M., Hsu, J., Katsumata, S.: Metric semantics for probabilistic relational reasoning. CoRR abs\/1807.05091 (2018), http:\/\/arxiv.org\/abs\/1807.05091"},{"key":"13_CR7","doi-asserted-by":"publisher","unstructured":"Antonelli, M., Dal\u00a0Lago, U., Pistone, P.: Towards logical foundations for probabilistic computation. Annals of Pure and Applied Logic 175(9), 103341 (2024). https:\/\/doi.org\/10.1016\/J.APAL.2023.103341","DOI":"10.1016\/J.APAL.2023.103341"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Barbanera, F., Dezani-Ciancaglini, M., de\u2019 Liguoro, U.: Intersection and union types: syntax and semantics. Information and Computation 119, 202\u2013230 (1995). https:\/\/doi.org\/10.1006\/INCO.1995.1086","DOI":"10.1006\/INCO.1995.1086"},{"key":"13_CR9","unstructured":"Barendregt, H.: The Lambda Calculus - its Syntax and Semantics, Studies in logic and the foundations of mathematics, vol.\u00a0103. North-Holland (1985), https:\/\/api.pageplace.de\/preview\/DT0400.9780080933757_A23543814\/preview-9780080933757_A23543814.pdf"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic 48(4), 931\u2013940 (1983). https:\/\/doi.org\/10.2307\/2273659","DOI":"10.2307\/2273659"},{"key":"13_CR11","doi-asserted-by":"publisher","unstructured":"Barendregt, H., Dekkers, W., Statman, R.: Lambda Calculus with Types. Cambridge University Press (2013). https:\/\/doi.org\/10.1017\/CBO9781139032636","DOI":"10.1017\/CBO9781139032636"},{"key":"13_CR12","unstructured":"Barendregt, H., Manzonetto, G.: A Lambda Calculus Satellite. College Publications (2022), https:\/\/www.collegepublications.co.uk\/logic\/mlf\/?00035"},{"key":"13_CR13","doi-asserted-by":"publisher","unstructured":"Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the lambda-calculus. Logic Journal of the IGPL 25, 433\u2013464 (2017). https:\/\/doi.org\/10.1093\/jigpal\/jzx018","DOI":"10.1093\/jigpal\/jzx018"},{"key":"13_CR14","doi-asserted-by":"publisher","unstructured":"Cerda, R., Manzonetto, G., Saurin, A.: Ohana trees and Taylor expansion for the $$\\lambda $$I-calculus: No variable gets left behind or forgotten! In: Fern\u00e1ndez, M. (ed.) FSCD. LIPIcs, vol.\u00a0337, pp. 12:1\u201312:20. Schloss Dagstuhl (2025). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2025.12","DOI":"10.4230\/LIPICS.FSCD.2025.12"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56 \u2013 68 (1940). https:\/\/doi.org\/10.2307\/2266170","DOI":"10.2307\/2266170"},{"key":"13_CR16","doi-asserted-by":"publisher","unstructured":"Coppo, M., Dezani-Ciancaglini, M.: An extension of the basic functionality theory for the $$\\lambda $$-calculus. Notre Dame Journal of Formal Logic 21(4), 685\u2013693 (1980). https:\/\/doi.org\/10.1305\/ndjfl\/1093883253","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"13_CR17","doi-asserted-by":"publisher","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Honsell, F., Longo, G.: Extended type structures and filter lambda models. In: Lolli, G., Longo, G., Marcja, A. (eds.) Logic Colloquium\u201982, Studies in Logic and the Foundations of Mathematics, vol.\u00a0112, pp. 241\u2013262. Elsevier (1984). https:\/\/doi.org\/10.1016\/S0049-237X(08)71819-6","DOI":"10.1016\/S0049-237X(08)71819-6"},{"key":"13_CR18","doi-asserted-by":"publisher","unstructured":"Coppo, M., Dezani-Ciancaglini, M., Zacchi, M.: Type theories, normal forms and $$D_\\infty $$-lambda-models. Information and Computation 72(2), 85\u2013116 (1987). https:\/\/doi.org\/10.1016\/0890-5401(87)90042-3","DOI":"10.1016\/0890-5401(87)90042-3"},{"key":"13_CR19","doi-asserted-by":"publisher","unstructured":"Coquand, T., Huet, G.P.: The calculus of constructions. Information and Computation 76(2\/3), 95\u2013120 (1988). https:\/\/doi.org\/10.1016\/0890-5401(88)90005-3","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Curry, H.B.: Functionality in combinatory logic. Proceedings of the National Academy of Science of the USA 20, 584\u2013590 (1934). https:\/\/doi.org\/10.1073\/pnas.20.11.584","DOI":"10.1073\/pnas.20.11.584"},{"key":"13_CR21","doi-asserted-by":"publisher","unstructured":"Dezani-Ciancaglini, M., Giannini, P., Honsell, F.: Unsolvable terms in filter models. In: Fern\u00e1ndez, M. (ed.) FSCD. LIPIcs, vol.\u00a0337, pp. 3:1\u20133:24. Schloss Dagstuhl (2025). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2025.3","DOI":"10.4230\/LIPICS.FSCD.2025.3"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Dezani-Ciancaglini, M., Honsell, F., Motohama, Y.: Compositional characterisations of lambda-terms using intersection types. Theoretical Computer Science 340(3), 459\u2013495 (2005). https:\/\/doi.org\/10.1016\/J.TCS.2005.03.011","DOI":"10.1016\/J.TCS.2005.03.011"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Esp\u00edrito\u00a0Santo, J., Kesner, D., Peyrot, L.: A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications. Logical Methods in Computer Science 20(3) (2024). https:\/\/doi.org\/10.46298\/LMCS-20(3:10)2024","DOI":"10.46298\/LMCS-20(3:10)2024"},{"key":"13_CR24","doi-asserted-by":"publisher","unstructured":"Fern\u00e1ndez, M., Nantes-Sobrinho, D., Santaguida, D.: A completion procedure for equational rewriting systems with binders. In: Escobar, S., Titolo, L. (eds.) LOPSTR. LNCS, vol. 16117, pp. 94\u2013112. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-032-04848-6_6","DOI":"10.1007\/978-3-032-04848-6_6"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Gay, S.J., Vasconcelos, V.T.: Session Types. Cambridge University Press (2025). https:\/\/doi.org\/10.1017\/9781009000062","DOI":"10.1017\/9781009000062"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Girard, J.Y.: Une extension de l\u2019interpretation de G\u00f6del a l\u2019analyse, et son application a l\u2019elimination des coupures dans l\u2019analyse et la theorie des types. Studies in Logic and the Foundations of Mathematics 63, 63\u201392 (1971). https:\/\/doi.org\/10.1016\/S0049-237X(08)70843-7","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Hindley, R., Longo, G.: Lambda calculus models and extensionality. Mathematical Logic Quarterly 26(19-21), 289\u2013310 (1980). https:\/\/doi.org\/10.1002\/malq.19800261902","DOI":"10.1002\/malq.19800261902"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Honsell, F., Lenisa, M.: Semantical analysis of perpetual strategies in lambda-calculus. Theoretical Computer Science 212(1-2), 183\u2013209 (1999). https:\/\/doi.org\/10.1016\/S0304-3975(98)00140-6","DOI":"10.1016\/S0304-3975(98)00140-6"},{"key":"13_CR29","doi-asserted-by":"publisher","unstructured":"Honsell, F., Ronchi Della\u00a0Rocca, S.: An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences 45(1), 49\u201375 (1992). https:\/\/doi.org\/10.1016\/0022-0000(92)90040-P","DOI":"10.1016\/0022-0000(92)90040-P"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Margaria, I., Zacchi, M.: Filter models with polymorphic types. Theoretical Computer Science 95(1), 143\u2013148 (1992). https:\/\/doi.org\/10.1016\/0304-3975(92)90070-V","DOI":"10.1016\/0304-3975(92)90070-V"},{"key":"13_CR31","doi-asserted-by":"publisher","unstructured":"Kerinec, A., Manzonetto, G., Ronchi Della\u00a0Rocca, S.: Call-by-value, again! In: Kobayashi, N. (ed.) FSCD. LIPIcs, vol.\u00a0195, pp. 7:1\u20137:18. Schloss Dagstuhl (2021). https:\/\/doi.org\/10.4230\/LIPICS.FSCD.2021.7","DOI":"10.4230\/LIPICS.FSCD.2021.7"},{"key":"13_CR32","unstructured":"Krivine, J.L.: Lambda-calculus, types and models. Ellis Horwood (1993), https:\/\/www.irif.fr\/~krivine\/articles\/Lambda.pdf, translated from the 1990 French original by Ren\u00e9 Cori"},{"key":"13_CR33","doi-asserted-by":"publisher","unstructured":"Landin, P.J.: A correspondence between ALGOL 60 and Church\u2019s lambda notation: Part II. Communications of the ACM 8, 89\u2013101,158\u2013165 (1965). https:\/\/doi.org\/10.1145\/363791.363804","DOI":"10.1145\/363791.363804"},{"key":"13_CR34","doi-asserted-by":"publisher","unstructured":"L\u00e9vy, J.: An algebraic interpretation of the lambda beta-calculus and a labeled lambda-calculus. In: B\u00f6hm, C. (ed.) Lambda-Calculus and Computer Science Theory. LNCS, vol.\u00a037, pp. 147\u2013165. Springer (1975). https:\/\/doi.org\/10.1007\/BFB0029523","DOI":"10.1007\/BFB0029523"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Manzonetto, G., Pagani, M., Ronchi Della\u00a0Rocca, S.: New semantical insights into call-by-value $$\\lambda $$-calculus. Fundamenta Informaticae 170(1-3), 241\u2013265 (2019). https:\/\/doi.org\/10.3233\/FI-2019-1862","DOI":"10.3233\/FI-2019-1862"},{"key":"13_CR36","doi-asserted-by":"publisher","unstructured":"Manzonetto, G., Polonsky, A., Saurin, A., Simonsen, J.G.: The fixed point property and a technique to harness double fixed point combinators. Journal of Logic and Computation 29(5), 831\u2013880 (2019). https:\/\/doi.org\/10.1093\/LOGCOM\/EXZ013","DOI":"10.1093\/LOGCOM\/EXZ013"},{"key":"13_CR37","doi-asserted-by":"publisher","unstructured":"Mendler, N.P.: Inductive types and type constraints in the second-order lambda calculus. Annals of Pure and Applied Logic 51(1-2), 159\u2013172 (1991). https:\/\/doi.org\/10.1016\/0168-0072(91)90069-X","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Milner, R.: A theory of type polymorphism in programming. Journal of Computer and System Sciences 17, 348\u2013375 (1978). https:\/\/doi.org\/10.1016\/0022-0000(78)90014-4","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Mosses, P.D., Plotkin, G.D.: On proving limiting completeness. SIAM Journal of Computing 16(1), 179\u2013194 (1987). https:\/\/doi.org\/10.1137\/0216015","DOI":"10.1137\/0216015"},{"key":"13_CR40","doi-asserted-by":"publisher","unstructured":"Paolini, L., Piccolo, M., Ronchi Della\u00a0Rocca, S.: Essential and relational models. Mathematical Structures in Computer Science 27(5), 626\u2013650 (2017). https:\/\/doi.org\/10.1017\/S0960129515000316","DOI":"10.1017\/S0960129515000316"},{"key":"13_CR41","doi-asserted-by":"publisher","unstructured":"Paolini, L., Pimentel, E., Ronchi Della\u00a0Rocca, S.: Strong normalization from an unusual point of view. Theoretical Computer Science 412(20), 1903\u20131915 (2011). https:\/\/doi.org\/10.1016\/J.TCS.2010.12.018","DOI":"10.1016\/J.TCS.2010.12.018"},{"key":"13_CR42","unstructured":"Park, D.: The Y-combinator in Scott\u2019s lambda-calculus models (1976), http:\/\/wrap.warwick.ac.uk\/46310\/, Theory of Computation Report, University of Warwick. Department of Computer Science"},{"key":"13_CR43","doi-asserted-by":"publisher","unstructured":"Plotkin, G.D.: Call-by-name, call-by-value and the $$\\lambda $$-calculus. Theoretical Computer Science 1(2), 125\u2013159 (1975). https:\/\/doi.org\/10.1016\/0304-3975(75)90017-1","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"13_CR44","unstructured":"Rocq (2025), https:\/\/github.com\/rocq-prover\/rocq\/releases\/tag\/V9.0.0"},{"key":"13_CR45","doi-asserted-by":"publisher","unstructured":"Scott, D.S.: Continuous lattices. In: Lawvere, F.W. (ed.) Toposes, Algebraic Geometry and Logic. LNM, vol.\u00a0274, pp. 97\u2013136. Springer (1972). https:\/\/doi.org\/10.1007\/BFb0073967","DOI":"10.1007\/BFb0073967"},{"key":"13_CR46","doi-asserted-by":"publisher","unstructured":"Scott, D.S.: Domains for denotational semantics. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP. LNCS, vol.\u00a0140, pp. 577\u2013613. Springer (1982). https:\/\/doi.org\/10.1007\/BFB0012801","DOI":"10.1007\/BFB0012801"},{"key":"13_CR47","doi-asserted-by":"publisher","unstructured":"Scott, D.S.: Lectures on a mathematical theory of computation. In: Broy, M., Schmidt, G. (eds.) Theoretical Foundations of Programming Methodology, NATO Advanced Study Institutes, vol.\u00a091, pp. 145\u2013292. Springer (1982). https:\/\/doi.org\/10.1007\/978-94-009-7893-5_9","DOI":"10.1007\/978-94-009-7893-5_9"},{"key":"13_CR48","unstructured":"Scott, D.S., Strachey, C.: Toward a mathematical semantics for computer languages. Tech. Rep. PRG06, OUCL (1971), https:\/\/www.cs.cmu.edu\/~crary\/819-f09\/Scott71.pdf"},{"key":"13_CR49","doi-asserted-by":"publisher","unstructured":"Tait, W.W.: Intensional interpretations of functionals of finite type I. The Journal of Symbolic Logic 32, 198\u2013212 (1967). https:\/\/doi.org\/10.2307\/2271658","DOI":"10.2307\/2271658"},{"key":"13_CR50","doi-asserted-by":"publisher","unstructured":"Wegner, P.: The Vienna definition language. ACM Comput.ing Surveys 4(1), 5\u201363 (1972). https:\/\/doi.org\/10.1145\/356596.356598","DOI":"10.1145\/356596.356598"}],"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-032-22730-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T23:51:31Z","timestamp":1782949891000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22730-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227294","9783032227300"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22730-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","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":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2026\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}