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