{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,6]],"date-time":"2026-10-06T14:24:49Z","timestamp":1791296689746,"version":"4.1.0"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2007,10,24]],"date-time":"2007-10-24T00:00:00Z","timestamp":1193184000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Higher-Order Symb Comput"],"published-print":{"date-parts":[[2007,11,20]]},"DOI":"10.1007\/s10990-007-9013-1","type":"journal-article","created":{"date-parts":[[2007,10,23]],"date-time":"2007-10-23T16:15:52Z","timestamp":1193156152000},"page":"257-270","source":"Crossref","is-referenced-by-count":7,"title":["Explaining the lazy Krivine machine using explicit substitution and addresses"],"prefix":"10.1007","volume":"20","author":[{"given":"Fr\u00e9d\u00e9ric","family":"Lang","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,10,24]]},"reference":[{"issue":"4","key":"9013_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitutions. J. Funct. Program. 1(4), 375\u2013416 (1991)","journal-title":"J. Funct. Program."},{"key":"9013_CR2","unstructured":"Abramsky, S.: The lazy lambda calculus. In: Research Topics in Functional Programming, pp. 65\u2013116 (1990)"},{"key":"9013_CR3","doi-asserted-by":"crossref","unstructured":"Ager, M., Biernacki, D., Danvy, O., Midtgaard, J.: From interpreter to compiler and virtual machine: a functional derivation. Technical Report RS-03-14, Basic Research in Computer Science (BRICS), Denmark (2003)","DOI":"10.7146\/brics.v10i14.21784"},{"key":"9013_CR4","doi-asserted-by":"crossref","unstructured":"Ager, M., Biernacki, D., Danvy, O., Midtgaard, J.: A functional correspondence between evaluators and abstract machines. Technical Report RS-03-13, Basic Research in Computer Science (BRICS), Denmark (2003)","DOI":"10.7146\/brics.v10i13.21783"},{"issue":"3","key":"9013_CR5","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1017\/S0956796897002724","volume":"7","author":"Z.M. 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":"9013_CR6","doi-asserted-by":"crossref","unstructured":"Benaissa, Z.E.-A., Lescanne, P., Rose, K.H.: Modeling sharing and recursion for weak reduction strategies using explicit substitution. In: Proceedings of the Symposium on Programming Languages: Implementation, Logics and Programs PLILP\u201996 (1996)","DOI":"10.1007\/3-540-61756-6_99"},{"key":"9013_CR7","unstructured":"Cr\u00e9gut, P.: Machines \u00e0 environnement pour la r\u00e9duction symbolique et l\u2019\u00e9valuation partielle. Ph.D. Thesis, Universit\u00e9 de Paris 7 (1991)"},{"key":"9013_CR8","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1016\/0304-3975(91)90230-Y","volume":"82","author":"P.-L. Curien","year":"1991","unstructured":"Curien, P.-L.: An abstract framework for environment machines. Theor. Comput. Sci. 82, 389\u2013402 (1991)","journal-title":"Theor. Comput. Sci."},{"key":"9013_CR9","doi-asserted-by":"crossref","unstructured":"Curien, P.-L., Hardin, T., L\u00e9vy, J.-J.: Weak and strong confluent calculi of explicit substitutions. J. ACM 43(2) (1996)","DOI":"10.1145\/226643.226675"},{"issue":"5","key":"9013_CR10","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"N.G. Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Proc. Koninkl. Nederl. Akad. Wet. 75(5), 381\u2013392 (1972)","journal-title":"Proc. Koninkl. Nederl. Akad. Wet."},{"key":"9013_CR11","doi-asserted-by":"crossref","unstructured":"Fairbairn, J., Wray, S.C.: TIM: a simple, lazy abstract machine to execute supercombinators. In: Kahn, G. (ed.) Functional Programming and Computer Architecture, Portland, Oregon, pp. 34\u201345 (1987)","DOI":"10.1007\/3-540-18317-5_3"},{"key":"9013_CR12","doi-asserted-by":"crossref","unstructured":"Gustavsson, J.: A type based sharing analysis for update avoidance and optimisation. Thesis for the Licentiate Degree, Chalmers, G\u00f6teborg University (1999)","DOI":"10.1145\/291251.289427"},{"key":"9013_CR13","doi-asserted-by":"crossref","unstructured":"Hardin, T., Maranget, L., Pagano, B.: Functional back-ends within the lambda-sigma calculus. In: Proceeding of the International Conference on Functional Programming ICFP\u201996 (1996)","DOI":"10.1145\/232627.232632"},{"key":"9013_CR14","volume-title":"Functional Programming\u2014Application and Implementation","author":"P. Henderson","year":"1980","unstructured":"Henderson, P.: Functional Programming\u2014Application and Implementation. Prentice-Hall, Englewood Cliffs (1980)"},{"issue":"6","key":"9013_CR15","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1145\/502949.502880","volume":"19","author":"T. Johnsson","year":"1984","unstructured":"Johnsson, T.: Efficient compilation of lazy evaluation. SIGPLAN Not. 19(6), 58\u201369 (1984)","journal-title":"SIGPLAN Not."},{"key":"9013_CR16","unstructured":"Lang, F.: Mod\u00e8les de la ` b-r\u00e9duction pour les implantations. Ph.D. Thesis, \u00c9cole Normale Sup\u00e9rieure de Lyon (1998)"},{"key":"9013_CR17","unstructured":"Lang, F., Dougherty, D.J., Lescanne, P., Rose, K.H.: Addressed term rewriting systems. Technical Report, Laboratoire de l\u2019Informatique du Parall\u00e9lisme, \u00c9cole Normale Sup\u00e9rieure de Lyon (1999)"},{"key":"9013_CR18","doi-asserted-by":"crossref","unstructured":"Lang, F., Lescanne, P., Liquori, L.: A framework for defining object-calculi. In: Proceedings of Formal Methods Europe FME\u201999 (1999)","DOI":"10.1007\/3-540-48118-4_2"},{"key":"9013_CR19","doi-asserted-by":"crossref","unstructured":"Launchbury, J.: A natural semantics for lazy evaluation. In: Principles of Programming Languages (1993)","DOI":"10.1145\/158511.158618"},{"key":"9013_CR20","doi-asserted-by":"crossref","unstructured":"Mountjoy, J.: The spineless tagless G-machine, naturally. In: Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming ICFP\u201999, Baltimore, Maryland, United States, pp.\u00a0163\u2013173. ACM Press (1998)","DOI":"10.1145\/289423.289439"},{"issue":"2","key":"9013_CR21","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1017\/S0956796800000319","volume":"2","author":"S.L. Peyton Jones","year":"1992","unstructured":"Peyton Jones, S.L.: Implementing lazy functional programming languages on stock hardware: the spineless tagless G-machine. J. Funct. Program. 2(2), 127\u2013202 (1992)","journal-title":"J. Funct. Program."},{"key":"9013_CR22","volume-title":"Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems CTRS\u201992","author":"K.H. Rose","year":"1992","unstructured":"Rose, K.H.: Explicit cyclic substitutions. In: Rusinowitch, M., R\u00e9my, J.-L. (eds.) Proceedings of the 3rd International Workshop on Conditional Term Rewriting Systems CTRS\u201992. Springer, New York (1992)"},{"key":"9013_CR23","unstructured":"Rose, K.H.: Operational reduction models for functional programming languages. Ph.D. Thesis, DIKU, Dept. of Computer Science, Univ. of Copenhagen, Universitetsparken 1, DK-2100 K\u00f8benhavn \u00d8. DIKU report 96\/1 (1996)"},{"key":"9013_CR24","unstructured":"Sestoft, P.: Analysis and efficient implementation of functional programs. Ph.D. Thesis, DIKU, University of Copenhagen, Denmark (1991)"},{"key":"9013_CR25","doi-asserted-by":"crossref","unstructured":"Sestoft, P.: Deriving a lazy abstract machine. J. Funct. Program. 7(3) (1997)","DOI":"10.1017\/S0956796897002712"},{"key":"9013_CR26","unstructured":"Wadsworth, C.: Semantics and pragmatics of the lambda calculus. Ph.D. Thesis, Oxford (1971)"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9013-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-007-9013-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9013-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T01:29:41Z","timestamp":1559352581000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10990-007-9013-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,24]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,11,20]]}},"alternative-id":["9013"],"URL":"https:\/\/doi.org\/10.1007\/s10990-007-9013-1","relation":{},"ISSN":["1388-3690","1573-0557"],"issn-type":[{"value":"1388-3690","type":"print"},{"value":"1573-0557","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,10,24]]}}}