Functional Program Correctness Through Types

This thesis addresses the problem of avoiding errors in functional programs. The thesis has three parts, discussing different aspects of program correctness, with the unifying theme that types are an integral part of the methods used to establish correctness. The first part validates a common, but not obviously correct, method for reasoning about functional programs. In this method, dubbed “fast and loose reasoning”, programs written in a language with non-terminating functions are treated as if they were written in a total language. It is shown that fast and loose reasoning is sound when the programs are written in a given total subset of the language, and the resulting properties are translated back to the partial setting using certain partial equivalence relations which capture the concept of totality. The second part discusses a method for ensuring that functions meet specified time bounds. The method is aimed at implementations of purel