Combining algebra and higher-order types

The author studies the higher-order rewrite/equational proof systems obtained by adding the simply typed lambda calculus to algebraic rewrite/equational proof systems. He shows that if a many-sorted algebraic rewrite system has the Church-Rosser property, then the corresponding higher-order rewrite system which adds simply typed beta -reduction has the Church-Rossers property too. This result is relevant to parallel implementations of functional programming languages. The author also shows that provability in the higher-order equational proof system obtained by adding the simply typed beta and eta axions to some many-sorted algebraic proof system is effectively reducible to provability in that algebraic proof system. This effective reduction also establishes transformations between higher-order and algebraic equational proofs, which can be useful in automated deduction.<>