Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                          Salle Lions 1, bâtiment C
                          Lundi 19 septembre, 10h30

                                Guilhem Jaber
                             Université de Nantes

            From game semantics to verification of OCaml programs

Game semantics provides a representation of open programs in the form
of sequences of actions representing possible interactions with the
environment. It is particularly suited to studying higher-order
programming languages with side effects, for which it provides
fully-abstract models. As the manipulated sequences of actions are of
simple complexity, it also allows one to reason automatically about
such programs, via model-checking techniques.

In this talk, we present how game semantics models some of the
features of the OCaml programming language. We will introduce a
representation of the polymorphism of the type system as a dynamic
sealing process that constrains the interactions of the environment.
We will also see how nominal techniques represent the dynamic
allocation of resources such as (higher-order) references.

To allow automation of reasoning via temporal logics, we will
introduce a Kripke-style reasoning technique that provides a
separation between control flow and data flow. Finally, we will
discuss the remaining challenges to overcome in order to modularly
verify OCaml programs.

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

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn