Draft, July 2007 Extended Static Checking of Call-by-Value Functional Programs

Abstract We present a Hoare logic for a call-by-value programming lan-guage equipped with recursive, higher-order functions, algebraic data types, and a polymorphic type system in the style of Hind-ley and Milner. It is the theoretical basis for a tool that extracts proof obligations out of programs annotated with logical assertions.These proof obligations, expressed in a typed, higher-order logic, are discharged using off-the-shelf automated or interactive theoremprovers. Although the technical apparatus that we exploit is by now standard, its application to call-by-value functional programminglanguages appears to be new, and (we claim) deserves attention. As a sample application, we check the partial correctness of a balancedbinary search tree implementation