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

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