Recently we have endowed the proof assistant Isabelle/HOL with a powerful framework for programming with, and reasoning about, infinite objects such as streams and infinite-depth trees. It implements the paradigm of total/productive coprogramming, and is based on a modular design of coinductive datatypes. The tutorial will present this framework through examples taken from the field of programming languages.

Mon 8 Jan
Times are displayed in time zone: Tijuana, Baja California change

09:00 - 10:30: Programming and Reasoning with Infinite Data in IsabelleTutorialFest at Hershey
09:00 - 10:30
Talk
TutorialFest
A: Mathias FleuryMPI-INF, A: Andreas Lochbihler, A: Andrei PopescuMiddlesex University, London
Media Attached
11:00 - 12:00: Programming and Reasoning with Infinite Data in IsabelleTutorialFest at Hershey
11:00 - 12:00
Talk
TutorialFest
A: Mathias FleuryMPI-INF, A: Andreas Lochbihler, A: Andrei PopescuMiddlesex University, London
Media Attached