OCC - An Open Calculus of Constructions

Mark-Oliver Stehr

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.

Relevant References:

  1. Mark-Oliver Stehr: CINNI - A New Calculus of Explicit Substitutions and its Application to Pure Type Systems, Manuscript, CSL, SRI-International, Menlo Park, CA, USA, May 1999
  2. Manuel Clavel, Francisco Duran, Steven Eker, Jose Meseguer, Mark-Oliver Stehr: Maude as a Formal Meta-Tool. In the proceedings of FM'99, The World Congress On Formal Methods. Toulouse, France, September 20-24, 1999. Also appeared in the book OBJ/CafeOBJ/Maude at Formal Methods '99, Kokichi Futatsugi, Joseph Goguen and Jose Meseguer (Eds.), Theta (Bucharest), September 1999, ISBN 973-99097-1-X.
  3. Mark-Oliver Stehr: Type Theory in a Membership Equational Logic Framework (Talk given at Cornell)
  4. Mark-Oliver Stehr, Jose Meseguer: Pure Type Systems in Rewriting Logic , Proceedings of LFM'99: Workshop on Logical Frameworks and Meta-languages, Paris, France, September 28, 1999. Paper available here . Extended version submitted for publication.