Theories of Programming: The Life and Works of Tony HoareOctober 2021
  • Association for Computing Machinery
  • New York
  • NY
  • United States
Appears In:


Sir Tony Hoare has had an enormous influence on computer science, from the Quicksort algorithm to the science of software development, concurrency and program verification. His contributions have been widely recognised: He was awarded the ACM’s Turing Award in 1980, the Kyoto Prize from the Inamori Foundation in 2000, and was knighted for “services to education and computer science” by Queen Elizabeth II of England in 2000.

This book presents the essence of his various works—the quest for effective abstractions—both in his own words as well as chapters written by leading experts in the field, including many of his research collaborators. In addition, this volume contains biographical material, his Turing award lecture, the transcript of an interview and some of his seminal papers.

Hoare’s foundational paper “An Axiomatic Basis for Computer Programming”, presented his approach, commonly known as Hoare Logic, for proving the correctness of programs by using logical assertions. Hoare Logic and subsequent developments have formed the basis of a wide variety of software verification efforts. Hoare was instrumental in proposing the Verified Software Initiative, a cooperative international project directed at the scientific challenges of large-scale software verification, encompassing theories, tools and experiments.

Tony Hoare’s contributions to the theory and practice of concurrent software systems are equally impressive. The process algebra called Communicating Sequential Processes (CSP) has been one of the fundamental paradigms, both as a mathematical theory to reason about concurrent computation as well as the basis for the programming language occam. CSP served as a framework for exploring several ideas in denotational semantics such as powerdomains, as well as notions of abstraction and refinement. It is the basis for a series of industrial-strength tools which have been employed in a wide range of applications.

This book also presents Hoare’s work in the last few decades. These works include a rigorous approach to specifications in software engineering practice, including procedural and data abstractions, data refinement, and a modular theory of designs. More recently, he has worked with collaborators to develop Unifying Theories of Programming (UTP). Their goal is to identify the common algebraic theories that lie at the core of sequential, concurrent, reactive and cyber-physical computations.

Theories of Programming: The Life and Works of Tony Hoare is available as a printed book and an on-line version. In addition to the book itself, a number of on-line resources might be of interest to readers:

  • A bibliography of Tony Hoare’s papers with clickable DOIs/URLs where available (
  • Appendix E of the book provides links to talks and interviews featuring Tony Hoare (
  • The Oxford archive of Hoare’s manuscripts (

"Supplementary Material: Tony Hoare" is a PDF of additional material (not included in the book) containing the following:

  • Stories from a Life in Interesting Times (A transcription by Jayadev Misra of Tony Hoare’s acceptance speech for the 2000 Kyoto prize)
  • Tony Hoare’s Heidelberg comments (A transcription by Margaret Gray of Tony Hoare’s part in the 2020 Heidelberg event)
  • Milestones in Tony’s Life and Work (A ‘cv’ of Tony Hoare prepared by Margaret Gray)
  • Extended version - "Bernard Sufrin: Teaching at Belfast and Oxford"

Book Downloads

October 2021, pp xvii–xx

Tony Hoare has had an enormous impact on computing: early in his career, he created software for users; even when he addressed more theoretical topics, there was always the aim to affect the way that software could be created. A theme that can be seen ...

              The 1980 ACM Turing Award Lecture
              Finding Effective Abstractions
              Preface to Special Issue on Software Verification
              The First Fifteen Years of the Verified Software Project
              Communicating Sequential Processes
              October 2021, pp 157–186
              CSP: A Practical Process Algebra
              October 2021, pp 187–222
              Teaching at Belfast and Oxford
              October 2021, pp 223–250
              Software Specification
              October 2021, pp 251–270
              CSP, Occam, and Inmos
              October 2021, pp 271–284
              Hoare and He’s Unifying Theories of Programming
              October 2021, pp 285–316
              Trimming the Hedges: An Algebra to Tame Concurrency
              October 2021, pp 317–346
              October 2021, pp 347–356
              ACM Interview
              October 2021, pp 359–386
              October 2021, pp 387–392
              Doctoral Students
              October 2021, pp 393–394
              List of Tony Hoare’s Publications
              October 2021, pp 395–410
              Online Resources
              October 2021, pp 411–412
              Authors’ Biographies/Index
              October 2021, pp 413–420



              About Cookies On This Site

              We use cookies to ensure that we give you the best experience on our website.

              Learn more

              Got it!