Compilation Formellement Vérifiée d'un Langage de Programmation Orienté Interaction

Topic description Avec la démocratisation des appareils interactifs, les utilisateurs s'attendent désormais à interagir avec leurs systèmes par le biais d'interactions tactiles et avancées. Pour faciliter la mise en œuvre de ces systèmes, des langages de programmation dédiés « orientés interaction » ont été proposés. Ces langages permettent de décrire efficacement à la fois l'apparence du système et son comportement interactif. Ils sont de plus en plus populaires, y compris pour le développement de systèmes critiques. Cependant, peu d'efforts ont été consacrés à la formalisation de ces langages, de leur sémantique ou de leur modèle d'exécution. L'objectif de ce projet de recherche est de formaliser Smala, un langage orienté interaction développé à l'ENAC. Smala est un langage réactif, dans lequel le programmeur spécifie la façon dont les événements extérieurs sont propagés et dont le programme réagit, en mettant à jour son état interne et en déclenchant des comportements observables. Ce programme déclaratif de haut niveau peut ensuite être compilé en code impératif qui implémente ces réactions. Au cours de ce projet, le candidat formalisera le langage et sa sémantique, et implémentera sa compilation vers le langage de bas niveau C. Une partie importante du travail sera consacrée à la vérification de bout en bout du schéma de compilation : le candidat développera une preuve mécanisée que le programme C généré implémente bien le comportement spécifié par le programme source Smala. Pour ce faire, le candidat utilisera principalement l'assistant de preuves interactif Rocq. En effet, celui-ci comprend des fonctionnalités pour la spécification (de la sémantique de Smala), l'écriture de programmes (le schéma de compilation en tant que programme purement fonctionnel) et les preuves vérifiées automatiquement (relant cette sémantique, la fonction de compilation et la sémantique du C telle que spécifiée dans le projet CompCert).------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------With the democratization of interactive devices, users now expect to interact with their systems through tactile and advanced interactions. To facilitate the implementation of these systems, dedicated ”interaction-oriented” programming languages have been proposed. These languages can efficiently describe both the appearance of the system and the interactive behavior. They are becoming more popular, including for the development of critical systems. However, there has not yet been a lot of effort in formalizing these languages, their semantics or their execution model. The goal of this research project is to formalize Smala, an interaction-oriented language developped at ENAC. Smala is, at its core, a reactive language, where bindings written by the programmer specify how outside events are propagated, and how the program reacts by updating its internal state and trigger observable behaviors. This high-level, declarative program can then be compiled into imperative code that implements these reactions. During this project, the candidate will formalize the language and its semantics, and implement its compilation into the low-level language C. A significant amount of work will be dedicated to the end-to-end verification of the compilation scheme: the candidate will develop a mechanized proof that the generated C program does implement the behavior specified by the source Smala program. To do so, the candidate will use the Rocq prover as a primary tool. Indeed, it includes facilities for specification (of Smala's semantics), writing programs (the compilation scheme as a purely functional program), and automatically-checked proofs (relating these semantics, the compilation function, and the semantics of C as specified in the CompCert project).------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------Début de la thèse : 01/10/ Funding category Funding further details Concours de l'École Doctorale