Coinduction, the dual of induction, is a fundamental principle for defining infinite objects and proving properties about them. The broad applicability and rapidly increasing interest in... Show moreCoinduction, the dual of induction, is a fundamental principle for defining infinite objects and proving properties about them. The broad applicability and rapidly increasing interest in coinductive techniques is based on the theory of coalgebras, which allows one to understand and prove properties of state-based models of computation at a high level of abstraction. In this thesis we develop methods that simplify and enhance coinductive reasoning, with coalgebra as the framework of choice to obtain generally applicable techniques. In the first part, we introduce a coalgebraic framework of enhanced coinductive proof methods, which is applicable to a wide range of coinductive predicates and a wide range of state-based systems. In the second part, we propose enhancements to coinductive definition techniques based on the theory of mathematical operational semantics. Show less
