Sites Inria

Version française

Turing Award 2013

Olivier Lapirot - 3/06/2014

Leslie Lamport: a pioneering scientific career

Leslie Lamport Leslie Lamport - © Bernard Lachaud

On 21 June, the Association for Computing Machinery's Turing Award for 2013 will be presented to Leslie Lamport, a researcher at the Microsoft Research-Inria joint laboratory. Below is a review of the 40-year career of a researcher in mathematics for digital technology

How can several programmes be made to work on a computer without conflict and how can several computers work together on a network? Leslie Lamport has dedicated a large part of his work to these complex problems, known as distributed computing. His decisive contribution to research has been recognised by the 2013 Turing Award, considered as the "Nobel Prize for computer science".

After receiving his doctorate in mathematics in 1972, Leslie Lamport began his career in the field of computer science at the American Research Institute SRI International in 1977 and then, from 1985 to 2001, with the computer manufacturers DEC. The scientist then joined the Microsoft Research Centre. "Leslie liked to add a very personal touch to his work, anchoring his theories in the real world", stated Jean-Jacques Lévy , Emeritus Research Director at Inria. The three algorithms that made him famous therefore have very concrete names: the "boulangerie" (bakery) algorithm, the Byzantine generals' algorithm and Paxos".

The first algorithm was inspired by the queue at the boulangerie, as in order to work, each programme has to wait its turn in accordance with the order of arrival. The second and third algorithms allow several computers to make a joint decision despite the presence of "traitors" among them, or absent parliamentarians... Leslie Lamport likes to push these analogies to the limit in order to cover every possibility. As for Paxos, well this is the algorithm currently used for synchronising Bing and Google servers.

Mathematics and computer science

Another aspect of his work involves programming. The mathematician believes that instead of writing instructions, it is necessary to explain what the programme has to do. To do this, he invented a new programming language: TLA (Temporal Logic of Actions). The aim was to create instructions for programmes using logical mathematical formulae.  In 2006, he joined the Microsoft Research-Inria joint laboratory to develop a toolbox for TLA+. "His toolbox was launched in 2010, asserted Jean-Jacques Lévy, then Director of the Laboratory. It is a graphics editor in which specifications can be entered and modified. At the same time, an automatic demonstration system makes it possible to check that the results are consistent. Now aged 73, Leslie Lamport is still working on improving it and spends three months a year in France working with researchers from the Microsoft Research-Inria Joint Centre."

But this is not the only major innovation to his credit in the field of mathematics applied to computer science. In 1983, Leslie Lamport created the document preparation software LaTeX, an improved version of the TeX programme developed a few years previously by Donald Knuth . LaTeX allows the most complex mathematical formulae to be written easily and is currently used by the entire scientific community for drafting the formulae which appear in research articles!

The official presentation ceremony of the Turing Award will take place on June 21 in San Francisco.

Keywords: Microsoft Research Turing Award ACM Distributed system