# zbMATH — the first resource for mathematics

A unification algorithm for typed $$\overline\lambda$$-calculus. (English) Zbl 0337.68027

##### MSC:
 68W30 Symbolic computation and algebraic computation 68W99 Algorithms in computer science 68Q25 Analysis of algorithms and problem complexity 03B40 Combinatory logic and lambda calculus
Full Text:
##### References:
 [1] Andrews, P.B., Resolution in type theory, J. symb. logic, 36, 3, 414-432, (1971) · Zbl 0231.02038 [2] Church, A., A formulation of the simple theory of types, J. symb. logic, 5, 1, 56-68, (1940) · JFM 66.1192.06 [3] Darlington, J.L., A partial mechanization of second-order logic, (), 91-100 · Zbl 0261.68041 [4] Darlington, J.L., Automatic program synthesis in second-order logic, Proceedings of 3rd intern. joint conf. on artificial intelligence, (1973) [5] Ernst, G.W., A matching procedure for type theory, Personal communication, (1971) [6] Gould, W.E., A matching procedure for ω-order logic, Scientific report no. 4, 66-781, (1966), AD 646 560. [7] Guard, J.R., Automated logic for semi-automated mathematics, Scientific report no. 1, 64-411, (1964), AD 602 710. [8] Hindley, J.R.; Lercher, B.; Seldin, J.P., Introduction to combinatory logic, () · Zbl 0269.02005 [9] Huet, G.P., Constrained resolution: a complete method for type theory, () · Zbl 0337.68027 [10] Huet, G.P., Unification en théorie des types, Séminaire IRIA théorie des automates, des languages et de la programmation, (1973), volume [11] Huet, G.P., The undecidability of unification in third order logic, Information and control, 22, 3, 257-267, (1973) · Zbl 0257.02038 [12] Huet, G.P., A mechanization of type theory, Proceedings of 3rd intern. joint conf. on artificial intelligence, (1973) [13] Jensen, D.; Pietrzykowski, T., Mechanizing ω-order type theory through unification, () · Zbl 0361.02020 [14] Lucchesi, C.L., The undecidability of the unification problem for third order languages, () [15] Pietrzykowski, T., A complete mechanization of second order logic, J. assoc. comp. Mach., 20, 2, 333-364, (1971) · Zbl 0253.68021 [16] Pietrzykowski, T.; Jensen, D., A complete mechanization of ω-order type theory, Assoc. comp. Mach. nat. conf., Vol. 1, 82-92, (1972) [17] Robinson, G.A.; Wos, L.T., Paramodulation and theorem proving in first-order theories with equality, (), 135-150 · Zbl 0219.68047 [18] Robinson, J.A., A machine-oriented logic based on the resolution principle, J. assoc. comp. Mach., 12, 1, 23-41, (1965) · Zbl 0139.12303
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.