|
| << vorige | volgende >> |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 4 van 5 gevonden artikelen
| Titel: |
The Open Calculus of Constructions (Part II): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving |
| Auteur: |
Mark-Oliver Stehr |
| Verschenen in: |
Fundamenta informaticae |
| Paginering: | Jaargang 68 (2005) nr. 3 pagina's 249-288 |
| Jaar: |
2005-09-16 |
| Inhoud: |
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. |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 4 van 5 gevonden artikelen
| << vorige | volgende >> |