The aim of this project is to integrate program verification based on Type theory into classical program verification. This will be done by building a wide-spectrum, partially constructive logic that includes computational and noncomputational reasoning along with higher-order functions, destructive operations, and assignment. The semantics for this logic does not dichotimize constructive and nonconstructive reasoning but instead views them as being two poles of a continuum, with the partially constructive verified programs interesting to computer scientists in between. The logic will be implemented and test programs will be written for it. This new logic will be an advance over the logics currently available for program verification: it will be powerful enough and flexible enough to support constructive reasoning over functional and imperative programs, using one common syntax and semantics. Programs written with the logic will be efficient and concise. In addition, the existence of such a logic can be used to claim that constructive and classical verification, often thought to be inherently incompatible, are actually related parts of a larger whole.
