{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T17:38:23Z","timestamp":1748367503835,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":39,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677970"},{"type":"electronic","value":"9783540449577"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44957-4_16","type":"book-chapter","created":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T05:24:41Z","timestamp":1180675481000},"page":"239-253","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":21,"title":["Abstract Syntax for Variable Binders: An Overview"],"prefix":"10.1007","author":[{"given":"Dale","family":"Miller","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"issue":"4","key":"16_CR1","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"Martin Abadi","year":"1991","unstructured":"Martin Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 1(4):375\u2013416, October 1991.","journal-title":"Journal of Functional Programming"},{"issue":"5","key":"16_CR2","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. Bruijn de","year":"1972","unstructured":"N. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Math., 34(5):381\u2013392, 1972.","journal-title":"Indag. Math."},{"key":"16_CR3","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"Journal of Symbolic Logic"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Joelle Despeyroux, Amy Felty, and Andre Hirschowitz. Higher-order abstract syntax in Coq. In Second International Conference on Typed Lambda Calculi and Applications, pages 124\u2013138, April 1995.","DOI":"10.1007\/BFb0014049"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Joelle Despeyroux and Andre Hirschowitz. Higher-order abstract syntax with induction in Coq. In Fifth International Conference on Logic Programming and Automated Reasoning, pages 159\u2013173, June 1994.","DOI":"10.1007\/3-540-58216-9_36"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Joelle Despeyroux, Frank Pfenning, and Carsten Sch\u00fcrmann. Primitive recursion for higher-order abstract syntax. In Third International Conference on Typed Lambda Calculi and Applications, April 1997.","DOI":"10.1007\/3-540-62688-3_34"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. In D. Kozen, editor, Logic in Computer Science, pages 366\u2013374, 1995.","DOI":"10.1109\/LICS.1995.523271"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"M. P. Fiore, G. D. Plotkin, and D. Turi. Abstract syntax and variable binding. In Logic in Computer Science, pages 193\u2013202. IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782615"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"M. J. Gabbay and A. M. Pitts. A new approach to abstract syntax involving binders. In Logic in Computer Science, pages 214\u2013224. IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782617"},{"issue":"1","key":"16_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, 1993.","journal-title":"Journal of the ACM"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"M. Hofmann. Semantical analysis of higher-order abstract syntax. In Logic in Computer Science, pages 204\u2013213. IEEE Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782616"},{"key":"16_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G\u00e9rard Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27\u201357, 1975.","journal-title":"Theoretical Computer Science"},{"key":"16_CR13","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G\u00e9rard Huet and Bernard Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"key":"16_CR14","unstructured":"Dale Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Informal Proceedings of the Logical Frameworks BRA Workshop, June 1990. Available as UPenn CIS technical report MS-CIS-90-59."},{"issue":"4","key":"16_CR15","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1(4):497\u2013536, 1991.","journal-title":"J. of Logic and Computation"},{"key":"16_CR16","unstructured":"Dale Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255\u2013269, Paris, France, June 1991. MIT Press."},{"key":"16_CR17","doi-asserted-by":"crossref","unstructured":"Dale Miller. Abstract syntax and logic programming. In Logic Programming: Proceedings of the First and Second Russian Conferences on Logic Programming, number 592 in LNAI, pages 322\u2013337. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55460-2_24"},{"key":"16_CR18","doi-asserted-by":"crossref","unstructured":"Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, pages 321\u2013358, 1992.","DOI":"10.1016\/0747-7171(92)90011-R"},{"key":"16_CR19","doi-asserted-by":"crossref","unstructured":"Dale Miller and Gopalan Nadathur. Higher-order logic programming. In Ehud Shapiro, editor, Proceedings of the Third International Logic Programming Conference, pages 448\u2013462, London, June 1986.","DOI":"10.1007\/3-540-16492-8_94"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pages 247\u2013255, 1986.","DOI":"10.3115\/981131.981165"},{"key":"16_CR21","unstructured":"Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379\u2013388, San Francisco, September 1987."},{"key":"16_CR22","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125\u2013157, 1991.","journal-title":"Annals of Pure and Applied Logic"},{"key":"16_CR23","unstructured":"Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. In Pierpaolo Degano, Roberto Gorrieri, Alberto Marchetti-Spaccamela, and Peter Wegner, editors, ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, volume 31. ACM, Sep 1999. Article number 10."},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"John C. Mitchell and Eugenio Moggi. Kripke-style models for typed lambda calculus. Annals of Pure and Applied Logic, 51, 1991.","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"16_CR25","unstructured":"Gopalan Nadathur. A fine-grained notation for lambda terms and its use in intensional operations. Journal of Functional and Logic Programming, 1999(2), March 1999."},{"key":"16_CR26","unstructured":"Gopalan Nadathur and Dale Miller. An Overview of \u03bbProlog. In Fifth International Logic Programming Conference, pages 810\u2013827, Seattle, Washington, August 1988. MIT Press."},{"key":"16_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/3-540-48660-7_25","volume-title":"CADE-16","author":"G. Nadathur","year":"1999","unstructured":"Gopalan Nadathur and Dustin J. Mitchell. System description: Teyjus\u2014a compiler and abstract machine based implementation of \u03bbProlog. In H. Ganzinger, editor, CADE-16, pages 287\u2013291, Trento, Italy, July 1999. Springer LNCS."},{"issue":"1\u20132","key":"16_CR28","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(97)00184-9","volume":"198","author":"G. Nadathur","year":"1998","unstructured":"Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science, 198(1\u20132):49\u201398, 1998.","journal-title":"Theoretical Computer Science"},{"key":"16_CR29","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Higher-order critical pairs. In G. Kahn, editor, Sixth Annual Sym. on Logic in Computer Science, pages 342\u2013349. IEEE, July 1991.","DOI":"10.1109\/LICS.1991.151658"},{"key":"16_CR30","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Functional unification of higher-order patterns. In M. Vardi, editor, Eighth Annual Sym. on Logic in Computer Science, pages 64\u201374. IEEE, June 1993.","DOI":"10.1109\/LICS.1993.287599"},{"key":"16_CR31","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. The foundation of a generic theorem prover. Journal of Automated Reasoning, 5:363\u2013397, September 1989.","DOI":"10.1007\/BF00248324"},{"key":"16_CR32","unstructured":"Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 361\u2013386. Academic Press, 1990."},{"key":"16_CR33","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Elf: A language for logic definition and verified metaprogramming. In Fourth Annual Symposium on Logic in Computer Science, pages 313\u2013321, Monterey, CA, June 1989.","DOI":"10.1109\/LICS.1989.39186"},{"key":"16_CR34","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In G. Kahn, editor, Sixth Annual Symposium on Logic in Computer Science, pages 74\u201385. IEEE, July 1991.","DOI":"10.1109\/LICS.1991.151632"},{"key":"16_CR35","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1007\/3-540-61064-2_33","volume-title":"Proceedings of the Colloquium on Trees in Algebra and Programming","author":"F. Pfenning","year":"1996","unstructured":"Frank Pfenning. The practice of logical frameworks. In H\u00e9l\u00e9ne Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, volume LNCS 1059, pages 119\u2013134. Springer-Verlag, 1996."},{"key":"16_CR36","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Conal Elliot. Higher-order abstract syntax. In Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pages 199\u2013208. ACM Press, June 1988.","DOI":"10.1145\/960116.54010"},{"key":"16_CR37","doi-asserted-by":"crossref","unstructured":"Andrew M. Pitts and Murdoch J. Gabbay. A meta language for programming with bound names modulo renaming (preliminary report). Draft January 2000.","DOI":"10.1007\/10722010_15"},{"issue":"3","key":"16_CR38","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1093\/logcom\/6.3.315","volume":"6","author":"Z. Qian","year":"1996","unstructured":"Zhenyu Qian. Unification of higher-order patterns in linear time and space. J. Logic and Computation, 6(3):315\u2013341, 1996.","journal-title":"J. Logic and Computation"},{"key":"16_CR39","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90007-0","volume":"9","author":"R. Statman","year":"1979","unstructured":"Richard Statman. The typed \u03bb calculus is not elementary recursive. Theoretical Computer Science, 9:73\u201381, 1979.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Computational Logic \u2014 CL 2000"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44957-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T21:04:59Z","timestamp":1737061499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44957-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677970","9783540449577"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/3-540-44957-4_16","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"15 December 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}