{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:17:02Z","timestamp":1742959022501,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417392"},{"type":"electronic","value":"9783540447160"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","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":[[2001]]},"DOI":"10.1007\/3-540-44716-4_1","type":"book-chapter","created":{"date-parts":[[2007,8,15]],"date-time":"2007-08-15T18:16:34Z","timestamp":1187201794000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["The Metalanguage \u03bbprolog and Its Implementation"],"prefix":"10.1007","author":[{"given":"Gopalan","family":"Nadathur","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,21]]},"reference":[{"issue":"4","key":"1_CR1","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1017\/S0956796800000186","volume":"1","author":"M. Abadi","year":"1991","unstructured":"M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L\u00e9vy. Explicit substitutions. Journal of Functional Programming, 1(4):375\u2013416, 1991.","journal-title":"Journal of Functional Programming"},{"key":"1_CR2","unstructured":"A. W. Appel and A. P. Felty. Lightweight lemmas in \u03bbProlog. In International Conference on Logic Programming, pages 411\u2013425. MIT Press, November 1999."},{"key":"1_CR3","unstructured":"P. Brisset and O. Ridoux. Naive reverse can be linear. In K. Furukawa, editor, Eighth International Logic Programming Conference, pages 857\u2013870. MIT Press, June 1991."},{"key":"1_CR4","unstructured":"P. Brisset and O. Ridoux. The compilation of \u03bbProlog and its execution with MALI. Publication Interne 687, IRISA, 1992."},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1006\/inco.1999.2837","volume":"157","author":"G. Dowek","year":"2000","unstructured":"G. Dowek, T. Hardin, and C. Kirchner. Higher-order unification via explicit substitutions. Information and Computation, 157:183\u2013235, 2000.","journal-title":"Information and Computation"},{"issue":"1","key":"1_CR6","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/BF00881900","volume":"11","author":"A. Felty","year":"1993","unstructured":"A. Felty. Implementing tactics and tacticals in a higher-order logic programming language. Journal of Automated Reasoning, 11(1):43\u201381, August 1993.","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"1_CR7","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1017\/S0960129500001559","volume":"2","author":"J. Hannan","year":"1992","unstructured":"J. Hannan and D. Miller. From operational semantics to abstract machines. Mathematical Structures in Computer Science, 2(4):415\u2013459, 1992.","journal-title":"Mathematical Structures in Computer Science"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet. A unification algorithm for typed \u03bb-calculus. Theoretical Computer Science, 1:27-57, 1975.","journal-title":"Theoretical Computer Science"},{"key":"1_CR9","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. Huet","year":"1978","unstructured":"G. Huet and B. Lang. Proving and applying program transformations expressed with second-order patterns. Acta Informatica, 11:31\u201355, 1978.","journal-title":"Acta Informatica"},{"issue":"1","key":"1_CR10","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1016\/0096-0551(94)90012-4","volume":"20","author":"K. Kwon","year":"1994","unstructured":"K. Kwon, G. Nadathur, and D.S. Wilson. Implementing polymorphic typing in a logic programming language. Computer Languages, 20(1):25\u201342, 1994.","journal-title":"Computer Languages"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"J. Lamping. An algorithm for optimal lambda calculus reduction. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 16\u201330. ACM Press, 1990.","DOI":"10.1145\/96709.96711"},{"key":"1_CR12","unstructured":"J.-J. L\u00e9vy. Optimal reductions in the lambda-calculus. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 159\u2013191. Academic Press, 1980."},{"key":"1_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"490","DOI":"10.1007\/BFb0030621","volume-title":"TAPSOFT \u201997: Theory and Practice of Software Developmen","author":"C. Liang","year":"1997","unstructured":"C. Liang. Let-polymorphism and eager type schemes. In TAPSOFT \u201997: Theory and Practice of Software Development, pages 490\u2013501. Springer Verlag LNCS Vol. 1214, 1997."},{"key":"1_CR14","unstructured":"S. Michaylov and F. Pfenning. An empirical study of the runtime behavior of higher-order logic programs. In D. Miller, editor, Proceedings of the Workshop on the \u03bbProlog Programming Language, pages 257\u2013271, July 1992. Available as University of Pennsylvania Technical Report MS-CIS-92-86."},{"issue":"4","key":"1_CR15","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation, 1(4):497\u2013536, 1991.","journal-title":"Journal of Logic and Computation"},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"D. Miller","year":"1992","unstructured":"D. Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14:321\u2013358, 1992.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/3-540-58025-5_58","volume-title":"Proceedings of the 1993 Workshop on Extensions to Logic Programming","author":"D. Miller","year":"1994","unstructured":"D. Miller. A proposal for modules in \u03bbProlog. In R. Dyckho, editor, Proceedings of the 1993 Workshop on Extensions to Logic Programming, pages 206\u2013221. Springer-Verlag, 1994. Volume 798 of Lecture Notes in Computer Science."},{"key":"1_CR18","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"D. Miller, G. Nadathur, F. Pfenning, and A. 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"},{"issue":"1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/BF00881902","volume":"11","author":"G. Nadathur","year":"1993","unstructured":"G. Nadathur. A proof procedure for the logic of hereditary Harrop formulas. Journal of Automated Reasoning, 11(1):115\u2013145, August 1993.","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR20","volume-title":"Technical Report TR-98-01","author":"G. Nadathur","year":"1998","unstructured":"G. Nadathur. An explicit substitution notation in a \u03bbProlog implementation. Technical Report TR-98-01, Department of Computer Science, University of Chicago, January 1998."},{"key":"1_CR21","unstructured":"G. Nadathur. A fine-grained notation for lambda terms and its use in intensional operations. Journal of Functional and Logic Programming, 1999(2), March 1999."},{"issue":"2","key":"1_CR22","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/0743-1066(95)00037-K","volume":"25","author":"G. Nadathur","year":"1995","unstructured":"G. Nadathur, B. Jayaraman, and K. Kwon. Scoping constructs in logic programming: Implementation problems and their solution. Journal of Logic Programming, 25(2):119\u2013161, November 1995.","journal-title":"Journal of Logic Programming"},{"key":"1_CR23","volume-title":"Technical Report CS-1993-16","author":"G. Nadathur","year":"1993","unstructured":"G. Nadathur, B. Jayaraman, and D.S. Wilson. Implementation considerations for higher-order features in logic programming. Technical Report CS-1993-16, Department of Computer Science, Duke University, June 1993."},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"G. Nadathur and D. Miller. Higher-order logic programming. In D. Gabbay, C. Hogger, and A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 499\u2013590. Oxford University Press, 1998.","DOI":"10.1093\/oso\/9780198537922.003.0011"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"G. Nadathur and D.J. Mitchell. System description: Teyjus\u2014a compiler and abstract machine based implementation of \u03bbProlog. In H. Ganzinger, editor, Automated Deduction-CADE-16, number 1632 in Lecture Notes in Artificial Intelligence, pages 287\u2013291. Springer-Verlag, July 1999.","DOI":"10.1007\/3-540-48660-7_25"},{"key":"1_CR26","unstructured":"G. Nadathur and F. Pfenning. The type system of a higher-order logic programming language. In F. Pfenning, editor, Types in Logic Programming, pages 245\u2013283. MIT Press, 1992."},{"key":"1_CR27","unstructured":"G. Nadathur and G. Tong. Realizing modularity in \u03bbProlog. Journal of Functional and Logic Programming, 1999(9), April 1999."},{"issue":"1-2","key":"1_CR28","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1016\/S0304-3975(97)00184-9","volume":"198","author":"G. Nadathur","year":"1998","unstructured":"G. Nadathur and D. S. Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science, 198(1-2):49\u201398, 1998.","journal-title":"Theoretical Computer Science"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"G.C. Necula. Proof-carrying code. In 24th Annual ACM Symposium on Principles of Programming Languages, pages 106\u2013119. ACM Press, January 1997.","DOI":"10.1145\/263699.263712"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G.D. Plotkin, editors, Logical Frameworks, pages 149\u2013181. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.008"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Elliott. 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":"1_CR32","doi-asserted-by":"crossref","unstructured":"F. Pfenning and C. Sch\u00fcrmann. System description: Twelf-a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202\u2013206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"1_CR33","unstructured":"O. Ridoux. MALIv06: Tutorial and reference manual. Publication Interne 611, IRISA, 1991."},{"key":"1_CR34","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1007\/3-540-55602-8_189","volume-title":"Automated Deduction-CADE-11","author":"N. Shankar","year":"1992","unstructured":"N. Shankar. Proof search in the intuitionistic sequent calculus. In D. Kapur, editor, Automated Deduction-CADE-11, number 607 in Lecture Notes in Computer Science, pages 522\u2013536. Springer Verlag, June 1992."},{"key":"1_CR35","unstructured":"D.H.D. Warren. An abstract Prolog instruction set. Technical Note 309, SRI International, October 1983."}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44716-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,8]],"date-time":"2021-02-08T22:13:17Z","timestamp":1612822397000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44716-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417392","9783540447160"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/3-540-44716-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"21 March 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}