Avec le développement des dispositifs d'interaction, en particulier tactiles, les systèmes interactifs se multiplient. Les systèmes critiques n'échappent pas à cette règle. Ainsi, les cockpits, autrefois tangibles et mécaniques, embarquent maintenant des tablettes tactiles, des écrans numériques et autres dispositifs interactifs. Pour accompagner cette multiplication des systèmes interactifs critiques, il est nécessaire que les langages supportant le développement de ces systèmes d'une part soient dédiés à la création de tels systèmes et d'autre part apportent des garanties sur les systèmes développés, notamment dans leur processus de compilation. Ce n'est pas le cas actuellement.   Les UIDLs sont des langages dédiés au développement de systèmes interactifs. Leur utilisation pour le développement de systèmes critiques est de plus en plus répandue, ainsi il est nécessaire de leur donner un fondement théorique solide afin de pouvoir apporter des garanties sur leur compilation et leur exécution. Dans de précédents travaux, nous avons montré que la théorie des bigraphes, définie par Robin Milner dans les années 2000, était particulièrement adaptée pour exprimer la sémantique des UIDLs. Nous avons également défini un UIDL minimal formel à l'aide des bigraphes. Un bigraphe est un graphe qui permet de représenter à la fois des notions de localité (d'imbrication de composants les uns dans les autres) et de liens causaux (permettant de décrire des réactions en chaîne) au travers de deux sous-graphes. On peut ensuite décrire des évolutions de ces bigraphes (selon des évènements par exemple) via des règles de réaction qui décrivent comment transformer une sous-partie d'un bigraphe si certaines conditions sont respectées. On appelle système réactif bigraphique un bigraphe et les règles de réaction qui décrivent sa dynamique. Pour pouvoir aller plus loin et raisonner formellement sur cet UIDL minimal (à la fois pour apporter des garanties sur la compilation et vérifier des propriétés), il est nécessaire de formaliser la théorie des bigraphes dans un assistant de preuve. Pour pouvoir ensuite nous insérer dans des écosystèmes tels que CompCert (un compilateur vérifié pour le langage C), nous avons choisi d'utiliser l'assistant de preuve Coq, et avons formalisé la partie structurelle (statique) des bigraphes et montré que notre formalisation est correcte.   Le travail de cette thèse consiste à compléter l'implémentation des bigraphes dans Coq en ajoutant les aspects dynamiques (les règles de réaction) puis à instancier notre formalisation pour définir notre UIDL formel. Ce travail sera divisé en 4 parties : 1. Compléter l'implémentation des bigraphes dans Coq pour permettre le pattern matching 2. Implémenter la définition des règles de réaction pour permettre la définition d'un système réactif bigraphique à l'aide du pattern matching 3. Instancier cette formalisation pour définir notre UIDL formel dans Coq 4. Prouver sur ce modèle formel les propriétés sur les UIDLs formels   En plus de ces tâches liées à la recherche, il sera également possible d'effectuer des enseignements à l'ENAC (avec complément de salaire). ·        Bac +5 en informatique ·        Notions en méthodes formelles, idéalement en Coq, ou au moins une forte appétence pour la théorie et la preuve de programme ·        Notions en compilation ·       Bon niveau d'anglais (lu, écrit, parlé)