<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">\documentclass[10pt]{amsart}
\usepackage{a4}
\usepackage[margin=2.5cm]{geometry}

\usepackage[usenames,dvipsnames]{xcolor}
\usepackage{hyperref}
\hypersetup{colorlinks=true,citecolor=OliveGreen,urlcolor=NavyBlue}

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[english,french]{babel}

\renewcommand{\textsc}[1]{#1}
\usepackage[backend=biber,%
  style=alphabetic,%
  url=false,%
  sorting=ynt,%
  maxbibnames=99,%
]{biblatex}
\addbibresource{projet.bib}
\renewbibmacro{in:}{}
\AtEveryBibitem{\clearfield{month}}
\AtEveryBibitem{\clearfield{school}}
\DefineBibliographyStrings{french}{phdthesis = {ThÃ¨se}}

%"[]": do not repeat on other pages
\title[]{Projet de recherche:\\
  Techniques formelles pour aider la programmation}
\author[]{Gabriel Scherer}

\newcommand{\XXX}[2][]
    {\begingroup {\def \@test{#1}\ifx #1\empty\else \color{red}
      [\emph {#1}]\space \fi \color{blue}$\langle$~\textbf{#2}~$\rangle$}\endgroup}

\begin{document}

\maketitle

Une partie importante de la recherche en sciences du logiciel se
concentre sur la question de la \emph{vÃ©rification}: comment prouver
qu'un programme correspond Ã&nbsp; sa spÃ©cification ?

J'aimerais me consacrer Ã&nbsp; un problÃ¨me complÃ©mentaire : comment
utiliser les outils formels dÃ©veloppÃ©s dans la communautÃ© des langages
de programmation et ses voisines (thÃ©orie de la dÃ©monstration,
logique, et dÃ©monstration automatique) pour \emph{aider} l'Ã©criture de
programmes, en dÃ©veloppant des outils et langages qui rendent la
programmation plus aisÃ©e, plus concise, et rÃ©duisent les risques
d'erreurs ?

Je propose trois axes principaux:
\begin{enumerate}
\item L'Ã©tude de reprÃ©sentations canoniques des programmes dans des
  systÃ¨mes de types avancÃ©s.
  %
  Pour ce faire, je compte continuer Ã&nbsp; explorer le lien entre thÃ©orie
  de la dÃ©monstration, et en particulier le \emph{focusing}, et les
  langages de programmation. J'ai proposÃ© dans ma thÃ¨se la technique
  de \emph{saturation} qui Ã©tend le \emph{focusing} pour obtenir des
  formes canoniques pour le $\lambda$-calcul simplement typÃ©. Comment
  Ã©tendre cette saturation aux types polymorphes et dÃ©pendants?
  %
  J'espÃ¨re obtenir comme rÃ©sultat pratique un outil de synthÃ¨se de
  fragments de programmes dirigÃ© par les types, mÃªme des types riches.

\item L'Ã©laboration de procÃ©dures de dÃ©cision d'Ã©quivalence de
  programmes, et l'exploration des nouveaux outils et constructions de
  programmation qu'elles rendent possibles. J'espÃ¨re obtenir comme
  rÃ©sultat pratique des outils de vÃ©rification des restructurations de
  code (\emph{refactoring}), lÃ©gers et faciles d'emploi, qui
  augmentent donc la confiance et le confort des programmeurs.

\item Un travail thÃ©orique et pratique sur la conception de systÃ¨mes
  de programmation multi-langages avec des garanties formelles de
  bonne inter-opÃ©rabilitÃ©, et donc d'utilisabilitÃ© et de
  sÃ»retÃ©. J'aimerais pouvoir prendre un langage monolithique, le
  transformer en un systÃ¨me langages sÃ©parÃ©s conÃ§us pour interagir
  harmonieusement les uns avec les autres, et obtenir ainsi un
  meilleur systÃ¨me de programmation, plus simple Ã&nbsp; utiliser, et plus
  simple Ã&nbsp; faire Ã©voluer.
\end{enumerate}

La vÃ©rification et l'aide Ã&nbsp; la programmation par mÃ©thodes formelles
sont fortement complÃ©mentaires. Les approches de vÃ©rification -- par
exemple la preuve de programme, les types dÃ©pendants, la vÃ©rification
d'invariants logiques, le \emph{model-checking} ou les tests --
demandent Ã&nbsp; l'utilisateur de fournir des informations supplÃ©mentaires
qui constituent une \emph{spÃ©cification}, totale ou partielle, du
programme, et qui restreignent donc l'espace des programmes
possibles. Plus on a d'information sur le programme, plus l'espace
Ã&nbsp; explorer est restreint, plus ces outils d'aide Ã&nbsp; la programmation
peuvent Ãªtre efficaces. (On peut voir les systÃ¨mes de types puissants
comme une version plus gÃ©nÃ©raliste des contraintes structurelles
fortes imposÃ©es par l'expression ou le modelage de programme par des
automates ou leurs variantes Ã©tendues.)

Ã€ l'inverse, la programmation certifiÃ©e avec spÃ©cifications avancÃ©es
est aujourd'hui difficile d'utilisation et rÃ©servÃ©e aux experts; de
nouveaux outils d'aide Ã&nbsp; la programmation permettront d'espÃ©rer et de
rÃ©clamer non seulement un gain en sÃ»retÃ©, mais aussi en confort de
programmation. Ils pourraient alors jouer un rÃ´le important dans
l'adoption Ã&nbsp; plus grande Ã©chelle des mÃ©thodes de programmation
vÃ©rifiÃ©e.

Par exemple, j'ai Ã©tudiÃ© pendant ma thÃ¨se la question de dÃ©cider si un
type a un habitant unique (tous les programmes possibles Ã&nbsp; ce type
sont Ã©quivalents), et montrÃ© qu'on retrouve de tels types dans des
bibliothÃ¨ques logicielles utilisÃ©es en pratique, ce qui promet des
applications Ã&nbsp; la synthÃ¨se de programmes dirigÃ©e par les types. Cela
n'aurait pas Ã©tÃ© envisageable dans un langage moins typÃ©, par exemple
oÃ¹ les donnÃ©es sont reprÃ©sentÃ©es par des entiers -- un type aux
habitants pas du tout uniques. C'est grÃ¢ce Ã&nbsp; l'utilisation de types
plus informatifs, les types \emph{abstraits} -- introduits au dÃ©part
pour la sÃ»retÃ© et la modularitÃ© -- que les langages fonctionnels typÃ©s
rendent rÃ©aliste la synthÃ¨se de programme dirigÃ©e par les types.

\section{Focusing et langages de programmation}

La correspondance de Curry-Howard entre preuves et programmes est
maintenant bien connue et a donnÃ© pendant des dÃ©cennies de beaux
rÃ©sultats thÃ©oriques et pratiques, cÃ´tÃ© logique
(meilleure comprÃ©hension calculatoire de rÃ¨gles logiques), cÃ´tÃ©
programmation (``\emph{theorems for free}''), et dans des domaines
mixtes comme les assistants de preuve Ã&nbsp; base de type dÃ©pendants.

Il existe aussi une communautÃ© qui voit la recherche de preuve
(dans une logique bien choisie) comme une forme de calcul
correspondant prÃ©cisÃ©ment Ã&nbsp; la \emph{programmation logique},
popularisÃ©e par le langage Prolog.

Mais la communautÃ© des langages fonctionnels s'est concentrÃ©e sur le
lien entre exÃ©cution des programmes et rÃ©duction/simplification des
preuves, passant Ã&nbsp; cÃ´tÃ© d'une observation qui a Ã©tÃ© centrale Ã&nbsp; mes
travaux de thÃ¨se: la structure de la \emph{recherche} de preuve nous
renseigne sur la structure des programmes (en forme normale). On peut
voir tout programme fonctionnel comme une preuve, et donc le rÃ©sultat
d'un processus de recherche; mieux comprendre la structure de cette
recherche, par exemple par le \emph{focusing}, permet de mieux
comprendre les programmes, comment les reprÃ©senter et manipuler.

\subsection{Saturer les types riches}

J'ai transposÃ© pendant ma thÃ¨se la notion de \emph{focusing} de la
thÃ©orie de la dÃ©monstration aux langages de programmation, et ai
obtenu, en ajoutant la notion de \emph{saturation}, une reprÃ©sentation
canonique des programmes utilisant des types dits ``simples'',
reprÃ©sentants les types de donnÃ©es usuels en programmation :
fonctions, paires, sommes disjointes. J'ai pu montrer ainsi que des
types simples dont les habitants sont uniques apparaissent dans des
programmes typÃ©s existants.

Mais les types \emph{simples} que mon algorithme peut gÃ©rer ne font
que dÃ©crire les structures de donnÃ©es; il existe d'autres types dans
les langages typÃ©s modernes, en particulier les types
\emph{polymorphes} qui expriment la gÃ©nÃ©ricitÃ© et les types
\emph{dÃ©pendants} qui peuvent exprimer des spÃ©cifications
mathÃ©matiques.

Une notion de forme canonique qui prendrait aussi en compte ces types
riches serait nÃ©cessaire Ã&nbsp; une application Ã&nbsp; plus grande Ã©chelle de
cette technique pour la synthÃ¨se de programmes -- et permettrait aussi
d'appliquer cette technique Ã&nbsp; des types plus fins, et donc plus
souvent Ã&nbsp; habitants uniques.

C'est un projet ambitieux qui comporte des obstacles scientifiques
Ã&nbsp; surmonter. La dÃ©cidabilitÃ© de l'Ã©quivalence de types en prÃ©sence du
type vide, rÃ©sultat obtenu pendant mon post-doc en utilisant le
\emph{focusing} et la \emph{saturation}, Ã©tait restÃ© un problÃ¨me
ouvert connu depuis au moins 1995. Nous espÃ©rons que cette nouvelle
approche permettra aussi des avancÃ©es importantes pour les types
riches.

PremiÃ¨re difficultÃ©, l'indÃ©cidabilitÃ©. Dans un systÃ¨me avec
polymorphisme, trouver un habitant correspond Ã&nbsp; la recherche de preuve
dans des logiques d'ordre supÃ©rieur: l'existence d'un habitant, et
d'autant plus son unicitÃ©, deviennent indÃ©cidables. D'un algorithme
qui termine sur tous les types simples, on passerait Ã&nbsp; une procÃ©dure
partielle rÃ©pondant parfois ``je ne sais pas'' -- ce qui ne
l'empÃªcherait pas d'Ãªtre trÃ¨s utile aux programmeurs dans les cas oÃ¹
elle sait, tout comme un solveur SAT ou SMT peut exploser sur
certaines requÃªtes mais reste un outil prÃ©cieux dans les cas courants.

Une autre difficultÃ© provient de la \emph{paramÃ©tricitÃ©}, une garantie
sÃ©mantique apportÃ©e par les types polymorphes, souvent prÃ©sentÃ©e sous
l'angle des ``\emph{theorems for free}''. Par exemple, une fonction
gÃ©nÃ©rique en le type de son entrÃ©e ne peut pas faire d'hypothÃ¨se sur
ce type et ne peut donc pas inspecter la valeur de cette entrÃ©e. On
peut ainsi prouver qu'une fonction de type
$\forall \alpha, \alpha \to \alpha$, dans un langage totalement
fonctionnel, ne peut Ãªtre que la fonction identitÃ©. Mais aujourd'hui
on ne sait pas, dans le cas gÃ©nÃ©ral, remplacer le raisonnement
sÃ©mantique sur la paramÃ©tricitÃ© par une approche syntaxique permettant
l'automatisation par un algorithme -- pour
$\forall \alpha, \alpha \to \alpha$ on peut faire manuellement une
recherche de forme normale, mais comment gÃ©nÃ©raliser de faÃ§on uniforme
Ã&nbsp; tous les types ?

Une autre formulation du mÃªme problÃ¨me, plus formelle, est la
suivante. On sait que pour les systÃ¨mes de types simples,
l'Ã©quivalence observationelle, dÃ©finie sÃ©mantiquement, correspond Ã&nbsp; la
relation de $\beta\eta$-Ã©quivalence dÃ©finie syntactiquement. En
prÃ©sence de polymorphisme, la relation de $\beta\eta$-Ã©quivalence est
strictement plus faible que l'Ã©quivalence observationelle. Est-il
possible de proposer une Ã©quivalence syntactique plus forte ?

TroisiÃ¨me difficultÃ© Ã&nbsp; Ã©tudier, le \emph{focusing} est exprimÃ© par les
logiciens en utilisant le \emph{calcul des sÃ©quents}, une prÃ©sentation
des preuves qui ne correspond pas directement aux termes des langages
fonctionnels. On comprend bien comment passer de l'un Ã&nbsp; l'autre en
prÃ©sence de types simples et de polymorphisme, mais la combinaison du
calcul des sÃ©quents et des types dÃ©pendants, en prÃ©sence de sommes,
pose des problÃ¨mes thÃ©oriques non rÃ©solus, comme expliquÃ© dans
\cite{herbelin-hdr} -- sans les sommes, voir par exemple
\cite{sequents-PTS} pour un calcul des sÃ©quents dÃ©pendant
focalisÃ©. (Ã‰tienne Miquey, doctorant dans l'Ã©quipe PPS du laboratoire
IRIF, a fait un travail sur le sujet trÃ¨s prometteur mais pas encore
publiÃ©.)

\subsection{Saturation et rÃ©-Ã©criture}

Un besoin important pour utiliser la recherche de reprÃ©sentations
canoniques est de pouvoir faire une recherche modulo certaines
hypothÃ¨ses supplÃ©mentaires. Par exemple, en prÃ©sence de deux variables
$x, y : A$ et d'une fonction $r : A \to A \to \mathtt{Bool}$ inconnue,
l'espace des formes canoniques Ã&nbsp; un type $B$ est fortement simplifiÃ©
si on ajoute l'hypothÃ¨se que $r$ est une relation symÃ©trique,
$r(x,y) = r(y,x)$.

De faÃ§on gÃ©nÃ©rale on peut vouloir Ã©numÃ©rer les fragments de programme
canoniques modulo une famille d'Ã©quations sur les variables libres
utilisÃ©es par ces fragments -- supposer qu'un paramÃ¨tre est une loi de
groupe, par exemple. Une restriction naturelle est de supposer les
Ã©quations orientÃ©es en un systÃ¨me de rÃ©-Ã©criture. Mais les termes
prÃ©sents dans ces Ã©quations, fournies par l'utilisateur, ne sont pas
en forme focalisÃ©e: comment les reconnaÃ®tre efficacement pendant le
processus de recherche des formes focalisÃ©es ?

\subsection{SynthÃ¨se de programmes arbitraires}

Quand j'ai commencÃ© mes travaux de thÃ¨se, la question de la recherche
de programmes dirigÃ©e par les types avait Ã©tÃ© relativement peu
Ã©tudiÃ©e. Elle a fait l'objet d'un regain d'intÃ©rÃªt ces derniÃ¨res
annÃ©es, avec en particulier les travaux parallÃ¨les de Peter-Michael
Osera Ã&nbsp; UPenn et ses collaborateurs Ã&nbsp; Princeton \cite{osera1,osera2},
et des travaux indÃ©pendants au MIT \cite{mit}. Leur approche n'est pas
de se restreindre au cas non-ambigu oÃ¹ le type dÃ©termine uniquement le
fragment de programme, mais de demander des tests Ã&nbsp; l'utilisateur et
de s'arrÃªter au premier programme qui les passe.

MÃªme dans ce cadre, obtenir des reprÃ©sentations plus canoniques est
crucial : la recherche par \emph{force brute} de programmes se heurte
vite Ã&nbsp; une explosion combinatoire, mÃªme sur des petites tailles, et
toutes les idÃ©es sont bonnes pour restreindre la redondance parmi les
programmes. Les premiers travaux de Osera \cite{osera1} prÃ©sentaient
d'ailleurs des heuristiques trouvÃ©es en tÃ¢tonnant, qui sont en fait
des cas particuliers de la structure imposÃ©e par le
\emph{focusing}. J'ai pris contact avec ce groupe pendant mon
post-doc; leur proposer les termes focalisÃ©s saturÃ©s comme base de
recherche pourrait conduire Ã&nbsp; une collaboration intÃ©ressante.

\section{Ã‰quivalence de programmes}

Les outils de preuve automatique ont fait d'Ã©normes progrÃ¨s et sont
maintenant utilisÃ©s dans de nombreux domaines, dont la vÃ©rification de
programmes et les sciences du logiciel en gÃ©nÃ©ral -- des techniques de
recherche de preuve puissantes sont aussi utilisÃ©es, par exemple, pour
les bases de donnÃ©es ou les ontologies. On a donc des approches
fructueuses, et beaucoup d'implÃ©mentations utilisÃ©es en pratique, pour
vÃ©rifier automatiquement qu'un programme rÃ©pond Ã&nbsp; une
spÃ©cification. Comparativement, il y a eu peu de travail sur la
vÃ©rification automatique que deux programmes sont Ã©quivalents : les
types sommes rendent la thÃ©orie dÃ©licate et sont rencontrÃ©s trÃ¨s vite
en pratique. Par exemple, un boolÃ©en est un type somme, et dÃ©placer un
test plus tÃ´t ou plus tard dans un programme correspond Ã&nbsp; une
opÃ©ration dite d'$\eta$-expansion dont la justification est
non-triviale. Les progrÃ¨s accomplis pendant ma thÃ¨se et mon post-doc
devraient permettre de passer ces difficultÃ©s.

J'aimerais implÃ©menter en pratique des outils de test d'Ã©quivalence
pour des programmes fonctionnels et Ã©valuer leur applicabilitÃ©. C'est
un problÃ¨me qui est infaisable (\emph{intractable}) dans le cas
gÃ©nÃ©ral, et qui pourrait donc ne rien donner. Mais on peut espÃ©rer des
applications concrÃ¨tes quand on sait que les deux programmes Ã&nbsp; tester
ne sont pas trÃ¨s diffÃ©rents, ou alors qu'un algorithme trÃ¨s incomplet
serait suffisant.

\subsection{VÃ©rification de \emph{refactoring}}

Le \emph{refactoring}, la restructuration de programmes, est une
partie importante de l'activitÃ© de programmation. Elle est souvent une
Ã©tape prÃ©alable Ã&nbsp; des changements plus ambitieux, faite sÃ©parÃ©ment
pour Ãªtre plus facile Ã&nbsp; relire et vÃ©rifier par les collÃ¨gues ou
collaborateurs: un bon \emph{refactoring} transforme le programme pour
le rendre plus maintenable mais ne modifie pas son comportement.

Puisque ces transformations sont simples, on peut espÃ©rer qu'un test
d'Ã©quivalence de programmes soit capable de vÃ©rifier leur validitÃ©,
apportant un confort important aux utilisateurs. Le sujet a pourtant
Ã©tÃ© peu Ã©tudiÃ© jusqu'Ã&nbsp; prÃ©sent. Les rares outils en programmation
fonctionnelle soit se restreignent Ã&nbsp; des manipulations de donnÃ©es de
premier ordre \cite{hipspec} soit reposent sur un usage interactif
\cite{hermit} oÃ¹ le programmeur combine explicitement des
transformations unitaires -- une mÃ©thode de travail assez Ã©loignÃ©e de
celle des programmeurs et programmeuses aujourd'hui. Des outils au
niveau des modÃ¨les \cite{uml-stuff} reposent sur l'Ã©quivalence de
processus concurrents, aujourd'hui mieux comprise et implÃ©mentÃ©e, mais
difficilement applicable aux langages fonctionnels.

\subsection{VÃ©rification de compatiblitÃ© ou non-ambiguÃ¯tÃ©}

Dans le systÃ¨me de modules dits ``applicatifs'' des langages
fonctionnels de la famille ML, il est possible de construire un module
Ã&nbsp; partir d'un module paramÃ©trÃ©, et d'un choix de paramÃ¨tre
(un autre module). Si le mÃªme module paramÃ©trÃ© est appliquÃ© Ã&nbsp; deux
modules ``identiques'' passÃ©s en paramÃ¨tre, les modules rÃ©sultats sont
compatibles -- ils peuvent Ã©changer des valeurs. C'est important pour
faire communiquer deux bibliothÃ¨ques ayant fait indÃ©pendamment le mÃªme
choix de paramÃ¨tre, sans devoir les modifier pour dÃ©pendre d'un parent
commun.

Aujourd'hui, la notion d'identitÃ© des paramÃ¨tres est dÃ©finie par une
approximation syntaxique qui repose sur les noms. Deux bibliothÃ¨ques
peuvent faire le mÃªme choix de paramÃ¨tre indÃ©pendamment et coopÃ©rer
ensuite, mais elles ne peuvent pas utiliser deux paramÃ¨tres dÃ©finis de
la mÃªme faÃ§on, le paramÃ¨tre doit venir d'une dÃ©pendance commune. Un
algorithme robuste d'Ã©quivalence entre programmes (et modules)
permettrait de lever cette restriction, en testant que deux paramÃ¨tres
(non syntaxiquements Ã©gaux) sont Ã©quivalents, pour rendre plus de
modules compatibles et donc la programmation modulaire plus aisÃ©e.

Un autre cas d'usage proche correspond Ã&nbsp; des cas d'hÃ©ritage en
diamant: que faire quand un objet hÃ©rite les opÃ©rations de deux
sous-objets qui dÃ©finissent une opÃ©ration de mÃªme nom ? On peut
interdire ce cas, choisir un ordre arbitraire, produire deux
opÃ©rations sÃ©parÃ©es, forcer l'utilisateur Ã&nbsp; renommer... Souvent les
deux opÃ©rations Ã©taient en fait dÃ©finies de faÃ§on identique : un test
d'Ã©quivalence de programme (mÃªme incomplet) permettrait de respecter
l'intention du programmeur dans ce cas. Ce problÃ¨me se prÃ©sente aussi
naturellement dans les formalisations de hiÃ©rarchies de structures
algÃ©briques, par exemple avec les espÃ¨ces de Focalize \cite{focalize}
ou les coercions en Coq \cite{mathcomp}: un monoÃ¯de fini a la
structure d'un ensemble fini et d'un monoÃ¯de, et ces deux
sous-structures ont le mÃªme ensemble de support.

\section{Conception de multi-langages simples et sÃ»rs}

L'Ã©volution des langages gÃ©nÃ©ralistes tend vers l'accrÃ©tion de
fonctionnalitÃ©s pour mieux servir des domaines spÃ©cialisÃ©s divers, qui
peuvent poser des problÃ¨mes de cohÃ©rence ou de complexitÃ© pour le
langage dans son ensemble. OCaml, GHC Haskell, Scala ou encore C++ ont
acquis au fil des annÃ©es des fonctionnalitÃ©s qui rÃ©jouissent leurs
utilisateurs experts mais intimident leurs dÃ©butants, rendent leur
enseignement plus difficile, rendent les compilateurs plus fragiles,
et augmentent le coÃ»t et la difficultÃ© de la construction d'outils
gÃ©rant tout le langage. La recherche en langages de programmation
intensifie ces difficultÃ©s en proposant des fonctionnalitÃ©s puissantes
mais souvent plus complexes et difficile Ã&nbsp; combiner entre elles :
types dÃ©pendants, systÃ¨mes d'effets, types linÃ©aires, sous-ensembles
normalisants, opÃ©rateurs de contrÃ´le, etc. Il est aujourd'hui
nÃ©cessaire de faire diminuer cette complexitÃ© d'utilisation pour que
les rÃ©sultats de nos recherches puissent continuer Ã&nbsp; toucher un public
le plus large possible.

\subsection{Conception de nouveaux systÃ¨mes multi-langages}

Je propose d'Ã©tudier la conception de systÃ¨mes \emph{multi-langages},
dans lesquels plusieurs langages sÃ©parÃ©s co-opÃ¨rent pour couvrir les
mÃªmes domaines applicatifs, en en gÃ©rant chacun seulement une petite
partie. IdÃ©alement, Ã&nbsp; expressivitÃ© Ã©gale ces systÃ¨mes seraient moins
complexes Ã&nbsp; utiliser, en permettant en particulier aux utilisateurs
qui le souhaitent d'apprendre et d'utiliser seulement une partie des
langages du systÃ¨me.

Pour cela, il faut mieux comprendre les problÃ¨mes d'interactions entre
langages : comment concevoir ces systÃ¨mes de faÃ§on Ã&nbsp; Ã©viter les
``fuites d'abstraction'', oÃ¹ l'usage interne des fonctionnalitÃ©s d'un
langage peut casser les propriÃ©tÃ©s attendues par les utilisateurs
d'un autre langage ? Une Ã©tude prÃ©cise de cette question, telle que je
l'ai commencÃ©e pendant mon post-doc Ã&nbsp; Northeastern, devrait nous
donner des outils pour pallier aux intÃ©ractions problÃ©matiques entre
langages existants, et pour concevoir de nouveaux systÃ¨mes
multi-langages plus harmonieux.

Notre approche pour formaliser l'absence de fuites d'abstractions
(\emph{abstraction leaks}) est de prouver la propriÃ©tÃ© de \emph{pleine
  abstraction}: une transformation $f$ d'un langage $S$ vers un
langage $T$ est pleinement abstraite, relativement Ã&nbsp; des notions
d'Ã©quivalence $(=_S), (=_T)$ sur ces deux langages, si
\[
  \forall t, u \in S,\quad
  t =_S u
  \implies
  f(t) =_T f(u)
\]
Quand on considÃ¨re la relation d'Ã©quivalence contextuelle
(ou observationelle), une transformation est pleinement abstraite si,
quand deux fragments du langage source $S$ sont indistinguables
(aucune faÃ§on de les utiliser dans $S$ ne peut observer de diffÃ©rence
entre les deux), alors les fragments transformÃ©s sont indistinguables
dans $T$: mÃªme en utilisant les fonctionnalitÃ©s diffÃ©rentes du langage
$T$, on ne peut pas observer de diffÃ©rence. Si l'on considÃ¨re
maintenant le plongement d'un langage $S$ dans un multi-langage
$S + S'$, ce plongement est pleinement abstrait si les raisonnements
Ã©quationnels qui sont valides dans $S$ le restent dans le
multi-langage.

Pendant mon post-doc j'ai formalisÃ© un cas d'Ã©tude, un systÃ¨me formÃ©
d'un langage fonctionnel simple et d'un langage Ã&nbsp; types linÃ©aires --
permettant des manipulations sÃ»res de protocoles complexes ou de plus
bas niveau -- et prouvÃ© que le plongement du langage fonctionnel dans
le multi-langage est pleinement abstrait. J'aimerais mieux comprendre
les avantages et inconvÃ©nients de cette approche par rapport aux
conceptions de langages monolithiques intÃ©grant les deux aspects,
comme Mezzo \cite{mezzo} ou Rust \cite{rust}, et je pense qu'une faÃ§on
de rendre disponibles des constructions de plus bas niveau sans
augmenter la complexitÃ© du langage pour les utilisateurs non-experts
aurait de nombreuses applications.

Ã€ moyen terme, on imagine un langage fonctionnel gÃ©nÃ©raliste, comme
OCaml, accompagnÃ© d'un ``langage avancÃ©'' complÃ©mentaire, qui permette
d'Ã©crire les implÃ©mentations internes avec un contrÃ´le fin sur les
performances (modifications fortes d'Ã©tat Ã&nbsp; possesseur unique,
contrÃ´le des allocations et de la reprÃ©sentation mÃ©moire...), avec une
garantie d'utilisabilitÃ© : tant qu'une personne n'utilise que des
interfaces exprimÃ©es en OCaml, elle n'a pas besoin de connaÃ®tre le
langage avancÃ©. Ã€ long terme, de nombreux autres aspects avancÃ©s de la
recherche en langage de programmation peuvent Ãªtre proposÃ©s comme des
langages sÃ©parÃ©s : types dÃ©pendants, typage fin des opÃ©rateurs de
contrÃ´le, typage graduel...

Pour concevoir un ``langage du futur'' qui ne soit pas un monstre, il
faut chercher le \emph{multi-langage} du futur.

\subsection{Ã‰tude et amÃ©lioration de multi-langages existants}

La question de la fuite d'abstraction se pose tout particuliÃ¨rement
Ã&nbsp; l'interface entre un langage typÃ© et un langage non typÃ©
(typage graduel), entre un langage vÃ©rifiÃ© et un langage non-vÃ©rifiÃ©
(WhyML et OCaml), ou encore entre un langage totalement fonctionnel
(Coq) et un langage avec effets (OCaml) -- dans ce dernier cas, voir
les travaux prometteurs de \cite{gradual-coq}.
%
On peut aussi voir un problÃ¨me de l'interaction entre langages au
niveau des assistants de preuve : comment relier entre eux des
dÃ©veloppements menÃ©s avec des outils diffÃ©rents ? La question de
l'interopÃ©rabilitÃ© gracieuse, de l'absence de cassures d'abstractions,
se transforme en la question cruciale de la validitÃ© des preuves
combinÃ©es. En effet, les assistants de preuve modernes ne contiennent
pas que des dÃ©rivations statiques, mais aussi des comportements
calculatoires, que la combinaison de prouveurs doit prÃ©server : il
s'agit bien d'interopÃ©rabilitÃ© Ã&nbsp; la fois statique et dynamique, comme
en programmation.

Depuis deux langages existants, on peut toujours crÃ©er un
multi-langage tel que les plongements des langages existants soient
pleinement abstraits: il suffit que le systÃ¨me de typage du
multi-langage interdise aux deux fragments d'Ã©changer des donnÃ©es
(ou de se passer le contrÃ´le) -- on programme mixte est alors
seulement un programme de l'un des deux langages. Deux langages
arbitraires peuvent souvent partager leurs types de donnÃ©es de base
(les entiers par exemple) de faÃ§on sÃ»re; mais le partage de
comportements d'ordre supÃ©rieur, de fonctions ou d'objets par exemple,
est beaucoup plus dÃ©licat.

Par exemple, il n'est pas possible de reprÃ©senter les fonctions de Coq
en OCaml de faÃ§on sÃ»re, puisque OCaml ne peut pas reprÃ©senter
statiquement le type des fonctions qui terminent toujours et ne
produisent pas d'effets de bord. (Ã€ l'inverse on peut choisir une
reprÃ©sentation monadique des fonctions OCaml en Coq.) Cela suggÃ¨re
d'enrichir OCaml avec un type permettant une meilleure interaction, ce
qui pose le problÃ¨me scientifique suivant : si l'on considÃ¨re un
langage ML enrichi d'un type de fonctions totalement pures, d'une
part, et le calcul des constructions (inductives) d'autre part, leur
plongement dans un multi-langage commun est-il pleinement abstrait ?
Je suis convaincu que la rÃ©ponse est ``oui'', mais obtenir le rÃ©sultat
peut Ãªtre difficile. Les cas de l'interaction entre le lambda-calcul
pur non typÃ© et simplement typÃ© \cite{full-dominique}, et entre le
lambda-calcul simplement typÃ© (avec rÃ©cursion) et un lambda-calcul
avec polymorphisme \cite{full-max} n'ont Ã©tÃ© rÃ©solus que cette annÃ©e.

L'Ã©tude des multi-langages et des propriÃ©tÃ©s de pleine abstraction est
un outil de conception pour de nouveaux systÃ¨mes de programmation plus
simples, mais aussi un outil d'amÃ©lioration des systÃ¨mes existants.

\section{Ã‰quipes d'accueil}

Trois laboratoires oÃ¹ mon projet de recherche trouverait parfaitement
sa place m'ont fait l'honneur d'Ãªtre prÃªts Ã&nbsp; m'accueillir. En ordre
alphabÃ©tique : l'IRIF et son Ã©quipe PPS, le LIX et son Ã©quipe
Parsifal, et le LRI et son Ã©quipe VALS.

J'ai eu la chance de suivre des cours et de cÃ´toyer des membres de ces
laboratoires pendant mes Ã©tudes : Roberto Di Cosmo (PPS) m'a enseignÃ©
la logique linÃ©aire, Jean-Christophe FilliÃ¢tre (VALS) la compilation,
Paul-AndrÃ© MelliÃ¨s (PPS) la thÃ©orie des catÃ©gories, et Dale Miller
(Parsifal) la programmation logique. J'ai visitÃ© depuis leurs
laboratoires qui sont des endroits conviviaux oÃ¹ j'aurais plaisir
Ã&nbsp; travailler.

Ces trois laboratoires ont chacun des projets de dÃ©veloppement
logiciel ambitieux et implÃ©mentÃ©s dans le langage OCaml, auxquels je
pourrais donc aussi apporter mon expertise sur le dÃ©veloppement OCaml,
et plus gÃ©nÃ©ralement l'accompagnement des projets de logiciel libre.

\subsection{IRIF: PPS}

L'Ã©quipe PPS a des compÃ©tences riches en logique et en sciences du
logiciel. Elle est au centre du dÃ©veloppement de l'assistant de preuve
Coq, qui est d'abord un outil de preuve mathÃ©matique, mais aussi un
langage de programmation Ã&nbsp; types dÃ©pendants. Un langage au typage si
riche -- et donc aux contraintes de comportement si fortes sur les
programmes -- est un champ d'Ã©tude idÃ©al pour des outils de
programmation dirigÃ©e par les types. J'ai fait en 2013 une Ã©tude des
types utilisÃ©s dans les programmes Ã&nbsp; types dÃ©pendants publiÃ©s dans la
littÃ©rature, et de nombreux types Ã&nbsp; habitants uniques y apparaissent
\cite{dtp}. Une fonctionnalitÃ© d'infÃ©rence non-ambiguÃ« dÃ©terminÃ©e par
les types y serait plus efficace et plus souvent employÃ©e que dans un
langage fonctionnel ordinaire.

Alexis Saurin est un expert en \emph{focusing} avec qui j'aurais
plaisir Ã&nbsp; collaborer, sur l'extension des formes normales saturÃ©es
Ã&nbsp; des types riches par exemple. Yann RÃ©gis-Gianas s'intÃ©resse Ã&nbsp; de
nombreux problÃ¨mes de sciences du logiciel; par exemple, ses travaux
rÃ©cents avec Thibaut Girka sur le calcul des diffÃ©rences entre
programmes \cite{semantic-diff} sont bien alignÃ©s avec ma proposition
d'Ã©tudier les \emph{refactoring} de programmes. Yann a aussi un projet
de langage purement fonctionnel certifiant, Pangolin, actuellement en
pause et qui s'inscrit trÃ¨s bien dans mon projet global de recherche.

Hugo Herbelin et Pierre-Louis Curien sont les initiateurs d'une
famille de travaux sur des langages de programmation pour machines
abstraites dont les formulations rÃ©centes, en particulier les calculs
polarisÃ©s Ã©tablis avec Guillaume Munch-Maccagnoni (non PPS), sont liÃ©es
Ã&nbsp; la fois au \emph{focusing} et Ã&nbsp; l'Ã©tude thÃ©orique des effets de
bords dans les langages de programmation.

Le logiciel Coq est une grande rÃ©ussite Ã&nbsp; laquelle contribuent de
faÃ§on centrale les membres de PPS, et prÃ©sente des problÃ©matiques
dÃ©licates de dÃ©veloppement logiciel. Un travail important d'ouverture
du dÃ©veloppement a Ã©tÃ© accompli en 2016, grÃ¢ce en particulier aux
efforts de Maxime DÃ©nÃ¨s (non PPS), mais cela reste un stade
prÃ©liminaire comparÃ© Ã&nbsp; la situation du langage OCaml -- j'aimerais
contribuer Ã&nbsp; faire progresser les contributions extÃ©rieures. Coq est
aussi un programme exigeant qui utilise beaucoup d'aspects avancÃ©s du
langage OCaml, et nÃ©cessite parfois la correction de problÃ¨mes dans
l'implÃ©mentation d'OCaml ou motive de nouvelles fonctionnalitÃ©s. J'ai
Ã©tÃ© pendant ma thÃ¨se en contact rÃ©gulier avec l'Ã©quipe Coq en tant que
dÃ©veloppeur de l'implÃ©mentation OCaml (Pierre-Marie PÃ©drot, Maxime
DÃ©nÃ¨s, Hugo Herbelin ou Matthieu Sozeau pourront le confirmer), et je
serais ravi de renforcer ce pont entre leurs dÃ©veloppeurs.

Enfin, certaines parties de mon projet de recherche appellent
Ã&nbsp; l'utilisation d'outils de dÃ©monstration automatique et une
acquisition de compÃ©tences dans ce domaine. Cette direction serait un
apport intÃ©ressant aux compÃ©tences de PPS aujourd'hui et pourrait
ouvrir la porte Ã&nbsp; une collaboration fructueuse avec d'autres Ã©quipes
(au LRI et au LIX, mais aussi au LORIA et au LSV).

\subsection{LIX: Parsifal}

L'Ã©quipe Parsifal du laboratoire LIX est aujourd'hui le meilleur
endroit au monde pour travailler sur le \emph{focusing}. Elle a par
exemple accompli un travail remarquable sur l'Ã©tude des liens fins
entre le focusing et les stratÃ©gies existantes de recherche de preuve
et de programmation logique \cite{magic-sets,dpll}, et son travail sur
l'adaptation du focusing Ã&nbsp; la logique intuitioniste
\cite{intuitionistic-focusing,taus} et sur les formes canoniques de
preuves multi-focalisÃ©es \cite{multifocus,multifocus-classical} m'a
beaucoup inspirÃ©.

StÃ©phane Lengrand et Kaustuv Chaudhuri ont une expertise riche en
preuve automatique dont j'aimerais profiter. StÃ©phane connaÃ®t les
approches SMT, grÃ¢ce en particulier Ã&nbsp; des collaborations frÃ©quentes
avec le SRI Ã&nbsp; Stanford, et travaille Ã&nbsp; les intÃ©grer dans un assistant
de preuve. Kaustuv est un expert de la ``mÃ©thode inverse'', une
approche de la recherche de preuve par saturation qui est performante
sur des problÃ¨mes difficiles en logique linÃ©aire ou intuitionniste.

J'apporterais Ã&nbsp; cette Ã©quipe une expertise en conception de langages
de programmation fonctionnels. L'Ã©tude de la programmation logique est
un point fort de Parsifal, et mes travaux ont montrÃ© que les deux
points de vue incarnÃ©s par ces deux approches (les programmes comme
preuves et comme rÃ©sultat d'une recherche de preuve) peuvent produire
des rÃ©sultats nouveaux.

Enfin, je contribuerais aux dÃ©veloppements logiciels du projet
Parsifal, notamment l'assistant de preuve Abella, particuliÃ¨rement
adaptÃ© Ã&nbsp; l'Ã©tude des langages de programmation et qui commence Ã&nbsp; Ãªtre
utilisÃ© en-dehors de l'Ã©quipe, et le projet plus expÃ©rimental Psyche,
qui utilise la recherche sur le \emph{focusing} pour trouver un
Ã©quilibre harmonieux entre preuve automatique et preuve interactive.

\subsection{LRI: VALS}

L'Ã©quipe VALS dÃ©veloppe la plateforme de vÃ©rification de programme
Why3, qui permet Ã&nbsp; ses utilisateurs d'inclure dans leurs programmes
des invariants logiques qui sont vÃ©rifiÃ©s automatiquement. Elle
possÃ¨de aussi une compÃ©tence trÃ¨s forte en dÃ©monstration automatique,
avec en particulier le solveur SMT Alt-Ergo et le vÃ©rifieur de modÃ¨le
Cubicle, et en l'art dÃ©licat de combiner ces outils avec les
obligations de preuves gÃ©nÃ©rÃ©es par la vÃ©rification logicielle. Ce
travail, qui progresse depuis de nombreuses annÃ©es, donne Ã&nbsp; cette
Ã©quipe une expÃ©rience pratique trÃ¨s rare de la programmation aidÃ©e par
la dÃ©monstration automatique, dans laquelle mon projet de recherche
s'inscrit parfaitement.

Mon projet d'Ã©tude de l'interopÃ©rabilitÃ© entre langages, que ce soit
entre le certifiÃ© et le non-certifiÃ© ou le haut-niveau et le
bas-niveau, correspond aussi Ã&nbsp; un besoin dÃ©coulant naturellement des
travaux de cette Ã©quipe. En plus de Why3, Thibaut Balabonski travaille
sur le projet Mezzo, mÃ©langeant programmation fonctionelle et
linÃ©aritÃ© -- sous la forme diffÃ©rente et intÃ©ressante d'une logique de
sÃ©paration -- et Jean-Christophe FilliÃ¢tre coordonne le projet ANR
VOCAL, qui construit une bibliothÃ¨que gÃ©nÃ©raliste vÃ©rifiÃ©e pour OCaml,
et pose donc des questions d'interaction certifiÃ© / non-certifiÃ© et
d'interaction entre les assistants de preuve.

Le langage WhyML au centre de la plateforme Why3 est un langage qui
combine des traits fonctionnels et impÃ©ratifs. Cela a demandÃ© des
dÃ©veloppements intÃ©ressants et utiles pour la vÃ©rification dÃ©ductive,
mais cela limite aussi la libertÃ© des transformations de programme par
rapport Ã&nbsp; un langage aux effets plus restreints (par exemple avec un
systÃ¨me d'effets); deux appels de fonctions indÃ©pendants ne peuvent
pas forcÃ©ment Ãªtre rÃ©ordonnÃ©s, par exemple. En 2009, VALS avait
commencÃ© l'intÃ©gration d'un langage fonctionnel d'ordre supÃ©rieur dans
leur plateforme de programmation certifiÃ©e \cite{who}, que je
souhaiterais reprendre et continuer : c'est un excellent cadre pour
appliquer des techniques de dÃ©monstration automatique aux langages
fonctionnels, et pour Ã©tudier les questions d'interopÃ©rabilitÃ© entre
langages.

\newpage
\begin{small}
\printbibliography
\end{small}
\end{document}
</pre></body></html>