Program verification in a logical theory of constructions

Abstract

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.