Rewriting in modular setting

We consider the extension of the Calculus of Constructions with
modules and rewriting. Having rewriting in the conversion relation of
the calculus permits the automatization of equational proof steps and
compression of proof terms. Modules are needed to help users to cope
with large proofs, providing abstraction mechanism and name-space
management. They also can be used to represent mathematical
structures. Even though rewriting and modules seem orthogonal
concepts, they interfere in many ways.

We will present how rewriting can be introduced into an interactive
theorem prover in order to guarantee the strong normalization and the
confluence of the underlying reduction. Then we will discuss possible
interactions with different module systems, namely the variant of
Ocaml module system and the Module Calculus by Judicael Courant.

In the end we will discuss the specification calculus, the highly
parameterized calculus which presents modules, rewriting, and inductive
types in a uniform and elegant way.