Calculer avec la Sémantique Quantitative – CoQuaS

Le projet porte sur les fondations théoriques des méthodes formelles,
notamment celles basées sur l'analyse statique (sémantique, systèmes
des types), garantissant la validation et la vérification de logiciels.

La sémantique quantitative est l’objet d’une activité de recherche
féconde :
sémantiques vectorielles, extensions différentielles de la logique linéaire,
lambda-calculs algébriques et sensibles aux ressources. S'ensuivent de
nouvelles interactions entre l’algèbre linéaire et les méthodes formelles en
informatique et un renouveau du cadre théorique de la sémantique
dénotationnelle.

Il est grand temps d'appliquer cette approche à l’une des questions
fondamentales de l’informatique : décrire ce que calculent les programmes, et
comment ils le calculent, en faisant abstraction des détails de la syntaxe.
Notre but est de produire des exemples concrets illustrant le
renouveau apporté par les sémantiques quantitatives dans l’étude du calcul.

Nous proposons un projet « Jeunes Chercheuses et Jeunes Chercheurs », dont les
objectifs finaux sont précis et clairement formulés. Nous prévoyons d’obtenir
deux résultats importants, témoignant de la pertinence de la sémantique
quantitative pour l’étude du calcul :
— une description sémantique de l’information intentionnelle attachée au coût
calculatoire (par exemple la complexité en espace et en temps, cf. la
« Milestone 3.1 » du projet scientifique) ;
— une approche dénotationnelle de la programmation fonctionnelle quantique
d’ordre supérieur (cf. la « Milestone 3.2 ») ;

Ces deux buts sont ambitieux, et les atteindre permettrait de combler des
lacunes importantes de la littérature actuelle (cf. la tâche 3, pour plus de
détails). Leur résolution nécessite d’associer une signification mathématique à
la notion informatique de ressource non duplicable. La sémantique quantitative
établit cette notion à partir de la linéarité algébrique.

Le projet sera développé au sein de l’équipe « Logique, Calcul et Raisonnement »
(LCR) du LIPN, dont sont issus trois des cinq participants de la proposition.
Parmi les principaux thèmes de recherche de LCR se retrouvent la théorie de la
démonstration en logique linéaire, la programmation fonctionnelle et la
complexité implicite. Nous sommes convaincus que la sémantique quantitative s’y
insérera parfaitement en tant que nouvel axe de recherche, enrichissant ainsi
son activité de recherche tout en bénéficiant de l’expertise déjà présente. De
plus, cela permettra peut-être de renforcer les interactions de LCR avec le
domaine de la combinatoire algébrique qui est un autre thème majeur du LIPN.