We use cookies on this site. By browsing our site you agree to our use of cookies. Close this message Find out more

Home > Computer Science home > Events > Seminar Dr. Andrei Popescu
More in this section Events articles

Seminar Dr. Andrei Popescu

16/05/2017 (15:00-16:00)

Andrei Popescu

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)



Comment on this page

Did you find the information you were looking for? Is there a broken link or content that needs updating? Let us know so we can improve the page.

Note: If you need further information or have a question that cannot be satisfied by this page, please call our switchboard on +44 (0)1784 434455.

This window will close when you submit your comment.

Add Your Feedback