Fellow
United States – 2014
CITATION

For contributions to the theory and practice of distributed and concurrent systems

ACM A. M. Turing Award
Microsoft Research United States – 2013
READ FULL CITATION AND ESSAY
CITATION

For fundamental contributions to the theory and practice of distributed and concurrent systems, notably the invention of concepts such as causality and logical clocks, safety and liveness, replicated state machines, and sequential consistency.


Leslie Lamport originated many of the key concepts of distributed and concurrent computing, including causality and logical clocks, replicated state machines, and sequential consistency. Along with others, he invented the notion of Byzantine failure and algorithms for reaching agreement despite such failures. He contributed to the development and understanding of proof methods for concurrent systems, notably by introducing the notions of safety and liveness as the proper generalizations of partial correctness and termination to the concurrent setting. In addition, he devised important distributed algorithms and developed a substantial collection of formal modeling and verification methods and tools that have been used to improve the quality of real distributed systems. His contributions share a common theme: to impose clear and well-defined coherence on the seemingly chaotic behavior of a collection of distributed processes. They make it substantially easier for algorithm designers to design distributed algorithms, and for programmers to write distributed programs.