Although computers have a finite memory and cannot store an infinite amount of information, Functional Programming and Type Theory allow us to represent infinite mathematical objects. These are realized as processes that generate part of the structure at every step. The mathematical/categorical formulation for these processes is the notion of coalgebra. The first part of the course is an introduction to coalgebras with important examples like streams (infinite sequences) and non-well-founded trees. The most powerful proof method for infinite data structures is the Coinduction Principle, which allows us to prove that two objects are the same by a bisimulation, itself an coalgebraic process that generates an infinite equality proof by successive stages. We will study methods to construct sound infinite objects, to solve recursive equations on them and to prove their properties. I will give examples using functional programming in Haskell and formal reasoning in Coq. In Type Theory we can define coinductively not just single types, but families of types, predicates and relations. This leads to a proof technique in which the statement to be proved can be used recursively as long as it satisfies a guardedness condition. It amounts to constructing a proof with an infinite number of logical steps. We can combine coinduction with induction in several ways to define types with a complex internal structure. One example is the definition of all continuous functions between streams. A further generalization consists in defining a coinductive type simultaneously with a recursive function on it, in the style of induction-recursion. This leads to the very general notion of Wander types, that can be instantiated to many of the most common type-theoretic constructions.