## You are here

# Rewriting Calculi for Computation and Logic

**Abstract:**

*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

__ Prerequisites__:

- 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.