Blogs (27) >>
ICFP 2017
Sun 3 - Sat 9 September 2017 Oxford, United Kingdom
Sun 3 Sep 2017 14:00 - 15:00 at L5 - Afternoon tutorial session 1

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:

Sun 3 Sep

icfp-2017-tutorials
14:00 - 15:00: Tutorials - Afternoon tutorial session 1 at L5
icfp-2017-tutorials150444000000014:00 - 15:00
Talk