The first contribution was a foundational sorting algorithm 1 that became widely used. It relied on a partitioning technique 2 described in an earlier paper.
Later work introduced an axiomatic framework for reasoning about programs 3. This built on prior research into formal semantics 4.
Concurrency mechanisms were addressed in subsequent publications 3 5.