Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Confluence in UnTyped Higher-Order Theories by means of Critical Pairs

Gaspard Férey 1 Jean-Pierre Jouannaud 1 
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LMF - Laboratoire Méthodes Formelles
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. We develop here techniques that reduce confluence proofs to the checking of various forms of critical pairs for higher-order rewrite rules extending beta-reduction on pure lambda-terms. The present paper concentrates on the case where rewrite rules are left-linear and critical pairs can be joined without using beta-rewrite steps. The other two cases will be addressed in forthcoming papers.
Document type :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Tuesday, September 14, 2021 - 4:13:29 PM
Last modification on : Friday, August 5, 2022 - 2:58:08 PM


Files produced by the author(s)


  • HAL Id : hal-03126102, version 3


Gaspard Férey, Jean-Pierre Jouannaud. Confluence in UnTyped Higher-Order Theories by means of Critical Pairs. 2021. ⟨hal-03126102v3⟩



Record views


Files downloads