Wednesday 23rd August, AFTERNOON SESSION
Andrei Popescu, University of Sheffield.
I will illustrate the induction and coinduction facilities of the Isabelle/HOL proof assistant, covering inductive and coinductive datatypes and predicates, as well as recursion and corecusion. As a working example, I will give a formal proof of the equivalence between Knaster-Tarski least/greatest fixpoints and provability by finite/infinite proof trees — which is a foundational result for (co)induction in proof assistants. If time allows, I will also show how Isabelle caters for a sound mixture of recursion and corecursion.
BACKGROUND:
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle was originally developed at the University of Cambridge and Technische Universität München, but now includes numerous contributions from institutions and individuals worldwide. See the Isabelle overview for a brief introduction.
SPEAKER:
Andrei Popescu is a senior lecturer (associate professor) in the Security of Advanced Systems research group of the Department of Computer Science at the University of Sheffield. Previously, He worked as a lecturer at Middlesex University and as a postdoctoral researcher at TU Munich, in the Chair for Logic and Verification headed by Tobias Nipkow and patroned by goddess Isabelle.