Le prix Turing 2013 de l’Association for Computing Machinery (ACM) a été décerné cette année à Leslie Lamport, chercheur du laboratoire commun Inria-Microsoft Research. Retour sur 40 ans de travaux d’un chercheur qui met les mathématiques au service du numérique.

Comment faire travailler sans conflit plusieurs programmes sur un ordinateur, ou faire collaborer plusieurs ordinateurs sur un réseau ? Ces problématiques complexes, connues sous le nom d’informatique distribuée, Leslie Lamport y a consacré une grande partie de ses travaux. Une contribution décisive à la recherche  récompensée par le prix Turing 2013, considéré comme le « Nobel de l’Informatique ».

Après l’obtention de son doctorat en mathématiques en 1972, Leslie Lamport débute sa carrière dans le monde l’informatique en 1977 au sein de l’institut de recherche américain SRI International, puis, de 1985 à 2001, chez le fabricant d’ordinateurs Digital Equipment. Le scientifique intègre ensuite le centre de recherche de Microsoft.

Mathématiques et informatique

Autre volet de ses travaux : la programmation. Pour le mathématicien, plutôt que de se lancer dans l’écriture d’instructions, il faut expliciter ce que le programme doit faire. Il invente pour cela un nouveau langage de programmation : TLA (Temporal logic of actions). L’objectif : créer des instructions pour les programmes grâce à des  formules mathématiques logiques.

En 2006, il rejoint le laboratoire commun Inria-Microsoft Research pour développer une boîte à outils pour TLA+. « Sa boîte à outils voit le jour en 2010, confie Jean-Jacques Lévy, alors directeur du laboratoire. Il s’agit d’un éditeur graphique dans lequel on peut entrer et modifier les spécifications. En parallèle, un système de démonstration automatique permet de vérifier que les résultats sont cohérents. A 73 ans, Leslie Lamport travaille toujours à son amélioration et passe pour cela 3 mois par an en France à collaborer avec les chercheurs du Microsoft Research-Inria Joint Centre. »

Mais ce n’est pas la seule innovation majeure à mettre à son actif dans le domaine des mathématiques appliquées à l’informatique. Leslie Lamport a créé le logiciel de mise en page LaTeX, version améliorée du programme TeX mis au point quelques années auparavant par Donald Knuth.