13 Mars - 19 Mars


Retour à la vue des calendrier
Mardi 14 Mars
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Géométrie combinatoire : densité d'hypergraphes et méthode probabiliste
Description: Xavier Goaoc Un hypergraphe à n sommets dont aucune projection sur k sommet n'est complète a au plus O(n^{k-1}) arêtes. Ce résultat, découvert simultanément par Sauer, Vapnick-Chervonenkis et Perles-Shelah au début des années 1970, est fondamental en apprentissage. En géométrie combinatoire et algorithmique, il permet souvent de contrôler la complexité (globale) d'une structure par sa "densité" locale. J'introduirai à ce mécanisme avant de présenter quelques extensions récentes, obtenues conjointement avec Boris Bukh (https://arxiv.org/abs/1701.06632), qui permettent un controle plus fin de la complexité. L'exposé ne supposera aucune connaissance préalable et un des ingrédients sera une construction probabiliste.
Jeudi 16 Mars
Heure: 15:30 - 16:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Preserving Partial Order Runs in Parametric Time Petri Nets
Description: Cesar Rodriguez Parameter synthesis for timed systems aims at deriving parameter
valuations satisfying a given property.
In this paper we target concurrent systems; it is well known that
concurrency is a source of state-space explosion, and partial order
techniques were defined to cope with this problem.
Here we use partial order semantics for parametric time Petri nets as a
way to significantly enhance the result of an existing synthesis
algorithm.
Given a reference parameter valuation, our approach synthesizes other
valuations preserving, up to interleaving,
the behavior of the reference parameter valuation.
We show the applicability of our approach using acyclic asynchronous circuits.

Join work with Thomas Chatain and Étienne André.
Vendredi 17 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Des preuves, oui, mais formelles !
Description: Micaela MAYERO Dans cet exposé, très informel, lui, je parlerai de l'évolution des outils de preuves formelles ces 20, voire ces 30, dernières années. Nous nous appuierons sur quelques exemples afin de montrer comment les formalisations contribuent à la fois au développement de ces outils via des avancés théoriques majeurs ainsi qu'aux domaines qui s'engagent peu à peu dans leur utilisation. Suite à une première partie accessible à tout public, nous parlerons de la logique sous-jacente à l'un des système connaissant le plus d'avancées et de changements: Coq. Nous aborderons les évolutions de la théorie des types avec (im)prédicativité, la logique classique avec le choix de la totalité et d'autres avancées, pour finir, si nous avons le temps, par quelques mots sur CoqHoTT et l'axiome d'univalence.