An Introduction to the Theory of Coalgebras Abstract: This course gives an introduction to the theory of coalgebras. In the recent years, coalgebras, the formal dual of algebras, have been recognised as foundational models in a wide range of areas. Applications include infinite (i.e. possibly non well-founded) data types, state based systems, operational semantics, automata theory, modal logics, and abstract models of infinite computations. The goal of the lecture is to familiarise the audience with the basic concepts of the field and to provide a solid basis for further research. Apart from the basic concepts, we cover definitions and proofs by coinduction and logics for reasoning about coalgebras in detail. We begin with examining concrete examples of coalgebras, such as transition systems, in order to motivate the general definitions. Using basic category theory (which we keep to a minimum), we introduce coalgebras, homomorphisms and behavioural equivalence. Using categorical duality, we make the algebra / coalgebra duality explicit, which allows to transfer many ideas and techniques from universal algebra. We use this transfer principle to obtain two important techniques: definitions and proofs by coinduction. In order to obtain coinductive definition principles, we formulate induction in terms of algebras and then apply duality. This way, we obtain coiteration, primitive corecursion and course-of-value corecursion as definition principles, each of which we illustrate by examples. Concerning proofs by coinduction, we discuss two different methods: The bisimulation proof method and proofs by terminal sequence induction, an inductive method for establishing behavioural equalities. Viewing coalgebras as state based systems, we then present logics, which can be used to reason about coalgebras. We identify semantical structures, which allow us to interpret multimodal logics over coalgebras. We concentrate on two main aspects of logics for coalgebras: expressivity (aka Hennessy-Milner property) and complete axiomatisations. We show, how coinductive techniques enable us to prove corresponding theorems.