**Top Vole Leslie Lamport** has been named the winner of the 2013 ACM A.M. Turing Award for working out how to impose clear, well-defined coherence on the seemingly chaotic behaviour of distributed computing systems.

Lamport’s algorithms, models and verification systems have enabled distributed computer systems to play the key roles they’re used in throughout the data centre, security and cloud computing landscapes.

He wins a $250,000 prize, with funding support by Intel and Google.

The award was presented by ACM President Vint Cerf who said that as an applied mathematician, Lamport had an extraordinary sense of how to apply mathematical tools to important practical problems.

“By finding useful ways to write specifications and prove correctness of realistic algorithms, assuring a strong foundation for complex computing operations, he helped to move verification from an academic discipline to a practical tool,” Cerf said.

Lamport came up with the idea of Byzantine failure, temporal logic language (TLA+) and LaTex, a document preparation system used in computer science and other fields. We always thought that the Byzantine failure was due to the Battle of Manzikert and underestimating the Turkish empire.

But want Lamport describes makes the Emperor Romanos IV Diogenes battle plans seem straight forward. In 1978 Lamport’s wrote a paper called “Time, Clocks, and the Ordering of Events in a Distributed System” which is one of computer science’s most highly cited. Before joining Microsoft in 2001, Lamport worked for SRI International and DEC (later Compaq).

He earned a B.S. degree in mathematics from the Massachusetts Institute of Technology and an M.S. and Ph.D. in mathematics from Brandeis University.