{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T03:03:54Z","timestamp":1790737434285,"version":"4.1.0"},"reference-count":82,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>The semantics of the untyped (call-by-name) lambda-calculus is a well developed field built around the concept of solvable terms, which are elegantly characterized in many different ways. In particular, unsolvable terms provide a consistent notion of meaningless term. The semantics of the untyped call-by-value lambda-calculus (CbV) is instead still in its infancy, because of some inherent difficulties but also because CbV solvable terms are less studied and understood than in call-by-name. On the one hand, we show that a carefully crafted presentation of CbV allows us to recover many of the properties that solvability has in call-by-name, in particular qualitative and quantitative characterizations via multi types. On the other hand, we stress that, in CbV, solvability plays a different role: identifying unsolvable terms as meaningless induces an inconsistent theory.<\/jats:p>","DOI":"10.1145\/3547652","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T19:39:26Z","timestamp":1661974766000},"page":"855-885","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["The theory of call-by-value solvability"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4944-9944","authenticated-orcid":false,"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[{"name":"Inria, France \/ \u00c9cole Polytechnique, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0469-4279","authenticated-orcid":false,"given":"Giulio","family":"Guerrieri","sequence":"additional","affiliation":[{"name":"Huawei Edinburgh Research Centre, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90065-T"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2015.08.006"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354169"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470630"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2012.22"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434332"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470726"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236789"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_12"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_3"},{"key":"e_1_2_1_11_1","volume-title":"The Theory of Call-by-Value Solvability (long version). CoRR, abs\/2207.08697","author":"Accattoli Beniamino","year":"2022","unstructured":"Beniamino Accattoli and Giulio Guerrieri . 2022. The Theory of Call-by-Value Solvability (long version). CoRR, abs\/2207.08697 ( 2022 ), arxiv:2207.08697 Beniamino Accattoli and Giulio Guerrieri. 2022. The Theory of Call-by-Value Solvability (long version). CoRR, abs\/2207.08697 (2022), arxiv:2207.08697"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_15"},{"key":"e_1_2_1_13_1","volume-title":"Semantic Bounds and Strong Call-by-Value Normalization. CoRR, abs\/2104.13979","author":"Accattoli Beniamino","year":"2021","unstructured":"Beniamino Accattoli , Giulio Guerrieri , and Maico Leberle . 2021. Semantic Bounds and Strong Call-by-Value Normalization. CoRR, abs\/2104.13979 ( 2021 ), arxiv:2104.13979 Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. 2021. Semantic Bounds and Strong Call-by-Value Normalization. CoRR, abs\/2104.13979 (2021), arxiv:2104.13979"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29822-6_4"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2015.23"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2017.01.003"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2019.3"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_2_1_19_1","unstructured":"Hendrik Pieter Barendregt. 1971. Some extensional term models for combinatory logics and \u03bb -calculi. Ph. D. Dissertation. Univ. Utrecht. \t\t\t\t  Hendrik Pieter Barendregt. 1971. Some extensional term models for combinatory logics and \u03bb -calculi. Ph. D. Dissertation. Univ. Utrecht."},{"key":"e_1_2_1_20_1","volume-title":"Colloque international de logique : Clermont-Ferrand, 18-25 juillet","author":"Barendregt Hendrik Pieter","year":"1975","unstructured":"Hendrik Pieter Barendregt . 1977. Solvability in lambda-calculi . In Colloque international de logique : Clermont-Ferrand, 18-25 juillet 1975 , M. Guillaume (Ed.). \u00c9ditions du C.N.R.S., Paris . 209\u2013219. Hendrik Pieter Barendregt. 1977. Solvability in lambda-calculi. In Colloque international de logique : Clermont-Ferrand, 18-25 juillet 1975, M. Guillaume (Ed.). \u00c9ditions du C.N.R.S., Paris. 209\u2013219."},{"key":"e_1_2_1_21_1","unstructured":"Hendrik Pieter Barendregt. 1984. The Lambda Calculus \u2013 Its Syntax and Semantics. 103 North-Holland. \t\t\t\t  Hendrik Pieter Barendregt. 1984. The Lambda Calculus \u2013 Its Syntax and Semantics. 103 North-Holland."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:3)2013"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00056-7"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59025-3_2"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-17(1:7)2021"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzx018"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_7"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02011875"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90042-3"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351262"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434313"},{"key":"e_1_2_1_33_1","unstructured":"Daniel de Carvalho. 2007. S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Universit\u00e9 Aix-Marseille II. \t\t\t\t  Daniel de Carvalho. 2007. S\u00e9mantiques de la logique lin\u00e9aire et temps de calcul. Universit\u00e9 Aix-Marseille II."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129516000396"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.017"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.010"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm037"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/161643.161646"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2012.259"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2020.35"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(2:12)2016"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0_115"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1703"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(88)90025-5"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASIcs.WPTE.2015.3"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.293.5"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TLCA.2015.211"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:29)2017"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_12"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19800261902"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(92)90040-P"},{"key":"e_1_2_1_54_1","article-title":"Meaningless Terms in Rewriting","volume":"1999","author":"Kennaway Richard","year":"1999","unstructured":"Richard Kennaway , Vincent van Oostrom , and Fer-Jan de Vries . 1999 . Meaningless Terms in Rewriting . J. Funct. Log. Program. , 1999 , 1 (1999). Richard Kennaway, Vincent van Oostrom, and Fer-Jan de Vries. 1999. Meaningless Terms in Rewriting. J. Funct. Log. Program., 1999, 1 (1999).","journal-title":"J. Funct. Log. Program."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2021.7"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_18"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394774"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2022.27"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/10.3.411"},{"key":"e_1_2_1_60_1","unstructured":"Jean-Louis Krivine. 1993. Lambda-calculus types and models. Masson. isbn:978-0-13-062407-9 \t\t\t\t  Jean-Louis Krivine. 1993. Lambda-calculus types and models. Masson. isbn:978-0-13-062407-9"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.15"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(83)90030-1"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2019-1862"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00358-2"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158094"},{"key":"e_1_2_1_67_1","volume-title":"Computational \u03bb -Calculus and Monads","author":"Moggi Eugenio","unstructured":"Eugenio Moggi . 1988. Computational \u03bb -Calculus and Monads . University of Edinburgh. http :\/\/www.lfcs.inf.ed.ac.uk\/reports\/88\/ECS-LFCS-88-66\/ECS-LFCS-88-66.pdf Eugenio Moggi. 1988. Computational \u03bb -Calculus and Monads. University of Edinburgh. http:\/\/www.lfcs.inf.ed.ac.uk\/reports\/88\/ECS-LFCS-88-66\/ECS-LFCS-88-66.pdf"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016871"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45446-2_5"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:1999130"},{"key":"e_1_2_1_72_1","volume-title":"Advanced Topics in Bisimulation and Coinduction, Davide Sangiorgi and Jan J","author":"Pitts Andrew M.","unstructured":"Andrew M. Pitts . 2012. Howe\u2019s method for higher-order languages . In Advanced Topics in Bisimulation and Coinduction, Davide Sangiorgi and Jan J . M. M. Rutten (Eds.) (Cambridge tracts in theoretical computer science, Vol. 52). Cambridge University Press, 197\u2013 232 . Andrew M. Pitts. 2012. Howe\u2019s method for higher-order languages. In Advanced Topics in Bisimulation and Coinduction, Davide Sangiorgi and Jan J. M. M. Rutten (Eds.) (Cambridge tracts in theoretical computer science, Vol. 52). Cambridge University Press, 197\u2013232."},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90094-A"},{"key":"e_1_2_1_75_1","unstructured":"Garrel Pottinger. 1980. A type assignment for the strongly normalizable \u03bb -terms. In To HB Curry: essays on combinatory logic \u03bb -calculus and formalism. 561\u2013577. \t\t\t\t  Garrel Pottinger. 1980. A type assignment for the strongly normalizable \u03bb -terms. In To HB Curry: essays on combinatory logic \u03bb -calculus and formalism. 561\u2013577."},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129598002722"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-10394-4"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269968"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0032397"},{"key":"e_1_2_1_81_1","volume-title":"Semantics and pragmatics of the lambda-calculus","author":"Wadsworth Christopher P.","unstructured":"Christopher P. Wadsworth . 1971. Semantics and pragmatics of the lambda-calculus . University of Oxford. Christopher P. Wadsworth. 1971. Semantics and pragmatics of the lambda-calculus. University of Oxford."},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1137\/0205036"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547652","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547652","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:43:29Z","timestamp":1750272209000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547652"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":82,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547652"],"URL":"https:\/\/doi.org\/10.1145\/3547652","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}