Séminaire Cambium, Inria Paris
                                     BJ09
                          Vendredi 17 octobre, 10h30

                                 Basile Gros
                                   Verimag

       Dependent programming in Rocq with proxy-based small inversions.

The different techniques of inversion present in Rocq all have the same problem
of creating large and difficult to read proof terms. While this is rarely a
problem, dependent functions defined in a library with inversion are then not
readable to a user trying to understand them. Small inversions were created to
have an inversion method that creates lightweight proof terms that can be used
for dependent programming. We present a version of small inversions, proxy-based
small inversions, that relies on defining in advance inductive types that
specialise the type of the object we seek to invert.

            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.