Sites Inria

Récompense

Alexandre Papin - 12/07/2012

Jean-Pierre Talpin récompensé 20 ans après

Jean-Pierre Talpin, responsable de l’équipe Espresso, vient de recevoir le LICS test-of-time Award 20 ans après la publication de son papier sur « The type and effect discipline ».

Vous venez d’être récompensé pour un article de conférence publié il y a 20 ans. Pouvez-vous nous en dire plus à ce sujet ?

Oui, il s'agit du "LICS test-of-time Award", un prix de l'ACM/IEEE qui récompense un ou plusieurs articles présentés à l'occasion de la conférence LICS (Logics in Computer Science).  En l'occurrence, il  s'agit de mon premier article de conférence, publié à LICS'92 avec mon directeur de thèse, Pierre Jouvelot (Ecole des Mines de Paris).  

Que votre article a-t-il apporté à la communauté scientifique?

Cet article est le pivot entre deux lignes de travaux. Il contribue tout d'abord au développement du langage fonctionnel typé FX (Dave Gifford et Pierre Jouvelot, MIT/PRSG). Il est ensuite le point de départ de ML-Kit, une mise en oeuvre du langage fonctionnel ML avec une gestion mémoire par région (Mads Tofte, DIKU).
On retrouve aujourd'hui ce principe de programmation dans Real-Time Java et Safety-Critical Java. Au lieu d'avoir recours à une tâche de fond, le GC ("garbage collector"), dont la charge de calcul n'est pas toujours prédictible, pour récupérer la mémoire inutilisée d'un programme, la gestion mémoire par région consiste à calculer la durée de vie des données du programme à la compilation, et de générer automatiquement les opération élémentaires d'allocation et de récupération de ses données.
L'article LICS présente deux avancées théoriques. Tout d'abord il établit la calculabilité d'abstractions de l'utilisation mémoire de programmes fonctionnels en utilisant un principe de typage. Il définit ensuite une relation d'abstraction qui, elle, conduit à la difficulté théorique majeure de l'article: la preuve de consistance entre l'utilisation mémoire effective d'un programme et le type qui le caractérise.
Cette preuve à elle seule nous a accaparé et passionné pendant plusieurs mois (et jusqu'à sa publication intégrale dans Information and Computation, en 1994). Elle a nécessité la mise en place d'un mécanisme de raisonnement co-inductif (alors peu utilisé) et la définition d'une relation d'équivalence comportementale entre programme-mémoire et type. De nombreux travaux apparentés se sont ensuite évertués à reproduire, simplifier, généraliser cette seule preuve, d'entre eux utilisant la théorie de la concurrence, d'autres un cadre monadique, etc.

Que vous apporte ce prix aujourd’hui?

Très franchement, cela a tout d'abord été un choc, car mon second article de conférence, publié avec Mads Tofte (DIKU) à POPL'94, lui jetant les bases de la gestion mémoire par région, avait déjà été primé dix ans plus tard avec le ACM/SIGPLAN "Most influencial POPL paper Award", en 2004. Rétrospectivement, je suis très heureux des marques de reconnaissances qui récompensent ainsi la contribution de ma thèse et mettent en valeur la qualité de l'encadrement qu'a assuré mon directeur de thèse et ami, Pierre Jouvelot.

Mots-clés : LICS Inria Rennes Bretagne Atlantique Jean-Pierre Taplin ESPRESSO

Haut de page

Suivez Inria