The Clausal Theory of Types

DOI10.1017/CBO9780511569906zbMath0782.68007MaRDI QIDQ5966632

D. A. Wolfram

Publication date: 23 January 1993

zbMATH Keywords

functional and logic programmingclausal theory of typeshigher-order equational unification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Research exposition (monographs, survey articles) pertaining to computer science (68-02) Logic programming (68N17) Combinatory logic and lambda calculus (03B40)

Related Items

Third order matching is decidable, Towards a domain theory for termination proofs, A restricted form of higher-order rewriting applied to an HDL semantics, Expressing combinatory reduction systems derivations in the rewriting calculus, Higher-order rewrite systems and their confluence, Modular AC unification of higher-order patterns, Higher order conditional rewriting and narrowing, Developing developments, Semantics for abstract clauses, An alternate proof of Statman's finite completeness theorem, Decidability of bounded higher-order unification, Third-order matching in the polymorphic lambda calculus, Unification and matching modulo nilpotence, On the confluence of lambda-calculus with conditional rewriting, Higher-order matching for program transformation, On the longest perpetual reductions in orthogonal expression reduction systems, Complexity of nilpotent unification and matching problems., Perpetuality and uniform normalization in orthogonal rewrite systems, Combinatory reduction systems: Introduction and survey