Séminaire Cambium, Inria Paris
                                     BJ09
                          Vendredi 27 février, 10h30

                                 Jean Caspar

                    A zoo of partial continuity properties

When we call a function of type (Q → A) → R in Rocq, it may only call its
argument a finite number of time. This property, which can be seen as some form
of continuity, can be formalized in several different ways, yielding different
definitions. Baillon et al. compared existing definitions and analysed which
implications between them holds. However, we work in Rocq, and some implications
which do not hold are not provably false, but unprovable in a constructive
setting. To prove that they are unprovable, we prove that they imply a known
unprovable formula.
In my work, I generalize the definitions of continuity and
their analysis to "pure" partial functions, for which the same intuition holds:
if a partial function (Q ⇀ A) ⇀ R terminates on some input, then it must have
called it a finite number of time.

            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.