Certified Functional (Co)programming with Isabelle/HOL

Tutorial colocated with CADE-26, 7 August 2017, Gothenburg, Sweden

Description

Over the past five years, the organizers have developed programming capabilities for finite and infinite (lazy) data structures in the Isabelle/HOL proof assistant, using the foundational approach characteristic of provers based on higher-order logic (HOL, also called simple type theory).

In contrast with the Isabelle tutorial at CADE-25, the focus will be on verified programming using the subset of Isabelle/HOL that corresponds to a typed functional programming language. The focus will be on mechanisms specific to Isabelle/HOL, notably:

  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 researchers with no or little prior experience with Isabelle or any other proof assistant, but with some experience with a typed functional programming language (e.g., Haskell, OCaml, Scala, Standard ML).

The tutorial will contain several hands-on exercises. We expect the attendants to bring laptops (with at least 2 cores and 4 GB memory) and have Isabelle installed before the start of the tutorial. Isabelle is freely available for Linux, Mac, and Windows. We will be using Isabelle2016-1.

Tentative Schedule

09:00–10:00    Isabelle/jEdit and Higher-Order Logic
10:00–10:30Coffee Break
10:30–11:15Datatypes and Recursion
11:15–12:00Codatatypes
12:00–14:00Lunch Break
14:00–15:00Primitive Corecursion
15:00–15:30Coffee Break
15:30–16:15Corecursion up to Friends
16:10–17:00Mixed Recursion/Corecursion

Organizers

The tutorial will be organized by

Resources