Mon 8 Jan 2018 09:00 - 10:30 at Hershey - Programming and Reasoning with Infinite Data in Isabelle
Mon 8 Jan 2018 11:00 - 12:00 at Hershey - Programming and Reasoning with Infinite Data in Isabelle
Mon 8 Jan 2018 11:00 - 12:00 at Hershey - Programming and Reasoning with Infinite Data in Isabelle
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.