Membership Equational Logic, Calculus of Inductive Constructions, and Rewrite Logic (Extended Abstract)

AbstractMany of the above ideas arose when discussing with people of the afore mentionned groups (Coq, Demons, Maude, PROTHEO), and especially with Gilles Dowek and Christine Paulin. Mitsuhiro Okada also deserves special thanks for introducing me to the Curry-Howard world, while I was introducing him to its Hurry-Coward counterpart