Functional Program Correctness Through Types

This thesis addresses the problem of avoiding errors in functionalprograms. The thesis has three parts, discussing different aspects ofprogram correctness, with the unifying theme that types are anintegral part of the methods used to establish correctness.The first part validates a common, but not obviously correct, methodfor reasoning about functional programs. In this method, dubbed "fastand loose reasoning", programs written in a language withnon-terminating functions are treated as if they were written in atotal language. It is shown that fast and loose reasoning is soundwhen the programs are written in a given total subset of the language,and the resulting properties are translated back to the partialsetting using certain partial equivalence relations which capture theconcept of totality.The second part discusses a method for ensuring that functions meetspecified time bounds. The method is aimed at implementations ofpurely functional data structures, which often make essential use oflazy evaluation to ensure good time complexity in the presence ofpersistence. The associated complexity analyses are often complicatedand hence error-prone, but by annotating the type of every functionwith its time complexity, using an annotated monad to combine timecomplexities of subexpressions, it is ensured that no details areforgotten.The last part of the thesis is a case study in programming with stronginvariants enforced by the type system. A dependently typed objectlanguage is represented in the meta language, which is alsodependently typed, in such a way that it is impossible to formill-typed terms. An interpreter is then implemented for the objectlanguage by using normalisation by evaluation. By virtue of the strongtypes used this implementation is a proof that every term has a normalform, and hence normalisation is proved. This also seems to be thefirst formal account of normalisation by evaluation for a dependentlytyped language