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

Displayed time zone: Tijuana, Baja California change

09:00 - 10:30
Programming and Reasoning with Infinite Data in IsabelleTutorialFest at Hershey
09:00
90m
Talk
Programming and Reasoning with Infinite Data in Isabelle/HOL.
TutorialFest
A: Mathias Fleury MPI-INF, A: Andreas Lochbihler , A: Andrei Popescu Middlesex University, London
Media Attached
11:00 - 12:00
Programming and Reasoning with Infinite Data in IsabelleTutorialFest at Hershey
11:00
60m
Talk
Programming and Reasoning with Infinite Data in Isabelle/HOL.
TutorialFest
A: Mathias Fleury MPI-INF, A: Andreas Lochbihler , A: Andrei Popescu Middlesex University, London
Media Attached