Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs

Abstract User-defined higher-order rewrite rules are becoming a standard in proof assistants based on intuitionistic type theory. This raises the question of proving that they preserve the properties of beta-reductions for the corresponding type systems. In a series of papers, we develop techniques ... View More