{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:45Z","timestamp":1760202645774},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642298219"},{"type":"electronic","value":"9783642298226"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-29822-6_4","type":"book-chapter","created":{"date-parts":[[2012,5,20]],"date-time":"2012-05-20T13:21:09Z","timestamp":1337520069000},"page":"4-16","source":"Crossref","is-referenced-by-count":25,"title":["Call-by-Value Solvability, Revisited"],"prefix":"10.1007","author":[{"given":"Beniamino","family":"Accattoli","sequence":"first","affiliation":[]},{"given":"Luca","family":"Paolini","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Accattoli, B.: An abstract factorisation theorem for explicit substitutions (2011) (accepted at RTA 2012), https:\/\/sites.google.com\/site\/beniaminoaccattoli\/factorisation.pdf"},{"key":"4_CR2","unstructured":"Accattoli, B.: Jumping around the box. Ph.D. Thesis, Universit\u00e0 di Roma La Sapienza (2011)"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-642-04027-6_7","volume-title":"Computer Science Logic","author":"B. Accattoli","year":"2009","unstructured":"Accattoli, B., Guerrini, S.: Jumping Boxes. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 55\u201370. Springer, Heidelberg (2009)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-28717-6_5","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"B. Accattoli","year":"2012","unstructured":"Accattoli, B., Kesner, D.: The Permutative \u03bb-Calculus. In: Bj\u00f8rner, N., Voronkov, A. (eds.) LPAR-18 2012. LNCS, vol.\u00a07180, pp. 23\u201336. Springer, Heidelberg (2012)"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-15205-4_30","volume-title":"Computer Science Logic","author":"B. Accattoli","year":"2010","unstructured":"Accattoli, B., Kesner, D.: The Structural \u03bb-Calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol.\u00a06247, pp. 381\u2013395. Springer, Heidelberg (2010)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Paolini, L.: Call-by-value solvability, revisited (ext. version) (2012), https:\/\/sites.google.com\/site\/beniaminoaccattoli\/CBV-solvabilitywithproofs.pdf","DOI":"10.1007\/978-3-642-29822-6_4"},{"key":"4_CR7","unstructured":"Barendregt, H.P.: The Lambda Calculus \u2013 Its Syntax and Semantics, vol.\u00a0103. North-Holland (1984)"},{"issue":"2","key":"4_CR8","first-page":"372","volume":"39","author":"H. Barendregt","year":"1975","unstructured":"Barendregt, H.: Solvability in lambda-calculi. The Journal of Symbolic Logic\u00a039(2), 372 (1975)","journal-title":"The Journal of Symbolic Logic"},{"issue":"6","key":"4_CR9","doi-asserted-by":"publisher","first-page":"1109","DOI":"10.1093\/logcom\/exm037","volume":"17","author":"R. Dyckhoff","year":"2007","unstructured":"Dyckhoff, R., Lengrand, S.: Call-by-value lambda-calculus and ljq. J. Log. Comput.\u00a017(6), 1109\u20131134 (2007)","journal-title":"J. Log. Comput."},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Fern\u00e1ndez, M., Siafakas, N.: Labelled lambda-calculi with explicit copy and erase. In: LINEARITY, pp. 49\u201364 (2009)","DOI":"10.4204\/EPTCS.22.5"},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-02273-9_12","volume-title":"Typed Lambda Calculi and Applications","author":"H. Herbelin","year":"2009","unstructured":"Herbelin, H., Zimmermann, S.: An Operational Account of Call-by-Value Minimal and Classical \u03bb-Calculus in \u201cNatural Deduction\u201d Form. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol.\u00a05608, pp. 142\u2013156. Springer, Heidelberg (2009)"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1017\/S0960129500001195","volume":"5","author":"M. Hofmann","year":"1995","unstructured":"Hofmann, M.: Sound and complete axiomatisations of call-by-value control operators. Mathematical Structures in Computer Science\u00a05, 461\u2013482 (1995)","journal-title":"Mathematical Structures in Computer Science"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/BFb0029520","volume-title":"\u03bb-Calculus and Computer Science Theory","author":"J.M.E. Hyland","year":"1975","unstructured":"Hyland, J.M.E.: A Survey of Some Useful Partial Order Relations on Terms of the Lambda Calculus. In: B\u00f6hm, C. (ed.) \u03bb-Calculus and Computer Science Theory. LNCS, vol.\u00a037, pp. 83\u201395. Springer, Heidelberg (1975)"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Klop, J.W.: On Solvability by \u03bb I - Terms. In: B\u00f6hm, C. (ed.) \u03bb-Calculus and Computer Science Theory. LNCS, vol.\u00a037, pp. 342\u2013345. Springer, Heidelberg (1975)","DOI":"10.1007\/BFb0029536"},{"issue":"2-3","key":"4_CR15","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/363744.363749","volume":"8","author":"P.J. Landin","year":"1965","unstructured":"Landin, P.J.: A correspondence between ALGOL 60 and Church\u2019s lambda-notation: Part I and Part II. Communications of the ACM\u00a08(2-3), 89\u2013101, 158\u2013165 (1965)","journal-title":"Communications of the ACM"},{"key":"4_CR16","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.\u00a01290, pp. 49\u201368. Springer, Heidelberg (1997)"},{"key":"4_CR17","first-page":"14","volume-title":"LICS","author":"E. Moggi","year":"1989","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: LICS, pp. 14\u201323. IEEE Computer Society Press, Piscataway (1989)"},{"issue":"1-4","key":"4_CR18","doi-asserted-by":"crossref","first-page":"173","DOI":"10.3233\/FI-2010-324","volume":"103","author":"M. Pagani","year":"2010","unstructured":"Pagani, M., Rocca, S.R.D.: Linearity, non-determinism and solvability. Fundam. Inform.\u00a0103(1-4), 173\u2013202 (2010)","journal-title":"Fundam. Inform."},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/3-540-45446-2_5","volume-title":"Theoretical Computer Science","author":"L. Paolini","year":"2001","unstructured":"Paolini, L.: Call-by-Value Separability and Computability. In: Restivo, A., Ronchi Della Rocca, S., Roversi, L. (eds.) ICTCS 2001. LNCS, vol.\u00a02202, pp. 74\u201389. Springer, Heidelberg (2001)"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/j.entcs.2005.06.013","volume":"136","author":"L. Paolini","year":"2005","unstructured":"Paolini, L., Pimentel, E., Ronchi Della Rocca, S.: Lazy strong normalization. Electr. Notes Theor. Comput. Sci.\u00a0136, 103\u2013116 (2005)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"6","key":"4_CR21","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1051\/ita:1999130","volume":"33","author":"L. Paolini","year":"1999","unstructured":"Paolini, L., Ronchi Della Rocca, S.: Call-by-value solvability. Theoretical Informatics and Applications\u00a033(6), 507\u2013534 (1999)","journal-title":"Theoretical Informatics and Applications"},{"key":"4_CR22","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 \u03bb-calculus. Theoretical Computer Science\u00a01, 125\u2013159 (1975)","journal-title":"Theoretical Computer Science"},{"key":"4_CR23","series-title":"Texts in Theoretical Computer Science: An EATCS","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-10394-4","volume-title":"The Parametric \u03bb-Calculus: a Metamodel for Computation","author":"S. Ronchi Della Rocca","year":"2004","unstructured":"Ronchi Della Rocca, S., Paolini, L.: The Parametric \u03bb-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS. Springer, Berlin (2004)"},{"key":"4_CR24","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/BF01019462","volume":"6","author":"A. Sabry","year":"1993","unstructured":"Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. LISP and Symbolic Computation\u00a06, 289\u2013360 (1993)","journal-title":"LISP and Symbolic Computation"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-12251-4_11","volume-title":"Functional and Logic Programming","author":"A. Saurin","year":"2010","unstructured":"Saurin, A.: Standardization and B\u00f6hm Trees for \u039b\u03bc-Calculus. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 134\u2013149. Springer, Heidelberg (2010)"},{"issue":"3","key":"4_CR26","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1137\/0205036","volume":"5","author":"C.P. Wadsworth","year":"1976","unstructured":"Wadsworth, C.P.: The relation between computational and denotational properties for Scott\u2019s D \u2009\u221e\u2009-models of the lambda-calculus. SIAM Journal of Computing\u00a05(3), 488\u2013521 (1976)","journal-title":"SIAM Journal of Computing"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-29822-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,7]],"date-time":"2020-07-07T22:01:08Z","timestamp":1594159268000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-29822-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642298219","9783642298226"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-29822-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}