https://www.ins2i.cnrs.fr/fr/cnrsin...
Il y a un besoin toujours très important dans le développement, la conception et la sémantique des langages de programmation, qui fournissent des abstractions les plus adaptées possibles à leur contexte d’utilisation. Ceci est notamment utile pour la production de compilateurs et d’outils de vérification mécanisée. On peut par exemple penser à des langages de programmation comme Rust qui possède une gestion de la mémoire sûre mais néanmoins optimisée et qui peut ainsi viser des applications de la programmation système ou à des langages dédiés au parallélisme permettant de passer d’une spécification déterministe à un code embarqué cible pouvant s’exécuter sur des architectures parallèles (multi-cœurs). Dans la plupart des cas, ces abstractions sont obtenues grâce à la conception de nouveaux systèmes de types, dont les propriétés sont prouvées et leur exploitation nécessite le développement de techniques modernes de compilation et de vérification qui permettent d’obtenir un code sûr et efficace. Ces thématiques de recherche sont activement développées dans les communautés qui publient dans les conférences telles que POPL, PLDI, ICFP, OOPSLA ou ECOOP.
