The notion of rewrite rule gives rise to several concepts:

- - The rewrite relation: it has been extensively studied since the seventies and is central in the study and operationalisation of equational logic
- - the rewriting logic: introduced by José Meseguer at the beginning of the nineties, it generalises equational logic in forgetting about its symmetry
- - More recently we have introduced with Horatiu Cirstea the rewriting calculus that consider the rewrite arrow as an abstractor and where the explicit application of a rewrite rule to a term produces a set of results. This calculus generalises the lambda calculus and provides by its binding mechanism a powerful tool to model and prove.

This presentation will be based on joint works with Horatiu Cirstea and Luigi Liquori.