Keywords: Calculus of Constructions, Higher Order Logic, Typed Lambda Calculus, Equational Logic, Rewriting Logic
Rewriting logic together with it's membership equational sublogic favors the use of abstract specifications. It has a flexible computation system based on conditional rewriting modulo equations, and via its initial semsntics it supports a very liberal notion of inductive definitions. Pure type systems, on the other hand, in particular the calculus of constructions, provide higher-order (dependent) types, but they are based on a fixed notion of computation, namely beta-reduction. This unsatisfying situation has been addressed by addition of inductive definitions (Ch. Pauline-Mohring 1993, Z. Luo 1994) and algebraic extensions in the style of abstract data type systems (Blanqui, Jouannaud, Okada 1999). Also, the idea of overcoming these limitations using some combination of membership equational logic with the calculus of constructions has been suggested as a long-term goal by Jouannaud 1998.
To close the gap between these two different paradigms of equational logic and higher-order type theory we are currently investigating the open calculus of constructions (OCC) an equational variant of the calculus of constructions with an open computational system and a flexible universe hierarchy. Using Maude and the ideas on the Calculus of Indexed Names and Named Indices (CINNI) and Uniform Pure Type Systems (UPTS), we have developed an experimental proof assistant for OCC that has additional features such as definitions and meta-variables. Maude has been extremely useful to explore the potential of OCC from the very early stage of its design. In addition, the formal executable specification of OCC exploits the reflective capabilities of Maude, yielding an computational efficiency that brings us closer the the goal of a unified tool for programming, specification and verification integrating equational logic, higher-order logic and dependent types.