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 in From Object-Orientation to Formal Methods: Essays in Memory of Ole-Johan Dahl , LNCS 2635, Springer-Verlag (available in pdf and ps).
  5. Mark-Oliver Stehr: Programming, Specification, and Interactive Theorem Proving - Towards a Unified Language based on Equational Logic, Rewriting Logic, and Type Theory , Doctoral Thesis, Fachbereich Informatik, Universität Hamburg, 2002. Published as E-Dissertation here by SUB Hamburg. Abstract available in html and ps. Thesis available in ps and pdf.
  6. M.-O. Stehr: The Open Calculus of Constructions: An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving (Part I and II). To appear in Fundamenta Informaticae. An earlier and longer draft is available here.
  7. I. Cervesato, M.-O. Stehr: Representing the MSR Cryptoprotocol Specification Language in an Extension of Rewriting Logic with Dependent Types. Fifth International Workshop on Rewriting Logic and its Applications (WRLA'2004), Barcelona, Spain, March 27 - 28, 2004, Electronic Notes in Theoretical Computer Science, Elsevier, 2004. Paper available here.
  8. M.-O. Stehr: Higher-Order Rewriting via Conditional First-Order Rewriting in the Open Calculus of Constructions. In Proceedings of HOR'04, 2nd International Workshop on Higher-Order Rewriting, Aachen, Germany, June 2, 2004, Aachener Informatik Berichte, AIB-2004-03, RWTH Aachen, Department of Computer Science, June 2004. Paper available in ps and pdf.
Presentations:
  1. The Open Calculus of Constructions and its Semantics . Talk at the 2nd Workshop on Coq and Rewriting September 22 - 24 2004, LIX, Palaiseau, France (slides available in ppt and pdf).
  2. The Open Calculus of Constructions as a Tool for Inductive and Coinductive Specification and Reasoning . Invited talk at the Workshop on Algorithms and Tools for Coinductive Reasoning, September 16 - 22, 2004, Dresden, Germany (slides available in ppt and pdf).
  3. Higher-Order Rewriting via Conditional First-Order Rewriting in the Open Calculus of Constructions . Invited talk at HOR'2004, June 2, Aachen, Germany (available in ps and pdf).
  4. The Open Calculus of Constructions: A Framework for Executable Mathematics. Ecole Polytechnique, Laboratoire d'Informatique - LIX, December 12, 2003, Paris. Slides available here.
  5. Tutorial: Explicit Substitutions and the Open Calculus of Constructions . Given at WRLA'2002, 4th International Workshop on Rewriting Logic and its Applications, Pisa, Italy, September 19--21, 2002.

OCC/Maude Prototype

The OCC/Maude prototype is available here. It is built on top of Maude 2.0 (see here), but requires a special version of the Maude engine, which is included in this package. The package contains the following files:
  1. README: a brief description of OCC/Maude and instructions on how to run the examples
  2. doc: papers and talks related to OCC
  3. bin: directory containing the version of Maude that is required by OCC
  4. sys: directory containing the Maude sources of OCC
  5. occ.maude: a Maude file that loads all required files and starts up OCC
  6. lib: some libraries with commonly used types and functions
  7. examples: a collection of examples (all these are included in examples.occ)
  8. tutorial: all examples from the tutorial (all these are included in tutorial.occ)
  9. unity: a UNITY-sytle temporal logic library
  10. echo: different specifications of a distributed algorithm

OCC/Prolog Prototype

The OCC/Prolog prototype is available here. It has been tested with SWI Prolog (available here). It is the most comprehensive prototype implementation of OCC available (see the README file below for all its features), but it is much less efficient than OCC/Maude, and in the present version only recommended for small examples. The package contains the following files:
  1. README: a brief description of OCC/Prolog and instructions on how to run the examples
  2. doc: papers and talks related to OCC
  3. sys: directory containing the Prolog sources of OCC
  4. occ: a script that loads starts up Prolog and OCC
  5. The following are OCC/Maude files with some minor changes for use with OCC/Prolog:
    1. lib.old: some libraries with commonly used types and functions
    2. examples: a collection of examples (all these are included in examples.occ)
    3. tutorial: all examples from the tutorial (all these are included in tutorial.occ)
    4. unity: a UNITY-sytle temporal logic library
    5. echo: specification of a distributed algorithm
  6. lib.new: some libraries using the new OCC/Prolog syntax
  7. testing: some random examples for OCC/Prolog
  8. hor: all examples (and more) from the paper on higher order rewriting
  9. behavioral: some examples of behavioral specifications
  10. msr: some examples of crytographic protocols translated from MSR into OCC using the method of the paper on representing MSR
[Homepage] [Department] [University]