Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic

Induction and coinduction are two complementary techniques used in mathematics and computer science. These techniques occur together, for example, in control systems: On the one hand, control systems are expected to run until turned off and to always react to their environment. This is what we call coinductive computations. On the other hand, they have to make internal computations. Restricting these computations to terminating, that is inductive, computations ensures that the systems continue to react to their environment. We develop in this thesis techniques for programming inductive-coinductive systems, and for describing their properties and proving these properties. The focus is on developing formal languages, in which proofsare written by humans and can be verified by a computer. This ensures the correctness of those proofs and thereby of the programmed systems. Due to their generality, the developed languages are also applicable to the formalisation of mathematics.