Dr. Andrei Popescu, Middlesex University London
Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
Corecursion is a mechanism for defining functions that produce infinite objects such as streams, lazy lists and infinite-depth trees. Establishing corecursion schemes that are expressive, sound and automatic is a notoriously hard problem. I will discuss an approach, implemented in the proof assistant Isabelle/HOL, for "training" a logical system to learn stronger and stronger schemes on a sound basis. The central notion is that of a friendly operator (or friend), which constitutes a safe context for corecursive calls. The framework relies on the ability to recognize friends quasi-automatically by verifying some relational parametricity conditions.
My talk will also include a general discussion about proof assistants and the advantages they have over traditional programming languages.
(joint work with Jasmin Blanchette, Aymeric Bouzy , Andreas Lochbihler and Dmitriy Traytel)