{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:24Z","timestamp":1761611064968},"reference-count":40,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1998,5,1]],"date-time":"1998-05-01T00:00:00Z","timestamp":893980800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":5556,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1998,5]]},"DOI":"10.1016\/s0304-3975(97)00184-9","type":"journal-article","created":{"date-parts":[[2003,5,13]],"date-time":"2003-05-13T00:04:58Z","timestamp":1052784298000},"page":"49-98","source":"Crossref","is-referenced-by-count":21,"title":["A notation for lambda terms a generalization of environments"],"prefix":"10.1016","volume":"198","author":[{"given":"Gopalan","family":"Nadathur","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Debra Sue","family":"Wilson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"4","key":"10.1016\/S0304-3975(97)00184-9_BIB1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","article-title":"Explicit substitutions","volume":"1","author":"Abadi","year":"1991","journal-title":"J. Funct. Programming"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB2","doi-asserted-by":"crossref","first-page":"383","DOI":"10.1016\/0022-0000(81)90073-8","article-title":"An efficient interpreter for the lambda-calculus","volume":"23","author":"Aiello","year":"1981","journal-title":"J. Comput. System Sci."},{"issue":"5","key":"10.1016\/S0304-3975(97)00184-9_BIB3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem","volume":"34","author":"de Bruijn","year":"1972","journal-title":"Indag. Math."},{"key":"10.1016\/S0304-3975(97)00184-9_BIB4","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/S1385-7258(78)80025-0","article-title":"Lambda-calculus notation with namefree formulas involving symbols that represent reference transforming mappings","volume":"40","author":"de Bruijn","year":"1978","journal-title":"Indag. Math."},{"key":"10.1016\/S0304-3975(97)00184-9_BIB5","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"579","article-title":"A survey of the project AUTOMATH","author":"de Bruijn","year":"1980"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB7","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"issue":"2\/3","key":"10.1016\/S0304-3975(97)00184-9_BIB8","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inform. Comput."},{"issue":"2","key":"10.1016\/S0304-3975(97)00184-9_BIB9","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0167-6423(87)90020-7","article-title":"The categorical abstract machine","volume":"8","author":"Cousineau","year":"1987","journal-title":"Sci. Programming"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB10","doi-asserted-by":"crossref","first-page":"188","DOI":"10.1016\/S0019-9958(86)80047-X","article-title":"Categorical combinators","volume":"69","author":"Curien","year":"1986","journal-title":"Inform. and Control"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB11","series-title":"Categorical Combinators, Sequential Algorithms and Functional Programming","author":"Curien","year":"1986"},{"issue":"3","key":"10.1016\/S0304-3975(97)00184-9_BIB12","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/0304-3975(82)90026-3","article-title":"Orderings for term-rewriting systems","volume":"17","author":"Dershowitz","year":"1982","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(97)00184-9_BIB13","series-title":"Proc. 17th Ann. ACM Symp. on Principles of Programming Languages, ACM Press","first-page":"1","article-title":"On laziness and optimality in lambda interpreters: tools for specification and analysis","author":"Field","year":"1990"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB14","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/0168-0072(91)90022-E","article-title":"What's so special about Kruskal's theorem and the ordinal \u03930? A survey of some results in proof theory","volume":"53","author":"Gallier","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB15","article-title":"Edinburgh LCF: A Mechanised Logic of Computation","volume":"vol. 78","author":"Gordon","year":"1979"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB16","series-title":"Naive Set Theory","author":"Halmos","year":"1960"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB17","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(89)90105-9","article-title":"Confluence results for the pure strong categorical logic CCL. \u03bb-calculi as subsystems of CCL","volume":"65","author":"Hardin","year":"1989","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"10.1016\/S0304-3975(97)00184-9_BIB18","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB19","series-title":"Introduction to Combinatory Logic and Lambda Calculus","author":"Hindley","year":"1986"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB20","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","article-title":"A unification algorithm for typed \u03bb-calculus","volume":"1","author":"Huet","year":"1975","journal-title":"Theoret. Comput. Sci."},{"issue":"4","key":"10.1016\/S0304-3975(97)00184-9_BIB21","doi-asserted-by":"crossref","first-page":"797","DOI":"10.1145\/322217.322230","article-title":"Confluent reductions: abstract properties and applications to term rewriting systems","volume":"27","author":"Huet","year":"1980","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB22","series-title":"Formal structures for computation and deduction","author":"Huet","year":"1986"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB23","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/BF00264598","article-title":"Proving and applying program transformations expressed with second-order patterns","volume":"11","author":"Huet","year":"1978","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(97)00184-9_BIB24","article-title":"Combinatory Reduction Systems","volume":"volume 127","author":"Klop","year":"1980"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB25","series-title":"Computational Problems in Abstract Algebra","first-page":"263","article-title":"Simple word problems in universal algebras","author":"Knuth","year":"1970"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB26","first-page":"210","article-title":"Well-quasi-ordering, the tree theorem and V\u00e1zsonyi's conjecture","volume":"95","author":"Kruskal","year":"1960","journal-title":"Trans. Amer. Math. Soc."},{"key":"10.1016\/S0304-3975(97)00184-9_BIB27","series-title":"Basic Set Theory","author":"Levy","year":"1979"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB28","series-title":"IEEE Symp. on Logic Programming","first-page":"379","article-title":"A logic programming approach to manipulating formulas and programs","author":"Miller","year":"1987"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB29","article-title":"A fine-grained notation for lambda terms and its use in intensional operations","author":"Nadathur","year":"1996"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB40","unstructured":"J. Funct. Logic Programming, to appear."},{"key":"10.1016\/S0304-3975(97)00184-9_BIB30","article-title":"Implementation considerations for higher-order features in logic programming","author":"Nadathur","year":"1993"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB31","series-title":"Proc. 5th Internat. Logic Programming Conf.","first-page":"810","article-title":"An overview of \u03bbProlog","author":"Nadathur","year":"1988"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB32","series-title":"Proc. 1990 ACM Conf. on Lisp and Functional Programming, ACM Press","first-page":"341","article-title":"A representation of lambda terms suitable for operations on their intensions","author":"Nadathur","year":"1990"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB33","article-title":"Twards a fully parallel implementation of the lambda calculus","author":"O'Donnell","year":"1984"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB34","article-title":"The representation of logics in higher-order logic","author":"Paulson","year":"1987"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB35","doi-asserted-by":"crossref","DOI":"10.1007\/BF00248324","article-title":"The foundations of a generic theorem prover","author":"Paulson","year":"1988"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB36","series-title":"Proc. 4th Ann. Symp. on Logic in Computer Science, IEEE Computer Society Press","first-page":"313","article-title":"Elf: a language for logic definition and verified metaprogramming","author":"Pfenning","year":"1989"},{"key":"10.1016\/S0304-3975(97)00184-9_BIB37","series-title":"Proc. ACM-SIGPLAN Conf. on Programming Language Design and Implementation, ACM Press","first-page":"199","article-title":"Higher-order abstract syntax","author":"Pfenning","year":"1988"},{"issue":"1","key":"10.1016\/S0304-3975(97)00184-9_BIB38","first-page":"201","article-title":"A new technique for analysing parameter passing, applied to the lambda calculus","volume":"3","author":"Staples","year":"1981","journal-title":"Australian Comput. Sci. Comm."},{"key":"10.1016\/S0304-3975(97)00184-9_BIB39","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/0304-3975(89)90104-7","article-title":"Church-Rosser Theorem for a rewriting system on categorical combinators","volume":"65","author":"Yokouchi","year":"1989","journal-title":"Theoret. Comput. Sci."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597001849?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397597001849?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,26]],"date-time":"2019-04-26T17:29:13Z","timestamp":1556299753000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397597001849"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,5]]},"references-count":40,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1998,5]]}},"alternative-id":["S0304397597001849"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(97)00184-9","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1998,5]]}}}