{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:36:49Z","timestamp":1725457009141},"publisher-location":"Berlin\/Heidelberg","reference-count":19,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540074163"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0029526","type":"book-chapter","created":{"date-parts":[[2005,12,6]],"date-time":"2005-12-06T14:42:57Z","timestamp":1133880177000},"page":"192-212","source":"Crossref","is-referenced-by-count":4,"title":["Unification in typed lambda calculus"],"prefix":"10.1007","author":[{"given":"G\u00e9rard","family":"Huet","sequence":"first","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"11_CR1","doi-asserted-by":"crossref","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"Andrews P.B., (1971): \u201c Resolution in type theory\u201d. Journal of Symbolic Logic 36, 3 pp. 414\u2013432.","journal-title":"Journal of Symbolic Logic"},{"issue":"1","key":"11_CR2","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"Church A. (1940): \u201cA formulation of the simple theory of types\u201d Journal of Symbolic Logic 5,1 pp. 56\u201368.","journal-title":"Journal of Symbolic Logic"},{"key":"11_CR3","unstructured":"Church A. (1941): \u201cThe calculi of lambda-conversion\u201d. Annals of Mathematical Studies n\u22186. Princeton University Press."},{"key":"11_CR4","unstructured":"Curry H.B., Feys R., Craig W. (1958): Combinatory Logic, vol 1, North Holland."},{"key":"11_CR5","first-page":"91","volume-title":"Machine Intelligence 6","author":"J.L. Darlington","year":"1971","unstructured":"Darlington J.L., (1971): \u201cA partial mechanization of second-order logic\u201d. Machine Intelligence 6, pp. 91\u2013100. American Elsevier, New York."},{"key":"11_CR6","unstructured":"Darlington J.L. (1973): \u201cAutomatic program synthesis in second-order logic\u201d. Proceedings 3rd IJCAI, Stanford August 73."},{"key":"11_CR7","unstructured":"Ernst G.W. (1971): \u201cA matching procedure for type theory\u201d. Personal communication."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Gould W.E. (1966): \u201cA matching procedure for \u03c9-order logic\u201d. Scientific report n\u22184, AFCRL 666-781. Contrat AF 19(628)-3250.AD 646-560.","DOI":"10.21236\/AD0646560"},{"key":"11_CR9","unstructured":"Guard J.R. (1964): \u201cAutomated logic for semi-automated mathematics\u201d. Scientific report n\u22181, AFCRL-64-411. Contrat AF 19(628)-3250. AD 602 710."},{"issue":"3","key":"11_CR10","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/S0019-9958(73)90301-X","volume":"22","author":"G.P. Huet","year":"1973","unstructured":"Huet G.P. (1973): \u201cThe undecidability of unification in third order logic\u201d. Information and Control 22,3 pp. 257\u2013267.","journal-title":"Information and Control"},{"key":"11_CR11","unstructured":"Huet G.P. (1973): \u201cA mechanization of type theory\u201d. Proceedings of 3rd IJCAI, Stanford August 73."},{"key":"11_CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(75)90008-0","volume":"1","author":"G.P. Huet","year":"1975","unstructured":"Huet G.P. (1975): \u201cA unification algorithm for typed \u03bb-calculus\u201d. Theoretical Computer Science 1,1.","journal-title":"Theoretical Computer Science"},{"key":"11_CR13","unstructured":"Lucchesi C.L. (1972): \u201cThe undecidability of the unification problem for third order languages\u201d. Report CSRR 2059, Dept. of Applied Analysis and Computer Science. University of Waterloo."},{"issue":"2","key":"11_CR14","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/321752.321764","volume":"20","author":"T. Pietrzykowski","year":"1971","unstructured":"Pietrzykowski T. (1971): \u201cA complete mechanization of second order logic\u201d. Journal of Assoc. for Comp. Mach. 20,2 pp. 333\u2013364.","journal-title":"Journal of Assoc. for Comp. Mach."},{"key":"11_CR15","first-page":"82","volume":"1","author":"T. Pietrzykowski","year":"1972","unstructured":"Pietrzykowski T. and Jensen D. (1972): \u201c A complete mechanization of \u03c9-order type theory\u201d. Association for computing Machinery National Conference 1972, vol.1, pp. 82\u201392.","journal-title":"Association for computing Machinery National Conference 1972"},{"key":"11_CR16","first-page":"73","volume-title":"Machine Intelligence 7","author":"G.D. Plotkin","year":"1972","unstructured":"Plotkin G.D. (1972): \u201cBuilding-in equational theories\u201d. Machine Intelligence 7, pp. 73\u201390. American Elsevier. New York."},{"issue":"1","key":"11_CR17","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson J.A. (1965): \u201cA machine-oriented logic based on the resolution principle\u201d. Journal of Assoc. for Comp. Mach. 12,1, pp.23\u201341.","journal-title":"Journal of Assoc. for Comp. Mach."},{"issue":"3","key":"11_CR18","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1305\/ndjfl\/1093956080","volume":"VIII","author":"L.E. Sanchis","year":"1967","unstructured":"Sanchis L.E. (1967): \u201cFunctionals defined by recursion\u201d. Notre Dame Journal of Formal Logic VIII, 3 pp. 161\u2013174.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"11_CR19","unstructured":"Jensen D. & Pietrzykowski T. (1973): \u201cMechanizing \u03c9-order type theory through unification\u201d. Report CS-73-16, Dept. of Applied Analysis and Computer Science, University of Waterloo."}],"container-title":["Lecture Notes in Computer Science","\u03bb-Calculus and Computer Science Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0029526.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T21:59:42Z","timestamp":1607551182000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0029526"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540074163"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0029526","relation":{},"subject":[]}}