The Open Calculus of Constructions (Part II): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving

Article type: Research Article

Authors: Stehr, Mark-Oliver

Affiliations: University of Illinois at Urbana-Champaign, Computer Science Department, Urbana, IL 61801, USA. E-mail: [email protected]

Abstract: The open calculus of constructions integrates key features of Martin-Löf's type theory, the calculus of constructions, membership equational logic, and rewriting logic into a single uniform language. The two key ingredients are dependent function types and conditional rewriting modulo equational theories. We explore the open calculus of constructions as a uniform framework for programming, specification and interactive verification in an equational higher-order style. By having equational logic and rewriting logic as executable sublogics we preserve the advantages of a first-order semantic and logical framework and we provide a foundation for a broad spectrum of applications ranging from what could be called executable mathematics, involving symbolic computations and logical proofs, to software and system engineering applications, involving symbolic execution and analysis of nondeterministic and concurrent systems.

Keywords: Equational Specification, Rewriting Logic, Type Theory

Journal: Fundamenta Informaticae, vol. 68, no. 3, pp. 249-288, 2005