{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,15]],"date-time":"2026-01-15T01:26:01Z","timestamp":1768440361752,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540164920","type":"print"},{"value":"9783540398318","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1986]]},"DOI":"10.1007\/3-540-16492-8_94","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:48:52Z","timestamp":1330195732000},"page":"448-462","source":"Crossref","is-referenced-by-count":70,"title":["Higher-order logic programming"],"prefix":"10.1007","author":[{"given":"Dale A.","family":"Miller","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gopalan","family":"Nadathur","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"34_CR1","doi-asserted-by":"publisher","first-page":"841","DOI":"10.1145\/322326.322339","volume":"29","author":"K. R. Apt","year":"1982","unstructured":"Krzysztof R. Apt and M. H. van Emden, \u201cContributions to the Theory of Logic Programming\u201d JACM, Vol 29 (1982), 841\u2013862.","journal-title":"JACM"},{"key":"34_CR2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Alonzo Church, \u201cA Formulation of the Simple Theory of Types,\u201d Journal of Symbolic Logic 5 (1940), 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"34_CR3","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/322358.322370","volume":"30","author":"S. Fortune","year":"1983","unstructured":"Steven Fortune, Daniel Leivant, and Michael O'Donnell, \u201cThe Expressiveness of Simple and Second-Order Type Structures\u201d, J.ACM Vol. 30(1), January 1983, pp. 151\u2013185.","journal-title":"J.ACM"},{"key":"34_CR4","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1016\/0304-3975(81)90040-2","volume":"13","author":"W. D. Goldfarb","year":"1981","unstructured":"Warren D. Goldfarb, \u201cThe Undecidability of the Second-Order Unification Problem,\u201d Theoretical Computer Science 13 (1981), 225\u2013230.","journal-title":"Theoretical Computer Science"},{"key":"34_CR5","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"G\u00e9rard P. Huet, \u201cA Unification Algorithm for Typed \u03bb-calculus,\u201d Theoretical Computer Science 1 (1975), 27\u201357.","journal-title":"Theoretical Computer Science"},{"key":"34_CR6","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/BF00264598","volume":"11","author":"G. P. Huet","year":"1978","unstructured":"G\u00e9rard P. Huet, Bernard Lang, \u201cProving and Applying Program Transformations Expressed with Second-Order Patterns\u201d Acta Informatica 11 (1978), 31\u201355.","journal-title":"Acta Informatica"},{"key":"34_CR7","unstructured":"Dale A. Miller, \u201cProofs in Higher-order Logic,\u201d Ph. D. Dissertation, Carnegie-Mellon University, August 1983."},{"key":"34_CR8","unstructured":"Dale A. Miller, \u201cA Theory of Modules for Logic Programming,\u201d University of Pennsylvania Technical Report, 1986."},{"key":"34_CR9","unstructured":"Dale A. Miller, Gopalan Nadathur, \u201cA Computational Logic Approach to Syntax and Semantics,\u201d 10th Annual Symposium of the Mathematical Foundations of Computer Science, IBM Japan, May 1985."},{"key":"34_CR10","unstructured":"Dale A. Miller, Gopalan Nadathur, \u201cAn Abstract Interpreter for a Higher Order Extension of Prolog,\u201d forthcoming UPenn technical report, December 1985."},{"key":"34_CR11","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Robin Milner, \u201cA Theory of Type Polymorphism in Programming,\u201d Journal of Computer and System Sciences 17, 348\u2013375, 1978.","journal-title":"Journal of Computer and System Sciences"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"A. Mycroft and R. A. O'Keefe, \u201cA Polymorphic Type System for Prolog,\u201d Artificial Intelligence, Vol. 23(3), August 1984.","DOI":"10.1016\/0004-3702(84)90017-1"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds, \u201cThree Approaches to Type Structure\u201d, Proceedings of the International Joint Conference on Theory and Practice of Software Development, March 1985.","DOI":"10.1007\/3-540-15198-2_7"},{"issue":"4","key":"34_CR14","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/321978.321991","volume":"23","author":"M. H. Emden van","year":"1976","unstructured":"M. H. van Emden, R. A. Kowalski, \u201cThe semantics of predicate logic as a programming language,\u201d J.ACM 23 4 (Oct. 1976), 733\u2013742.","journal-title":"J.ACM"},{"key":"34_CR15","first-page":"441","volume":"10","author":"D. H. D. Warren","year":"1982","unstructured":"D. H. D. Warren, \u201cHigher-order extension to PROLOG: are they needed?\u201d, Machine Intelligence 10, 1982, pp. 441\u2013454.","journal-title":"Machine Intelligence"},{"key":"34_CR16","doi-asserted-by":"crossref","unstructured":"David Scott Warren, \u201cUsing \u03bb-Calculus to Repressent Meaning in Logic Grammars\u201d in the Proceedings of the 21st Annual Meeting of the Association for Computational Linguistics, June 1983, 51\u201356.","DOI":"10.3115\/981311.981321"}],"container-title":["Lecture Notes in Computer Science","Third International Conference on Logic Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-16492-8_94.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:10:43Z","timestamp":1605643843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-16492-8_94"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986]]},"ISBN":["9783540164920","9783540398318"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-16492-8_94","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1986]]}}}