This program is tentative and subject to change.

Mon 16 Jan 2023 09:00 - 10:30 at Park - Tutorials 2A
Mon 16 Jan 2023 11:00 - 12:30 at Park - Tutorials 2B

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.

This program is tentative and subject to change.

Mon 16 Jan

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 10:30
Tutorials 2ATutorialFest at Park
09:00
90m
Tutorial
Isabelle/HOL: Foundations, Induction, and Coinduction
TutorialFest
Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen
11:00 - 12:30
Tutorials 2BTutorialFest at Park
11:00
90m
Tutorial
Isabelle/HOL: Foundations, Induction, and Coinduction
TutorialFest
Andrei Popescu University of Sheffield, Dmitriy Traytel University of Copenhagen