Inductive and Coinductive Reasoning with Isabelle/HOL (ISA)

Course at Midlands Graduate School 2021

Andrei Popescu

University of Sheffield

This course will provide an accessible, hands-on description of basic and advanced mechanisms for inductive and coinductive reasoning. It welcomes participants who use rigorous mathematical constructions in their day-to-day research and wish to widen their perspective on, and improve their arsenal of, practical induction and coinduction. The concepts will be illustrated with examples and exercises formalized in the proof assistant Isabelle/HOL, taking advantage of the substantial extension of Isabelle/HOL's (co)induction infrastructure in recent years. People who already have some familiarity with Isabelle will make the most of the exercises. However, the presented concepts themselves are proof-assistant independent hence understandable without any knowledge of Isabelle. The topics covered range from basic ones such as

inductive and coinductive predicates founded on Knaster-Tarski fixed points and
inductive datatypes and structural recursion

to more advanced ones such as

compositional, nested datatypes and codatatypes and
expressive corecursion "up-to" and mixed recursion-corecursion.

Links to course material will be provided here. Please refresh your browser window when you access this page.

	Isabelle exercises	Slides	Recordings
Monday		Lecture 1	Lecture 1
Tuesday	Exercise Session 1 Solutions	Inductive Predicates
Wednesday	Exercise Session 2 Solutions	Coinductive Predicates	Lecture 3
Thursday	Characterization Theorem — list-based Characterization Theorem — set-based
Friday		Datatypes and Codatatypes