Testing and Proving in Dependent Type Theory

We show how random testing, model checking and interactive proving can be combined for functional program verification in dependent type theory. <p />We extend the proof assistant Agda/Alfa for dependent type theory with a tool for random testing of functional programs, thus combining proving and testing in one system. Testing is used for debugging programs and specifications before a proof is attempted. Proving is used to decompose a goal into subgoals that can be subjected to testing before attempting to make a proof. Proving can guide the testing strategy to test all branches of a case statement and thus make it possible to localize the source of a bug more precisely. We show how some classic data structure algorithms (binary search tree insertion and AVL-tree insertion) are verified in the system. As a further case study, we show how the correctness of a BDD-algorithm written in Haskell is verified by testing properties of component functions. <p />We then augment the proof assistant Agda/Alfa with a simple tool for model checking boolean formulas using binary decision diagrams. We show two applications of this tool. The first is to prove Urquhart's U-formulas using a combination of interactive proving and testing. The second one is the verification of a sorting algorithm (bitonic sort) using a combination of interactive proving, model checking, and random testing. <p />Our tool uses test data generators which are defined inside Agda/Alfa. We can therefore use the type system to prove properties about them, in particular surjectivity stating that all possible test cases can indeed be generated. We discuss how surjective generators can be written for a class of inductively defined dependent types by using the correspondence between inductive definitions and logic programs. As an example, we give a generator for theorems in propositional logic. <p />The last part of the thesis is an advanced case study in formalisation and proving. We describe a formalisation of a reduction-free normalisation function nf for the typed lambda calculus. To extract the normalisation function nf, we develop a constructive category theory, which is called P-category theory, and a formalisation of the typed lambda calculus. From this we prove numerous properties of the typed lambda calculus. Two different approaches to formalising the typed lambda calculus are presented in ALF. Properties of the typed lambda calculus are organised in a categorical way, using the notion of categories with families. It is proved that the two approaches are equivalent as categorical structures