Séminaire d'Alan Schmitt à l'INSA

Le 11 mai 2026

Alan Schmitt de l'INRIA Rennes (Skeletal semantics) donne un séminaire intitulé :  « Formaliser un langage de programmation avec accès mémoire et exceptions » le 11 mai 2026 à 11h (en salle GEI-13)
L'exposé se veut relativement accessible, il est ouvert aux étudiants.

Résumé : Il existe de nombreuses raisons pour chercher à définir précisément un langage de programmation : pour le documenter ou l’enseigner, pour spécifier des implémentations compatibles, pour prouver des programmes... 
 Formaliser un langage simple est plutôt facile. Mais dès que le langage implique des /effets/, comme une interaction avec des périphériques (mémoire, entrées/sorties) ou un flot de contrôle complexe (exceptions, continuations), les approches deviennent compliquées et peuvent dépendre de l'objectif recherché. Par exemple, on peut vouloir une représentation différente de la mémoire si l'on vise une implémentation ou si l'on cherche à prouver des programmes. Dans le premier cas, une approche impérative où l'on compile un accès mémoire par une lecture/écriture physique est efficace et immédiat. Dans le second cas, représenter l’interaction avec la mémoire dans le cadre d’une théorie équationnelle simplifie les preuves. 
 L’objectif de cet exposé est d’illustrer différentes approches pour formaliser ces effets, comme les monades ou les effets algébriques, ainsi que leurs avantages et inconvénients.

Contact : Didier Le Botlan