Membership Equational Logic, Calculus of Inductive Constructions,
and Rewrite Logic
This paper is part of a long-term effort to
increase expressiveness of specification languages while at the same
time having a Curry-Howard semantic basis on which three major tools
can be based, namely efficient execution by rewriting, powerful
interactive and automated theorem-proving environments, and extraction
of provably correct code from specifications. This effort is conducted
in collaboration within the research project of the DEMONS team at
LRI, University Paris-Sud at Orsay, and the Coq project at
INRIA-Rocquencourt and its users. Some aspects are also investigated
in collaboration with the PROTHEO project at INRIA-Lorraine. It also
benefits from our long-standing collaboration with the Maude project
at SRI-CSL.
full paper