Tutorial colocated with CADE-26, 7 August 2017, Gothenburg, Sweden
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:
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.
|09:00–10:00||Isabelle/jEdit and Higher-Order Logic|
|10:30–11:15||Datatypes and Recursion|
|15:30–16:15||Corecursion up to Friends|
The tutorial will be organized by