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

			     S É M I N A I R E

                   ______                __    _
                  / ____/___ _____ ___  / /_  (_)_  ______ ___
                 / /   / __ `/ __ `__ \/ __ \/ / / / / __ `__ \
                / /___/ /_/ / / / / / / /_/ / / /_/ / / / / / /
                \____/\__,_/_/ /_/ /_/_.___/_/\__,_/_/ /_/ /_/

			     I N R I A - Paris
                 2 rue Simone Iff (ou: 41 rue du Charolais)
                                   En ligne

                           Lundi 11 janvier, 10h30

                              ------------------
                              Arthur Charguéraud
                              ------------------

                                    Inria

             ===================================================
             Sémantique big-step pour langages non-déterministes
             ===================================================

Dans cet exposé, je présenterai une définition inductive permettant de
caractériser la sémantique d'un langage non-déterministe en style big-step, et
d'en dériver la définition de triplets de Hoare.

Plus précisément, cet exposé vise à faire un tour d'horizon des définitions
possibles pour des triplets de Hoare vis-à-vis de sémantiques opérationnelles.
La sémantique peut être small-step ou bien big-step; le triplet peut capturer
la correction totale, la correction partielle, ou bien uniquement la
divergence; le langage peut être déterministe ou bien non-déterministe; la
sémantique peut inclure des programmes bloqués ou bien être complète (avec
propagation des erreurs). Je montrerai, pour chacune des 24 combinaisons
possibles, la ou les définitions pertinentes. Au total, je vous présenterai 20
définitions, dont 2 qui semblent nouvelles et particulièrement intéressantes,
à base de sémantique big-step non-déterministe. La première capture la
correction totale, via une définition inductive, tandis que la seconde capture
la correction partielle, via une interprétation co-inductive des mêmes règles
de dérivation.