Co 2017 - Certified Functional (Co) programming with Isabelle/HOL

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 HOL provers. 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.