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 (19)

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

This page was built for publication: The Clausal Theory of Types