Leslie Barry Lamport

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.