Séminaire Cambium, Inria Paris
                                  Paul Erdös
                           Vendredi 26 juin, 10h30

                              Roger Burtonpatel
                          University of Pennsylvania

                  Enhanced Coinduction and Interaction Trees

Coinduction is a fundamental proof technique of computer science whose
applications include proving properties about infinite structures, be they
streams, concurrent systems, or nonterminating programs. But despite its
positioning as a cornerstone of reasoning in the field, it is relatively
understudied, especially when compared to its popular cousin induction. In the
past few decades, however, coinduction has enjoyed a surge in popularity as
researchers have sought methods for infinite-scale reasoning about programs,
leading to increasingly expressive proof systems and better implementations in
proof assistants.
In this talk, I cover coinduction from both a theoretical and
historical perspective, and explain how I used the enhanced coinduction
techniques of the rocq-coinduction library to rewrite the underlying theory in
the coinductive library of Interaction Trees. I explain the coinductive proof
technique in theoretical and practical terms, highlight parts of its history,
and demonstrate the motivation and results of the transition from Parametrized
Coinduction to Enhanced Coinduction in the refactor.

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct
                            via le lien ci-dessus.