The complexity of verifying functional programs

Abstract

The set of finite interpretations in which a formula is valid is called the spectrum of the formula. For some program logics, the classes of spectra form complete subclasses of well known complexity classes. For various imperative and functional programming languages we know the complexity classes corresponding to the classes of spectra of partial correctness formulae. This means that for those formulae we know how hard it is to decide the sets of finite models. For some imperative languages it has already been shown that constructing formal proofs for valid formulae is of the same order of complexity. In this paper we prove the same result, i.e. that proofs can be constructed efficiently, for functional languages where recursive functions of arbitrary finite type are allowed. Since denotational semantics translates imperative programs into functional terms, the proof system for functional programs gives one for imperative programs as well. Choosing the right denotational semantics, we can show the effiency of the resulting verification method for Clarke’s language L4.