Description

During the past five years, the Isabelle/HOL proof assistant has been extended with rich programming capabilities for finite and infinite (lazy) data structures – using the foundational approach characteristic of HOL provers. While the ICFP/POPL communities have been widely exposed to type-theoretic approaches embodied in Coq or Agda (including by means of tutorials), the HOL alternative also has interesting ideas, especially when it comes to (1) reaching a balance between guaranteed termination/productivity and expressiveness, (2) mixing recursion with corecursion soundly, and (3) obtaining compositional proof methods that match the program definitions.

The tutorial will target Isabelle novices. However, a strong background in functional programming will be assumed. The tutorial will focus on advanced functional programming techniques and the associated proof techniques offered by Isabelle/HOL. The basic concepts of the Isar proof language will be covered as well.

The tutorial will contain several hands-on exercises. We expect the attendants to bring laptops and have the latest version of Isabelle installed before the start of the tutorial.

Material:

• Slides
• Induction.thy
• Coinduction.thy
• Friends.thy
• Language.thy (with proof holes), Language_Sol.thy (solution)