This tutorial has two parts. The first part is a general introduction to the Isabelle/HOL proof assistant and in particular to its logical foundations: higher-order logic. The second part will introduce the audience to basic and advanced mechanisms for inductive and coinductive reasoning in a proof assistant. Although we will continue to use Isabelle for all our hands-on examples and exercises in the second part, many of the ideas are largely proof-assistant independent, hence relevant beyond Isabelle. We target researches that have some experience with typed functional programming. Familiarity with using a proof assistant would be useful, but is not a prerequisite.