Leslie B. Lamport

Originated key concepts of distributed computing: logical time and timestamps, replicated state machines, atomic objects, sequential consistency, wait-freedom, safety and liveness, and global invariants. Pioneered global snapshots for distributed systems (with Chandy), prophecy variables (with Abadi), and Byzantine fault-tolerance (with Pease and Shostak). The underlying theme was to make a distributed system coherent, so that it is easier for programmers to make it work. Replicated state machines and Paxos consensus algorithm are now the basis for most reliable distributed systems. Showed how to prove a distributed algorithm correct with global invariants (predicates on the entire system state), proved by induction on program steps; most proofs for distributed algorithms are now done this way. Articulated safety and liveness properties, the generalization of partial correctness and total correctness. Today they are so widely used that no one cites Lamport. Developed TLA+ (Temporal Logic of Actions) for modeling and verifying distributed systems (both safety and liveness). These tools work for real systems, both hardware and software. Book, Specifying Systems (2002), teaches engineers how to use them. Lamport's LaTeX overlay on Knuth's TeX is the standard tool for typesetting scientific papers.