{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:50Z","timestamp":1761611150009},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2004,9,1]],"date-time":"2004-09-01T00:00:00Z","timestamp":1093996800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2004,9]]},"DOI":"10.1007\/s10817-004-6885-1","type":"journal-article","created":{"date-parts":[[2005,2,18]],"date-time":"2005-02-18T18:23:02Z","timestamp":1108750982000},"page":"89-132","source":"Crossref","is-referenced-by-count":11,"title":["Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts"],"prefix":"10.1007","volume":"33","author":[{"given":"Chuck","family":"Liang","sequence":"first","affiliation":[]},{"given":"Gopalan","family":"Nadathur","sequence":"additional","affiliation":[]},{"given":"Xiaochu","family":"Qi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,2,17]]},"reference":[{"issue":"4","key":"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. and L\u00e9vy, J.-J.: Explicit substitutions, J. Funct. Programming 1(4) (1991), 375?416.","journal-title":"J. Funct. Programming"},{"key":"CR2","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1016\/0022-0000(81)90073-8","volume":"23","author":"L. Aiello","year":"1981","unstructured":"Aiello, L. and Prini, G.: An efficient interpreter for the lambda-calculus, J. Comput. System Sci. 23 (1981), 383?425.","journal-title":"J. Comput. System Sci."},{"key":"CR3","unstructured":"Appel, A. and Shao, Z.: Smartest recompilation, in Tenth Annual ACM SIGPLAN?SIGACT Symposium on Principles of Programming Languages, January 1993, Longer version as Princeton University Technical Report CS-TR-395-92."},{"issue":"5","key":"CR4","doi-asserted-by":"crossref","first-page":"699","DOI":"10.1017\/S0956796800001945","volume":"6","author":"Z. Benaissa","year":"1996","unstructured":"Benaissa, Z., Briaud, D., Lescanne, P. and Rouyer-Degli, J.: ??, a calculus of explicit substitutions which preserves strong normalization, J. Funct. Programming 6(5) (1996), 699?722.","journal-title":"J. Funct. Programming"},{"key":"CR5","unstructured":"Brisset, P. and Ridoux, O.: Naive reverse can be linear, in K. Furukawa (ed.), Eighth International Logic Programming Conference, MIT Press, June 1991, pp. 857?870."},{"key":"CR6","unstructured":"Brisset, P. and Ridoux O.: The compilation of ?Prolog and its execution with MALI, Publication Interne 687, IRISA, Rennes, November 1992."},{"issue":"5","key":"CR7","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church?Rosser theorem, Indag. Math. 34(5) (1972), 381?392.","journal-title":"Indag. Math."},{"key":"CR8","unstructured":"de Bruijn, N.: A survey of the project AUTOMATH, in J. P. Seldin and J. R. Hindley (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 579?606."},{"key":"CR9","unstructured":"Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T. and Smith, S. F.: Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986."},{"issue":"2\/3","key":"CR10","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"February\/March 1988","unstructured":"Coquand, T. and Huet, G.: The calculus of constructions, Inform. and Comput. 76(2\/3) (February\/March 1988), 95?120.","journal-title":"Inform. and Comput."},{"key":"CR11","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1017\/S0960129500003224","volume":"11","author":"R. David","year":"2001","unstructured":"David, R. and Guillaume, B.: A ?-calculus with explicit weakening and explicit substitution, Math. Structures Comput. Sci. 11 (2001), 169?206.","journal-title":"Math. Structures Comput. Sci."},{"key":"CR12","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G. Dowek","year":"2000","unstructured":"Dowek, G., Hardin, T. and Kirchner, C.: Higher-order unification via explicit substitutions, Inform. and Comput. 157 (2000), 183?235.","journal-title":"Inform. and Comput."},{"key":"CR13","unstructured":"Fernandez, M., Mackie, I. and Sinot, F.-R.: Closed reduction: Explicit substitutions without alpha-conversion, Math. Structures Comput. Sci. (2004), to appear."},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Field, J.: On laziness and optimality in lambda interpreters: Tools for specification and analysis, in Seventeenth Annual ACM Symposium on Principles of Programming Languages, ACM Press, January 1990, pp. 1?15.","DOI":"10.1145\/96709.96710"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B. and Leroy, X.: A compiled implementation of strong reduction, in Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, Pittsburgh, October 2002, pp. 235?246.","DOI":"10.1145\/581478.581501"},{"key":"CR16","unstructured":"Harper, R.: Introduction to Standard ML, Technical Report ECS-LFCS-86-14, Laboratory for Foundations of Computer Science, University of Edinburgh, November 1986. Revised by Nick Rothwell, January 1989, with exercises by Kevin Mitchell."},{"issue":"1","key":"CR17","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F. and Plotkin, G.: A framework for defining logics, J. ACM 40(1) (1993), 143?184.","journal-title":"J. ACM"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"Huet, G.: A unification algorithm for typed ?-calculus, Theoret. Comput. Sci. 1 (1975), 27?57.","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"CR19","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1017\/S0956796897002785","volume":"7","author":"F. Kamareddine","year":"1997","unstructured":"Kamareddine, F. and R\u00edos, A.: Extending the ?-calculus with explicit substitution which preserves strong normalization into a confluent calculus on open terms, J. Funct. Programming 7(4) (1997), 395?420.","journal-title":"J. Funct. Programming"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"Liang, C.: Let-polymorphism and eager type schemes, in TAPSOFT ?97: Theory and Practice of Software Development, LNCS 1214, Springer-Verlag, 1997, pp. 490?501.","DOI":"10.1007\/BFb0030621"},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"Liang, C.: Compiler construction in higher order logic programming, in 4th International Symposium on Practical Aspects of Declarative Languages, LNCS 2257, Springer-Verlag, 2002, pp. 47?63.","DOI":"10.1007\/3-540-45587-6_5"},{"key":"CR22","unstructured":"Miller, D.: Unification of simply typed lambda-terms as logic programming, in Eighth International Logic Programming Conference, MIT Press, June 1991, pp. 255?269."},{"issue":"4","key":"CR23","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification, J. Logic Comput. 1(4) (1991), 497?536.","journal-title":"J. Logic Comput."},{"key":"CR24","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D. Miller","year":"1992","unstructured":"Miller, D.: Unification under a mixed prefix, J. Symbolic Comput. 14 (1992), 321?358.","journal-title":"J. Symbolic Comput."},{"key":"CR25","unstructured":"Mottl, M.: Automating functional program transformation, M.Sc. Thesis, Division of Informatics, University of Edinburgh, September 2000."},{"key":"CR26","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, C.: Confluence and preservation of strong normalization in an explicit substitution calculus, in Eleventh Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, July 1996, pp. 440?447.","DOI":"10.1109\/LICS.1996.561460"},{"key":"CR27","unstructured":"Nadathur, G.: A fine-grained notation for lambda terms and its use in intensional operations, J. Funct. Logic Programming 2 (March 1999)."},{"key":"CR28","unstructured":"Nadathur, G. and Miller, D.: An overview of ?Prolog, in K. A. Bowen and R. A. Kowalski (eds.), Fifth International Logic Programming Conference, MIT Press, August 1988, pp. 810?827."},{"issue":"1?2","key":"CR29","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/S0304-3975(97)00184-9","volume":"198","author":"G. Nadathur","year":"1998","unstructured":"Nadathur, G. and Wilson, D. S.: A notation for lambda terms: A generalization of environments, Theoret. Comput. Sci. 198(1?2) (1998), 49?98.","journal-title":"Theoret. Comput. Sci."},{"key":"CR30","doi-asserted-by":"crossref","unstructured":"Nadathur, G. and Mitchell, D. J.: System description: Teyjus ? a compiler and abstract machine based implementation of ?Prolog, in H. Ganzinger (ed.), Automated Deduction ? CADE-16, Lecture Notes in Artificial Intelligence 1632, Springer-Verlag, July 1999, pp. 287?291.","DOI":"10.1007\/3-540-48660-7_25"},{"key":"CR31","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L. C. and Wenzel, M.: Isabelle\/HOL ? A Proof Assistant for Higher-Order Logic, LNCS 2283, Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"CR32","doi-asserted-by":"crossref","unstructured":"Pfenning, F. and Elliott, C.: Higher-order abstract syntax, in Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, ACM Press, June 1988, pp. 199?208.","DOI":"10.1145\/53990.54010"},{"key":"CR33","doi-asserted-by":"crossref","unstructured":"Pfenning, F. and Sch\u00fcrmann, C.: System description: Twelf ? a meta-logical framework for deductive systems, in H. Ganzinger (ed.), Proceedings of the 16th International Conference on Automated Deduction (CADE-16), Trento, Italy, LNAI 1632, Springer-Verlag, July 1999, pp. 202?206.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"CR34","unstructured":"The Coq Development Team: The Coq proof assistant reference manual version 7.2, Technical Report 255, INRIA, February 2002. More recent versions may be obtained from the site http:\/\/coq.inria.fr\/."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-6885-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-004-6885-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-004-6885-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T21:24:23Z","timestamp":1586121863000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-004-6885-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,9]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2004,9]]}},"alternative-id":["6885"],"URL":"https:\/\/doi.org\/10.1007\/s10817-004-6885-1","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,9]]}}}