Blogs (28) >>
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

Displayed time zone: Belfast change

14:00 - 15:00
Afternoon tutorial session 1Tutorials at L5
14:00
60m
Talk
Tutorial T2: Certified Functional (Co)programming with Isabelle/HOL
Tutorials
P: Jasmin Blanchette Vrije Universiteit Amsterdam, P: Andreas Lochbihler , P: Andrei Popescu Middlesex University, London, P: Dmitriy Traytel ETH Zurich