Séminaire Cambium, Inria Paris
                                  Anita Borg
                            Vendredi 29 mai, 10h30

                                 Noé De Santo
                          University of Pennsylvania

              Combining Dependent, Uniqueness, and Borrow Types

Many proof assistants allow users to verify programs out of the box, thanks to
the type theory at their core acting as a programming language. However, these
programming languages typically do not allow mutation, or at least not in a
first class manner. In this talk, I'll report on some work-in-progress about a
dependent type system which allows some lightweight forms of mutation, using
ideas from uniqueness and borrow types.

            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.