{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T13:55:30Z","timestamp":1790690130168,"version":"4.1.0"},"reference-count":21,"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-9015-z","type":"journal-article","created":{"date-parts":[[2007,10,23]],"date-time":"2007-10-23T16:17:04Z","timestamp":1193156224000},"page":"209-230","source":"Crossref","is-referenced-by-count":29,"title":["Strongly reducing variants of the Krivine abstract machine"],"prefix":"10.1007","volume":"20","author":[{"given":"Pierre","family":"Cr\u00e9gut","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,10,24]]},"reference":[{"key":"9015_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Cardelli, L., Curien, P.-L., L\u00e9vy, J.-J.: Explicit substitution. In: ACM Symposium on Principles of Programming Languages (POPL) (1990)","DOI":"10.1145\/96709.96712"},{"key":"9015_CR2","doi-asserted-by":"crossref","unstructured":"Ager, M., Biernacki, D., Danvy, O., Midtgaard, J.: A functional correspondance between evaluators and abstract machines. In: PPDP\u201903 Proceedings of the 5th ACM Sigplan International Conference on Principle and Practice of Declarative Programming, pp.\u00a08\u201319 (2003)","DOI":"10.1145\/888251.888254"},{"key":"9015_CR3","doi-asserted-by":"crossref","unstructured":"Argo, G.: Improving the three instruction machine. In: The Fourth International Conference on Functional Programming Languages and Computer Architecture, London (1989)","DOI":"10.1145\/99370.99378"},{"issue":"1","key":"9015_CR4","first-page":"3","volume":"22","author":"A. Asperti","year":"1994","unstructured":"Asperti, A.: Linear logic, comonads and optimal reductions. Fund. Inf. 22(1), 3\u201322 (1994)","journal-title":"Fund. Inf."},{"key":"9015_CR5","doi-asserted-by":"crossref","unstructured":"Asperti, A., Mairson, H.: Parallel beta reduction is not elementary recursive. In: ACM Symposium on Principles of Programming Languages, pp. 303\u2013315 (1998)","DOI":"10.1145\/268946.268971"},{"key":"9015_CR6","doi-asserted-by":"crossref","unstructured":"Barendregt, H.: The type free \u03bb-calculus. In: Handbook of Mathematical Logic, pp.\u00a01091\u20131132. North-Holland, Amsterdam (1977), Chap.\u00a0D.7","DOI":"10.1016\/S0049-237X(08)71129-7"},{"key":"9015_CR7","volume-title":"The Lambda Calculus","author":"H. Barendregt","year":"1981","unstructured":"Barendregt, H.: The Lambda Calculus. North-Holland, Amsterdam (1981)"},{"key":"9015_CR8","unstructured":"Barras, B.: Efficient reduction functions in Coq (1998). Unpublished note available at http:\/\/pauillac.inria.fr\/~barras\/reduction"},{"key":"9015_CR9","doi-asserted-by":"crossref","unstructured":"Cr\u00e9gut, P.: An abstract machine for the normalization of \u03bb-terms. In: ACM Lisp and Functional Programming Conference (1990)","DOI":"10.1145\/91556.91681"},{"key":"9015_CR10","unstructured":"Cr\u00e9gut, P.: Machines \u00e0 environnement pour la r\u00e9duction symbolique et l\u2019\u00e9valuation partielle. Ph.D. Thesis, Universit\u00e9 Paris VII (1991)"},{"issue":"2","key":"9015_CR11","first-page":"362","volume":"42","author":"P.-L. Curien","year":"1996","unstructured":"Curien, P.-L., Hardin, T., L\u00e9vy, J.-J.: Confluence properties of weak and strong calculi of explicit substitutions. J.\u00a0ACM 42(2), 362\u2013391 (1996)","journal-title":"J.\u00a0ACM"},{"key":"9015_CR12","doi-asserted-by":"crossref","unstructured":"Fairbairn, J., Wray, S.: TIM: a simple, lazy, abstract machine to execute supercombinators. In: Conference on Functional Programming and Computer Architecture, Portland (1987)","DOI":"10.1007\/3-540-18317-5_3"},{"key":"9015_CR13","doi-asserted-by":"crossref","unstructured":"Glauert, J.R., Kennaway, R., Papadopoulos, G., Sleep, R.: DACTL, an experimental graph rewriting language. In: Ehrig, H., Kreowsky, H., Rozenberg, G. (eds.) Graph Grammars and Their Application to Computer Science, pp. 378\u2013395 (1991)","DOI":"10.1007\/BFb0017401"},{"key":"9015_CR14","doi-asserted-by":"crossref","unstructured":"Gontier, G., Abadi, M., L\u00e9vy, J.-J.: The geometry of optimal reduction. In: ACM Symposium on Principles of Programming Languages, pp. 15\u201326 (1992)","DOI":"10.1145\/143165.143172"},{"key":"9015_CR15","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: International Conference on Functional Programming (ICFP\u201902) (2002)","DOI":"10.1145\/581478.581501"},{"issue":"2","key":"9015_CR16","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1017\/S0956796898002986","volume":"8","author":"T. Hardin","year":"1998","unstructured":"Hardin, T., Maranget, L., Paganot, B.: Functional runtimes within the lambda-sigma calculus. J. Funct. Program. 8(2), 131\u2013176 (1998)","journal-title":"J. Funct. Program."},{"key":"9015_CR17","doi-asserted-by":"crossref","unstructured":"Krivine, J.-L.: A call-by-name lambda-calculus machine. Higher Order Symb. Comput. (2007, this volume)","DOI":"10.1007\/s10990-007-9018-9"},{"key":"9015_CR18","doi-asserted-by":"crossref","unstructured":"Lamping, J.: An algorithm for optimal lambda calculus reduction. In: ACM Symposium on Principles of Programming Languages (POPL) (1990)","DOI":"10.1145\/96709.96711"},{"key":"9015_CR19","unstructured":"Leroy, X.: The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA (1990)"},{"key":"9015_CR20","unstructured":"L\u00e9vy, J.-J.: Optimal reductions in the lambda-calculus. In: Seldin, J., Hindley, J. (eds.) To H.B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pp. 159\u2013191 (1980)"},{"key":"9015_CR21","unstructured":"Sestoft, P.: Analysis and efficient implementation of functional programs. Ph.D. Thesis, University of Copenhagen, DIKU research report 92\/6 (1991)"}],"container-title":["Higher-Order and Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9015-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10990-007-9015-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10990-007-9015-z","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-9015-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,10,24]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,11,20]]}},"alternative-id":["9015"],"URL":"https:\/\/doi.org\/10.1007\/s10990-007-9015-z","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]]}}}