Anzeige
Erschienen in:
1985 | ReviewPaper | Buchkapitel
Program verification in a logical theory of constructions
verfasst von : Peter Dybjer
Erschienen in: Functional Programming Languages and Computer Architecture
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The logical theory of constructions is a simple theory which combines functional programs and intuitionistic predicate calculus. Here we propose that it is a practical alternative to other constructive programming logics, such as Martin-Löf's type theory. Its main advantage is that it admits reasoning directly about general recursion, while maintaining that all typed programs terminate. We illustrate the use of this theory by verifying the general recursive subtractive division program.