Résumé : Une sémantique dénotationelle interprète les types de données (comme Bool ou Int) par des espaces mathématiques (posets, treillis, structures algébriques) et les programmes par des fonctions sur ces espaces. L'intérêt d'une telle interprétation étant de donner une description du comportement opérationnel des programmes qui fait abstraction du langage dans lequel les programmes sont écrits. Les sémantiques quantitatives sont en particulier les sémantiques dénotationelles issues de la logique linéaire, où les types de données sont interprétés par des espaces vectoriels (ou, plus généralement, des modules), les programmes qui utilisent exactement une fois leurs données d'entrée deviennent des fonctions linéaires (au sens algébrique), alors que les programmes qui utilisent leurs ressources un nombre indéterminé de fois (comme les programmes récursifs ou les programmes utilisant l'instruction while, par exemple) sont interprétés par des fonctions analytiques, approximables par des polynômes, qui représentent des calculs partiels. Ces sémantiques sont particulièrement naturels pour décrire des programmes non-déterministes, voire probabilistes ou quantiques, l'addition exprimant une sorte de superposition des états élémentaires et les scalaires associant une estimation quantitative à une telle superposition. Dans cet exposé, je chercherai à donner une intuition de l'interprétation des programmes via quelques exemples de sémantiques quantitatives et à donner un aperçu des résultats récemment obtenus, en particulier dans le cadre des langages fonctionnels probabilistes.

Dernière modification : Monday 27 May 2024

Contact pour cette page : Cyril.Banderier at lipn.univ-paris13.fr