{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:39:08Z","timestamp":1725975548819},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319906850"},{"type":"electronic","value":"9783319906867"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","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":[[2018]]},"DOI":"10.1007\/978-3-319-90686-7_1","type":"book-chapter","created":{"date-parts":[[2018,4,23]],"date-time":"2018-04-23T13:49:55Z","timestamp":1524491395000},"page":"1-16","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name"],"prefix":"10.1007","author":[{"given":"Masayuki","family":"Mizuno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eijiro","family":"Sumii","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,24]]},"reference":[{"key":"1_CR1","first-page":"65","volume-title":"Research Topics in Functional Programming","author":"S Abramsky","year":"1990","unstructured":"Abramsky, S.: The lazy lambda calculus. In: Turner, D.A. (ed.) Research Topics in Functional Programming, pp. 65\u2013116. Addison-Wesley Publishing Co., Boston (1990)"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Jeuring, J., Chakravarty, M.M.T. (eds.) Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, 1\u20133 September 2014, pp. 363\u2013376. ACM (2014)","DOI":"10.1145\/2628136.2628154"},{"key":"1_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BFb0014548","volume-title":"Theoretical Aspects of Computer Software","author":"ZM Ariola","year":"1997","unstructured":"Ariola, Z.M., Blom, S.: Cyclic lambda calculi. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 77\u2013106. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0014548"},{"issue":"3","key":"1_CR4","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1017\/S0956796897002724","volume":"7","author":"ZM Ariola","year":"1997","unstructured":"Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. J. Funct. Program. 7(3), 265\u2013301 (1997)","journal-title":"J. Funct. Program."},{"key":"1_CR5","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, Revised edn. North-Holland, New York (1984)","edition":"Revised"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"e1","DOI":"10.1017\/S0956796817000144","volume":"28","author":"J Breitner","year":"2018","unstructured":"Breitner, J.: The adequacy of Launchbury\u2019s natural semantics for lazy evaluation. J. Funct. Program. 28, e1 (2018)","journal-title":"J. Funct. Program."},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/978-3-642-28869-2_7","volume-title":"Programming Languages and Systems","author":"S Chang","year":"2012","unstructured":"Chang, S., Felleisen, M.: The call-by-need lambda calculus, revisited. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 128\u2013147. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_7"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: Hook, J., Thiemann, P. (eds.) Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, Victoria, BC, Canada, 20\u201328 September 2008, pp. 143\u2013156. ACM (2008)","DOI":"10.1145\/1411204.1411226"},{"key":"1_CR9","unstructured":"Cr\u00e9gut, P.: Omega: a solver of quantifier-free problems in Presburger arithmetic. In: The Coq Proof Assistant Reference Manual, Version 8.7.0 (2017)"},{"issue":"5","key":"1_CR10","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"NG Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagation. Math. (Proc.) 75(5), 381\u2013392 (1972)","journal-title":"Indagation. Math. (Proc.)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/3-540-18317-5_3","volume-title":"Functional Programming Languages and Computer Architecture","author":"J Fairbairn","year":"1987","unstructured":"Fairbairn, J., Wray, S.: Tim: a simple, lazy abstract machine to execute supercombinators. In: Kahn, G. (ed.) FPCA 1987. LNCS, vol. 274, pp. 34\u201345. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/3-540-18317-5_3"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"WD Goldfarb","year":"1981","unstructured":"Goldfarb, W.D.: The undecidability of the second-order unification problem. Theor. Comput. Sci. 13, 225\u2013230 (1981)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/3-540-57826-9_152","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"AD Gordon","year":"1994","unstructured":"Gordon, A.D.: A mechanisation of name-carrying syntax up to alpha-conversion. In: Joyce, J.J., Seger, C.-J.H. (eds.) HUG 1993. LNCS, vol. 780, pp. 413\u2013425. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-57826-9_152"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Johnsson, T.: Efficient compilation of lazy evaluation. In: Deusen, M.S.V., Graham, S.L. (eds.) Proceedings of the 1984 SIGPLAN Symposium on Compiler Construction, Montreal, Canada, 17\u201322 June 1984, pp. 58\u201369. ACM (1984)","DOI":"10.1145\/502874.502880"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-662-49630-5_25","volume-title":"Foundations of Software Science and Computation Structures","author":"D Kesner","year":"2016","unstructured":"Kesner, D.: Reasoning about call-by-need by means of types. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 424\u2013441. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_25"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Launchbury, J.: A natural semantics for lazy evaluation. In: Deusen, M.S.V., Lang, B. (eds.) Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993, pp. 144\u2013154. ACM Press (1993)","DOI":"10.1145\/158511.158618"},{"issue":"3","key":"1_CR17","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1017\/S0956796898003037","volume":"8","author":"J Maraist","year":"1998","unstructured":"Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. J. Funct. Program. 8(3), 275\u2013317 (1998)","journal-title":"J. Funct. Program."},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"McBride, C., McKinna, J.: Functional pearl: I am not a number-I am a free variable. In: Nilsson, H. (ed.) Proceedings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Snowbird, UT, USA, 22\u201322 September 2004, pp. 1\u20139. ACM (2004)","DOI":"10.1145\/1017472.1017477"},{"issue":"3\u20134","key":"1_CR19","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1023\/A:1006294005493","volume":"23","author":"J McKinna","year":"1999","unstructured":"McKinna, J., Pollack, R.: Some lambda calculus and type theory formalized. J. Autom. Reason. 23(3\u20134), 373\u2013409 (1999)","journal-title":"J. Autom. Reason."},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Ong, C.L.: Fully abstract models of the lazy lambda calculus. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24\u201326 October 1988, pp. 368\u2013376. IEEE Computer Society (1988)","DOI":"10.1109\/SFCS.1988.21953"},{"issue":"2","key":"1_CR21","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1017\/S0956796800000319","volume":"2","author":"SL Peyton Jones","year":"1992","unstructured":"Peyton Jones, S.L.: Implementing lazy functional languages on stock hardware: the spineless tagless G-machine. J. Funct. Program. 2(2), 127\u2013202 (1992)","journal-title":"J. Funct. Program."},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Wexelblat, R.L. (ed.) Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, 22\u201324 June 1988, pp. 199\u2013208. ACM (1988)","DOI":"10.1145\/53990.54010"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-319-22102-1_24","volume-title":"Interactive Theorem Proving","author":"S Sch\u00e4fer","year":"2015","unstructured":"Sch\u00e4fer, S., Tebbi, T., Smolka, G.: Autosubst: reasoning with de Bruijn terms and parallel substitutions. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 359\u2013374. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_24"},{"issue":"3","key":"1_CR24","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1017\/S0956796897002712","volume":"7","author":"P Sestoft","year":"1997","unstructured":"Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3), 231\u2013264 (1997)","journal-title":"J. Funct. Program."},{"issue":"4","key":"1_CR25","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/s10817-008-9097-2","volume":"40","author":"C Urban","year":"2008","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. J. Autom. Reason. 40(4), 327\u2013356 (2008)","journal-title":"J. Autom. Reason."},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"Vassena, M., Breitner, J., Russo, A.: Securing concurrent lazy programs against information leakage. In: 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA, 21\u201325 August 2017, pp. 37\u201352 (2017)","DOI":"10.1109\/CSF.2017.39"},{"key":"1_CR27","unstructured":"Wadsworth, C.P.: Semantics and pragmatics of the lambda calculus. Ph.D. thesis, Oxford University (1971)"}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-90686-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,20]],"date-time":"2022-08-20T15:32:10Z","timestamp":1661009530000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-90686-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319906850","9783319906867"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-90686-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}