Membership Equational Logic, Calculus of Inductive Constructions, and Rewrite Logic (Extended Abstract)
Jean-Pierre Jouannaud · Electronic Notes in Theoretical Computer Science · 1998
Many 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.