## Paper: Combining algebra and higher-order types (at LICS 1988)

**Val Breazu-Tannen**

### Abstract

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 β-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 β and η 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

### BibTeX

@InProceedings{BreazuTannen-Combiningalgebraand, author = {Val Breazu-Tannen}, title = {Combining algebra and higher-order types}, booktitle = {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)}, year = {1988}, month = {July}, pages = {82--90}, location = {Edinburgh, Scotland, UK}, publisher = {IEEE Computer Society Press} }