|
| << previous | next >> |
Journal description
All volumes of the corresponding journal
All issues of the corresponding volume
All articles of the corresponding issues
Details for article 4 of 5 found articles
| Title: |
The Open Calculus of Constructions (Part II): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving |
| Author: |
Mark-Oliver Stehr |
| Appeared in: |
Fundamenta informaticae |
| Paging: | Volume 68 (2005) nr. 3 pages 249-288 |
| Year: |
2005-09-16 |
| Contents: |
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. |
| Publisher: |
IOS Press |
| Source file: |
Elektronische Wetenschappelijke Tijdschriften |
Details for article 4 of 5 found articles
| << previous | next >> |