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

Authors: 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}
  }