You are here

Rewriting Calculi for Computation and Logic


Lecturer: Claude Kirchner, Inria, France

The rho-calculi provide enlightening concepts for both computing and reasoning as well as their combination. They consist in the generalization of lambda-calculus to structures like terms, propositions or graphs. We will first introduce, define and study them. We will then show how their interrelations with deduction provide powerful frameworks to understand uniformly current deduction mechanisms and how they can be used to design the next generation of proof assistants.

The following topics will be covered:

  • Rewriting calculus
  • Deduction modulo
  • Rewriting modulo 
  • Rewriting logic


  • Equational logic
  • Basics on Term rewriting and lambda calculus
  • First-order unification and matching
  • First-order logic 

Material for the presentations can be obtained here.

Slides used in the presentation can be downloaded from here.