Lifo - Laboratoire d'Informatique Fondamentale d'orléans INSA Centre Val de Loire Université d'Orléans Université d'Orléans

Lifo > Les séminaires du LIFO

English Version



Contact

LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2

Email: contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37



Les séminaires du LIFO


Accès par année : 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018 2019 2020

Sauf exception, les séminaires se déroulent le lundi de 14h à 15h, Salle de réunion 1, bâtiment IIIA (voir plan du campus).


27/04/2020 : "Contact-Tracing" respecteux de la vie privée : utilité et sécurité
Benjamin Nguyen (LIFO) Résumé
Attention : Lieu : visioconférence

17/04/2020 : LMV visio : Kindly Bent to Free Us
Gabriel Radanne (IRIF) Résumé
Attention : Lieu : visioconférence

15/04/2020 : LMV visio : A Fast Verified Liveness Analysis in SSA form
Jean-Christophe Léchenet (IRISA) Résumé
Attention : Lieu : visioconférence

10/04/2020 : LMV visio : Les langages k-blocs déterministes
Clément Miklarz (LITIS) Résumé
Attention : Débute à 11 h. Lieu : visioconférence

08/04/2020 : LMV visio : Toward certified quantum programming
Christophe Chareton (LRI) Résumé
Attention : Lieu : visioconférence

06/04/2020 : LMV visio : Sémantiques quantitatives et développement de Taylor syntaxique
Jules Chouquet () Résumé
Attention : Lieu : visioconférence

01/04/2020 : LMV visio : Un monde distribué
Victor Allombert (Nomadic Labs) Résumé
Attention : Débute à 15 h. Lieu : visioconférence

30/03/2020 : LMV visio : Fibrations, Approximations and Intersection Type Systems
Luc Pellissier (LIX) Résumé
Attention : Lieu : visioconférence

09/03/2020 : Interactive mapping specification and repairing in the presence of policy views
Ugo Comignani (LIS) Résumé

02/03/2020 : Apprentissage par transfert : Etat de l’art et présentation d’une nouvelle méthode par boosting de traductions entre cible et source
Antoine Cornuéjols (AgroParisTech) Résumé

17/02/2020 : Ordonnancement d'un système de production industriel complexe : flow shop hybride avec des machines dédiées soumis à différentes contraintes temporelles
Houda Harbaoui (LIFO) Résumé

03/02/2020 : Loi de Programmation Pluriannuelle de la Recherche (LPPR)
Florent Becker (LIFO) Résumé

20/01/2020 : Confidentialité différentielle et Machine Learning
Vincent Thouvenot (Thales Group) Résumé

Résumés des séminaires


"Contact-Tracing" respecteux de la vie privée : utilité et sécurité Benjamin Nguyen, LIFO
En cette période d'épidémie, le traçage des contacts est une opération épidémiologique classique, réalisée manuellement. Des initiatives pour automatiser ce traçage ont vu le jour, basées sur le fait que beaucoup de personnes portent constamment sur eux un téléphone portable. Ces initiatives automatiques posent la question de la mise en balance de l'utilité et de l'efficacité de l'application par rapport à son côté intrusif et au risque d'atteintes à la vie privée des utilisateurs (dévoiler leurs contacts ou dévoiler leur statut infectieux). Afin d'éclairer le débat citoyen des membres du laboratoire, en vue du débat à l'assemblée sur ce thème le 28 avril prochain, nous proposons une présentation introductive à cette question. Nous discuterons de la problématique générale de la mise en place de tels systèmes, en particulier en décrivant certaines attaques, et présenter le fonctionnement de deux systèmes européens actuellement en cours d'élaboration : D3PT et ROBERT.


LMV visio : Kindly Bent to Free Us Gabriel Radanne, IRIF
Systems programming often requires the manipulation of resources like file handles, network connections, or dynamically allocated memory. Programmers need to follow certain protocols to handle these resources correctly. Violating these protocols causes bugs ranging from type mismatches over data races to use-after-free errors and memory leaks. These bugs often lead to security vulnerabilities. While statically typed programming languages guarantee type soundness and memory safety by design, most of them do not address issues arising from improper resource handling. Linear and affine types guarantee single-threaded resource usage, but they are rarely deployed as they are too restrictive for real-world applications. We present Affe, an extension of ML with constrained types that manages linearity and affinity properties through kinds. In addition Affe supports the exclusive and unrestricted borrowing of affine resources, inspired by features of Rust. Moreover, Affe retains the defining features of the ML family: an impure, strict functional expression language with complete principal type inference and type abstraction through modules. Our language does not require any linearity annotations in expressions and supports common functional programming idioms.


LMV visio : A Fast Verified Liveness Analysis in SSA form Jean-Christophe Léchenet, IRISA
Liveness analysis is a standard compiler analysis, enabling several optimizations such as deadcode elimination. The SSA form is a popular compiler intermediate language allowing for simple and fast optimizations. In 2008, Boissinot et al. designed a fast liveness analysis by combining the specific properties of SSA with graph-theoretic ideas such as depth-first search and dominance. We formalize their approach in the Coq proof assistant, inside the CompCertSSA verified C compiler. We also compare experimentally this approach on CompCert’s benchmarks with respect to the classic dataflow-based liveness analysis, and observe performance gains. This is a joint work with Sandrine Blazy and David Pichardie, and it will be presented in IJCAR 2020.


LMV visio : Les langages k-blocs déterministes Clément Miklarz, LITIS
Une expression rationnelle est 1-non-ambiguë si son automate des positions est déterministe, et un langage est 1-non-ambigu s’il peut être représenté par une expression 1-non-ambiguë. Brüggemann-Klein et Wood caractérisent cette propriété sur un langage en partant de son automate déterministe minimal et en appliquant une procédure : le BW-test. La famille des langages bloc-déterministes, étudiée par Giammarresi et al. puis par Han et Wood, est une extension de celle des langages 1-non-ambigus, où l’on utilise des mots à la place des lettres dans les expressions. Nous avons montré que certains résultats précédemment obtenus étaient erronés, et que d’autres avaient été incorrectement démontrés. Nous présenterons les premiers éléments de caractérisation de cette famille, sa hiérarchie propre par rapport à la taille maximum des blocs, et sa stricte inclusion dans les langages rationnels.


LMV visio : Toward certified quantum programming Christophe Chareton, LRI
While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Early attempts either suffer from the lack of automation or parametrized reasoning, or require the user to write specifications and algorithms far from those presented in research articles or textbooks, and as a consequence, no significant quantum algorithm implementation has been currently verified in a scale-invariant manner. We propose Q BRICKS , the first development environment for certified quantum programs featuring clear separation between code and proof, scale-invariance specification and proof, high degree of proof automation and allowing to encode quantum programs in a natural way, i.e. close to textbook style. This environment features a new domain-specific language for quantum programs, namely Q BRICKS -DSL, together with a new logical specification language QBRICKS -SPEC. Especially, we introduce and intensively build upon HOPS, a higher-order extension of the recent path-sum semantics, used for both specification (parametrized, versatile) and automation (closure properties). QBRICKS builds on best practice of formal verification for the classic case and tailor them to the quantum case. To illustrate the opportunity of Q-BRICKS, we implement the first scale-invariant verified implementations of non-trivial quantum algorithms, namely phase estimation (QPE) – the purely quantum part of Shor algorithm for integer factoring – and Grover search. It proves by fact that applying formal verification to real quantum programs is possible and should be further developed.


LMV visio : Sémantiques quantitatives et développement de Taylor syntaxique Jules Chouquet,
Les sémantiques quantitatives permettent d’étudier certaines propriétés des langages de programmation, qui peuvent, selon les modèles, être relatives à la normalisation, au temps de calcul, aux probabilités… Dans ces sémantiques (espaces de finitude, espaces cohérents probabilistes, modèle relationnel pondéré…) il existe une corrélation entre les propriétés globales des programmes et la possibilité de décomposer ces derniers à l’aide d’approximations, de dérivations. Le développement de Taylor syntaxique est un outil qui permet de tisser ce lien entre l’approximation et la sémantique, et c’est la construction sur laquelle porteront notamment les raisonnements visant à établir la correction des modèles quantitatifs. Nous présentons des résultats de la sorte pour le développement de Taylor appliqué à Call-By-Push-Value, un langage de haut niveau permettant d’encoder plusieurs stratégies d’évaluation, et nous montrerons le lien entre cette sémantique et la Logique Linéaire de Girard.


LMV visio : Un monde distribué Victor Allombert, Nomadic Labs
Il existe une grande diversité de plateformes programmables. Que l'on parle de machines physiques (multi-cœurs, accélérateurs graphiques, FPGA, …), d'architectures abstraites (cloud, iot, …) ou même de plateformes d'exécution (blockchains via smart contracts), ces différentes plateformes doivent pouvoir évoluer dans un environnement hétérogène et souvent distribué. Bien que différente, la programmation de ces entités nécessite abstraction et rigueur afin de garantir des interactions correctes menant au résultat attendu, tout en garantissant une bonne efficacité. Pour ce faire, il est nécessaire d'identifier l'essence de ces interactions et d'en modéliser le comportement afin de garantir des propriétés fortes. C'est avec des cas d'utilisation concrets que nous illustrerons différentes approches.


LMV visio : Fibrations, Approximations and Intersection Type Systems Luc Pellissier, LIX
We present calculi (intuitionistic or classical) in a bioperadic setting, and, following Melliès and Zeilberger (2015), represent type systems as morphisms of such structure. Programs in such calculi can be approximated arbitrarily well by linear programs, that use their argument exactly once. In this work, we show that such linear approximations give rise, through an adapted Grothendieck construction, to intersection type systems for any logical system that can be embed meaningfully into linear logic. We recover in this way all well-known intersection type systems, capturing different notions of normalization for various languages — λμ-calculus, System L — and give a blueprint to compute new ones. Based on “Polyadic Approximations, Fibrations and Intersection Types“, Mazza, Pellissier and Vial, POPL 2018.


Interactive mapping specification and repairing in the presence of policy views Ugo Comignani, LIS
Data exchange between sources over heterogeneous schemas is an ever-growing field of study with the increased availability of data, oftentimes available in open access, and the pooling of such data for data mining or learning purposes. However, the description of the data exchange process from a source to a target instance defined over a different schema is a cumbersome task, even for users acquainted with data exchange. In this presentation, I will address the problem of allowing a non-expert user to specify a source-to-target mapping. To do so, I will describe the foundations of an interactive process in which users provide small examples of their data, and answer simple boolean questions in order to specify their intended mapping. The first contribution is a formal definition of the problem of interactive mapping specification, as well as a formal resolution process for which desirable properties are proved. Then, based on this formal resolution process I will describe how practical algorithms can be designed in order to reduce the number users interactions. Especially, I will describe how to make use of quasi-lattice structures to order the set of possible mappings to explore, and efficiently prune the space of explored mappings. Then, I will show how this pruning can be improved by extending the approach to the use of integrity constraints. Finally, I will present some experimental results over the open source prototype built from the described framework.


Apprentissage par transfert : Etat de l’art et présentation d’une nouvelle méthode par boosting de traductions entre cible et source Antoine Cornuéjols, AgroParisTech
L’apprentissage par transfert consiste à ré-utiliser ce qui a été appris sur une tâche source afin d’apprendre plus vite et/ou mieux à résoudre une tâche cible. Ce type d’apprentissage connaît un spectaculaire regain d’intérêt depuis l’émergence des réseaux de neurones profonds. Ceux-ci sont en effet très coûteux à entraîner et il paraît avantageux d’utiliser un réseau déjà appris sur une tâche « proche ». Cet exposé situera d’abord les différents types d’apprentissage par transfert. En sélectionnant quelques travaux récents, il donnera un aperçu de l’état de l’art et des approches privilégiées actuellement. Dans une deuxième partie, l’exposé présentera une approche originale de l’apprentissage par transfert supervisé, appelée TransBoost. Cette approche s’appuie sur l’apprentissage de traductions « faibles » entre la cible et la source. L’analyse des propriétés de cette méthode conduit à revisiter les conditions d’un apprentissage par transfert réussi.


Ordonnancement d'un système de production industriel complexe : flow shop hybride avec des machines dédiées soumis à différentes contraintes temporelles Houda Harbaoui, LIFO
L'accroissement des profits, à travers l'amélioration de la productivité et la réduction des pertes de matières, représente un objectif primordial pour les entreprises industrielles. Dans cette thèse, nous nous intéressons à la résolution d'un problème industriel complexe réel avec des contraintes de temps. Nous nous sommes intéressés, tout d'abord, à un objectif principal, soit la minimisation des dates de fin de production, suivi d'un objectif secondaire qui est la minimisation des quantités de déchets non recyclables. Dans un premier temps, nous avons modélisé le problème par des modèles mathématiques, que nous avons résolu à l'aide d'un solveur. Dans un second temps, nous avons proposé une méthode approchée en forme d'algorithmes évolutionnistes. Cette méthode est appliquée aux deux objectifs mentionnés ci-dessus séparément. Une troisième méthode est ensuite appliquée à l'objectif principal, à savoir une méthode arborescente approchée. Nous avons testé les algorithmes proposés sur des instances inspirées d'un cas réel ; issues d'une entreprise du secteur agroalimentaire et sur des instances inspirées de la littérature. Dans cette présentation, on va se limiter à présenter la modélisation mathématique du problème et à la présentation de la méthode approchée (algorithme génétique hybride) Dans cette présentation, après avoir présenté le problème industriel, nous présenterons sa modélisation mathématique et la première méthode de résolution soit un algorithme génétique hybride.


Loi de Programmation Pluriannuelle de la Recherche (LPPR) Florent Becker, LIFO
La loi de programmation pluriannuelle de la recherche sera présentée au parlement à partir de février. Elle veut définir un cadre pluriannuel pour la politique de recherche. Il s'agit ainsi de déterminer à l'avance le budget consacré à la recherche. Des groupes de travail, réunis en 2019 ont produit des documents qui ont servi de base pour la rédaction du texte de cette loi. Certaines mesures qu'elle contiendra ont déjà été annoncées par le gouvernement. La politique qui en découle veut: - Renforcer la capacité de financement des projets, programmes et laboratoires de recherche ; - Conforter et renforcer l'attractivité des emplois et des carrières scientifiques ; - Consolider la recherche partenariale et le modèle d'innovation français ; - En nous appuyant sur les textes des groupes de travail, les annonces gouvernementale ainsi que les analyses faites au sein de la communauté académique (laboratoires, section CNU, revues…), nous présenterons le contexte de cette loi et de son élaboration, les pistes explorées et annoncées pour répondre à ces enjeux, et ce qu'elles signifient pour les collègues (statut, service d'enseignement, recrutement…), les laboratoires tels que le lifo (financement et orientation de la recherche), des universités telles qu'Orléans. Nous analyserons le modèle de recherche qui est proposé, et ses effets pour les personnels et la société.


Confidentialité différentielle et Machine Learning Vincent Thouvenot, Thales Group
Smartphone, carte d'abonnement, compteur intelligent énergétique, etc., les sources de données personnelles sont nombreuses. Si ces données peuvent apporter des fortes valeurs ajoutées, que ce soit aux citoyens, aux collectivités ou aux entreprises, celles-ci doivent être protégées. La réglementation autour de la donnée personnelle évolue et se renforce (voire la RGPD). L'anonymisation des données peut être utilisée pour les protéger. La confidentialité différentielle est une propriété mathématiques que l'on cherche à imposer à des mécanismes de bruitage appliqués pour protéger les individus. Dans cette présentation, après avoir défini les principes de base de la confidentialité différentielle, nous présenterons des exemples de l'Etat de l'Art sur son application en Machine Learning.