Deduction modulo is a way to remove computational arguments from proofs by reasoning
modulo a congruence on propositions. Such a technique, issued from automated theorem …

This paper presents general syntactic conditions ensuring the strong normalisation and the
logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus …

In a previous work (“Abstract Data Type Systems”, TCS 173 (2), 1997), the last two authors
presented a combined language made of a (strongly normalizing) algebraic rewrite system …

We give a first-order presentation of higher-order logic based on explicit substitutions. This
presentation is intentionally equivalent to the usual presentation of higher-order logic based …

Several authors devised type-based termination criteria for ML-like languages allowing non-
structural recursive calls. We extend these works to general rewriting and dependent types …

We show how to incorporate rewriting into the Calculus of Constructions and we prove that
the resulting system is strongly normalizing with respect to beta and rewrite reductions. An …

We give a short constructive proof of the fact that certain binary relations> are well-founded,
given a lifting≫ á la Ferreira-Zantema and a well-founded relation>. This construction …

Deduction modulo is a way to express a theory using computation rules instead of axioms.
We present in this paper an extension of deduction modulo, called Polarized deduction …

Ce mémoire est une introduction à un dossier d'habilitation composé d'articles écrits entre
1994 et 1998 et référencés ci-dessous [a, b, c, d, e, f, g, h, i, j]. Par ailleurs, une annexe …

The goal of this note is to compare two notions, one coming from the theory of rewrite
systems and the other from proof theory: confluence and cut elimination. We show that to …