
Logic & Semantics 
A mathematical proof is generally made of clever deductions and mechanizable computations. However, current proof assistants (Coq, Lego, Nuprl, HOL, etc.) have a rather simple computation mechanism. Although they allow one to express many functions (any function whose existence is provable in intuitionist higherorder arithmetic), definitions can be uneasy and sometimes inefficient (they must follow a very restrictive schema similar to primitive recursion). Therefore, these systems do not allow one to define functions and predicates as one would like, which makes them difficult to use for nonspecialists and restrict the use of computations in proofs: some propositions that could be proved automatically, by a simple computation, require complex deductions. Conversely, with a richer computation notion, but such that the equality of two terms remain decidable, it is not necessary to memorize the computation steps. Proofs are then reduced to true deductions. And the size of proofs is a critical problem in current proof assistants.
Definitions with rewrite rules are more general, easier and may be more efficient. However, considering functions or predicates defined by a set of a priori arbitrary rewrite rules raises an important problem: can we check whether a proof is correct? This is the decidability of "type checking".
In this talk, I will present the interest of extending the Calculus of Constructions with function and predicate definitions based on rewrite rules. Then, I will give general conditions ensuring the decidability of typechecking. These conditions generalize all the previous work on the combination lambdacalculus and rewriting, include the Calculus of Inductive Constructions with strong elimination and can also be applied to Natural Deduction Modulo.
(Frédéric comes from LRI, Université ParisSud; he is in the Computer Lab doing a postdoc with Larry Paulson.)