Abstract: The rewriting calculus
Claude Kirchner
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.
The talk will motivate the rewriting calculus and present its
properties and some of its modelling capabilities. I will also show
how the abstraction mechanism allows us to define type systems that
generalise those of the lambda cube. Then the ELAN system that
provides a partial implementation of the rewriting calculus will be
shortly presented.
This presentation will be based on joint works with Horatiu Cirstea
and Luigi Liquori.