{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:00Z","timestamp":1749125400650,"version":"3.41.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,7,1]],"date-time":"1999-07-01T00:00:00Z","timestamp":930787200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1999,7]]},"DOI":"10.1023\/a:1006151910336","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T00:53:09Z","timestamp":1040518389000},"page":"43-62","source":"Crossref","is-referenced-by-count":4,"title":["The Tail-Recursive SECD Machine"],"prefix":"10.1007","volume":"23","author":[{"given":"John D.","family":"Ramsdell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"198662_CR1","volume-title":"The Lambda Calculus, Its Syntax and Semantics","author":"H. P. Barendregt","year":"1984","unstructured":"Barendregt, H. P.: The Lambda Calculus, Its Syntax and Semantics, North-Holland, Amsterdam, 1984, revised edition.","edition":"revised edition"},{"key":"198662_CR2","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic Handbook, Academic Press, 1988."},{"key":"198662_CR3","doi-asserted-by":"crossref","unstructured":"Clinger, W. D.: The scheme 311 compiler: An exercise in denotational semantics, in ACM Symposium on Lisp and Functional Programming, New York, 1984, pp. 356\u2013364.","DOI":"10.1145\/800055.802052"},{"issue":"5","key":"198662_CR4","doi-asserted-by":"crossref","first-page":"174","DOI":"10.1145\/277652.277719","volume":"33","author":"W. D. Clinger","year":"1998","unstructured":"Clinger, W. D.: Proper tail recursion and space efficiency, ACM SIGPLAN Notices\n33(5) (1998), pp. 174\u2013185. Proc. SIGPLAN '98 Conference on Programming Language Design and Implementation.","journal-title":"ACM SIGPLAN Notices"},{"issue":"4","key":"198662_CR5","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1017\/S0960129500001535","volume":"2","author":"O. Danvy","year":"1992","unstructured":"Danvy, O. and Filinski, A.: Representing control, a study of the CPS transformation, Math. Struct. Comput. Sci.\n2(4) (1992), pp. 361\u2013391.","journal-title":"Math. Struct. Comput. Sci."},{"key":"198662_CR6","first-page":"193","volume-title":"Formal Description of Programming Concepts III","author":"M. Felleisen","year":"1987","unstructured":"Felleisen, M. and Friedman, D.: Control operators, the SECD-machine, and the lambda calculus, in M. Wirsing (ed.), Formal Description of Programming Concepts III, Elsevier, Amsterdam, 1987, pp. 193\u2013217."},{"issue":"6","key":"198662_CR7","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1145\/173262.155113","volume":"28","author":"C. Flanagan","year":"1993","unstructured":"Flanagan, C., Sabry, A., Duba, B. F. and Felleisen, M.: The essence of compiling with continuations, ACM SIGPLAN Notices\n28(6) (1993), pp. 237\u2013247. Proc. SIGPLAN '93 Conference on Programming Language Design and Implementation.","journal-title":"ACM SIGPLAN Notices"},{"key":"198662_CR8","volume-title":"The SECD Machine: A Verification Case Study","author":"B. T. Graham","year":"1992","unstructured":"Graham, B. T.: The SECD Machine: A Verification Case Study, SECS178, Kluwer Academic Publishers, Dordrecht, 1992."},{"key":"198662_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-2339-0","volume-title":"VLISP: A Verified Implementation of Scheme","author":"J. D. Guttman","year":"1995","unstructured":"Guttman, J. D. and Wand, M. (eds.): VLISP: A Verified Implementation of Scheme, Kluwer Academic Publishers, Dordrecht, 1995. Contents identical to Lisp and Symbolic Computation, Vol. 8, Nos. 1 & 2, special double issue devoted to the results of VLISP."},{"key":"198662_CR10","doi-asserted-by":"crossref","unstructured":"Hannan, J.: Making abstract machines less abstract, in J. Hughes (ed.), Lecture Notes in Comput. Sci. 524, 1991, pp. 618\u2013635. Proc. of the 5th ACM Conference on Function Programming Languages and Computer Architecture.","DOI":"10.1007\/3540543961_29"},{"key":"198662_CR11","volume-title":"IEEE Standard for the Scheme Programming Language","author":"IEEE Std 1178-1990","year":"1991","unstructured":"IEEE Std 1178-1990: IEEE Standard for the Scheme Programming Language, Institute of Electrical and Electronic Engineers, New York, 1991."},{"key":"198662_CR12","unstructured":"Kelsey, R., Clinger, W. and Rees, J. (eds.): Revised5 report on the algorithmic language scheme, Higher-Order and Symbolic Computation\n11(1) (1998), pp. 7\u2013105."},{"key":"198662_CR13","doi-asserted-by":"crossref","unstructured":"Plotkin, G. D.: Call-by-name, Call-by-value and the-calculus, Theoret. Comput. Sci. (1975), 125\u2013159.","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"198662_CR14","unstructured":"Ramsdell, J. D.: SECD Events, NQTHM event file, 1996. ftp:\/\/ftp.cs.utexas.edu\/pub\/boyer\/nqthm\/trsecd\/secd.events."},{"key":"198662_CR15","unstructured":"Ramsdell, J. D.: TR-SECD Events, NQTHM event file, 1996. ftp:\/\/ftp.cs.utexas.edu\/pub\/boyer\/nqthm\/trsecd\/trsecd.events."},{"key":"198662_CR16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511569883","volume-title":"Metamathematics, Machines, and Goedel's Proof","author":"N. Shankar","year":"1994","unstructured":"Shankar, N.: Metamathematics, Machines, and Goedel's Proof, Cambridge Univ. Press, Cambridge, 1994, revised edition.","edition":"revised edition"},{"key":"198662_CR17","doi-asserted-by":"crossref","unstructured":"Wand, M.: Correctness of procedure representations in higher-order assembly language, in S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt (eds.), Lecture Notes in Comput. Sci. 529, 1991, pp. 294\u2013311. Mathematical Foundations of Programming Semantics.","DOI":"10.1007\/3-540-55511-0_15"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006151910336.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1006151910336\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1006151910336.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:45:51Z","timestamp":1749123951000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1006151910336"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999,7]]},"references-count":17,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1999,7]]}},"alternative-id":["198662"],"URL":"https:\/\/doi.org\/10.1023\/a:1006151910336","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1999,7]]}}}