Equational programming in λ-calculus

A system of equations in λ-calculus is a pair (Γ, X) where Γ is a set of formulas of Λ (the equations) and X is a finite set of variables of Λ (the unknowns). A system S=(Γ, X) is said to be solvable in the theory T (T-solvable) if there exists a simultaneous substitution with closed λ-terms for the unknowns that makes the formulas of Γ theorems in the theory T. A class of systems for which the β-solvability problem is decidable in polynomial time is defined. This class yields an equational programming language in which constraints on the code generated by the compiler can be specified by the user and (properties of) data structures can be described in an abstract way