Skip to main content
SpringerLink
Log in
Book cover

Reflections on the Work of C.A.R. Hoare pp 1–32Cite as

Insight, Inspiration and Collaboration

  • Chapter
  • First Online:

Abstract

Tony Hoare’s many contributions to computing science are marked by insight that was grounded in practical programming. Many of his papers have had a profound impact on the evolution of our field; they have moreover provided a source of inspiration to several generations of researchers. We examine the development of his work through a review of the development of some of his most influential pieces of work such as Hoare logic, CSP and Unifying Theories.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    See thepeerage.com, for example.

  2. 2.

    This is a a type of position given by Oxford Colleges to allow leading young academics to pursue their research.

  3. 3.

    According to [27] when the compiler was run on the much slower 803 a typical half-page ALGOL program would take half an hour to compile and execute.

  4. 4.

    The Turing Award is often referred to as the “Nobel Prize for computing”. It is not clear that the Kyoto Prize committee would concede this – but Tony Hoare has been awarded both.

  5. 5.

    Probably because of his respect for this language, Hoare outlined its defects in [WSH77].

  6. 6.

    In terminology that some find unfortunate – but that has become ubiquitous – he limited himself to “partial correctness” whereas Floyd treated “total correctness”.

  7. 7.

    The slightly enigmatic “Part I” sub-title indicates Apt’s strong interest in non-determinism which he covered in [3].

  8. 8.

    The material had been presented in his Marktoberdorf lectures of 1970.

  9. 9.

    The development of Abrial’s ideas through to “B” [1] (and beyond) deserves separate discussion elsewhere.

  10. 10.

    At the April 2009 event to celebrate Tony’s 75th birthday, Peter O’Hearn linked this to his own research on Separation Logic.

  11. 11.

    In the interview with Bowen cited in Sources.

  12. 12.

    The powerdomain of downward-closed sets was not developed by Hoare, but named after him by Plotkin, because of its close relationship to Tony’s important work on partial correctness.

  13. 13.

    P ⊓Q is a non-deterministic process which is itself allowed to decide which of P and Q to run. Thus the second of these two processes can opt to offer just the event a, while the first has to offer nothing at all (STOP) or {a, b}.

  14. 14.

    P □ Q means that the environment has the choice of the initial events offered by P and Q. The counter-intuitive failure of this law comes about because in P □ P the two copies of P might, because they resolve non-determinism differently, choose to offer different sets, which the operator combines into a single offer that P alone cannot make. This distinction is made in the acceptances or ready-sets congruence, but not using the upwards-closed version of acceptances.

  15. 15.

    The intuition that divergence should be disastrous, derived from the first failures model, was very strong at that time. It is interesting that neither Brookes nor the second author then discovered the “stable failures model”, in which divergence is not recorded, so (as in the traces model) the simply divergent process is top of the refinement order. The existence of that model was conjectured by Albert Meyer and Lalita Jagadeesan in the late 1980s, and developed by the second author following a conversation with them.

  16. 16.

    The second author’s paper elsewhere in this volume illustrates how well CSP has stood the test of time. His 1997 book [31] and forthcoming book [32] both give extensive updates on CSP, its theory, tools and applications.

  17. 17.

    This work led to Oxford and Inmos receiving the Queen's Award for Technological Achievement in 1990

  18. 18.

    http://genealogy.math.ndsu.nodak.edu/

  19. 19.

    Esparza, Lavrov and Wimmel were Habilitation rather than doctoral students of Best.

  20. 20.

    University of Newcastle upon Tyne.

  21. 21.

    Open University.

  22. 22.

    Technical University of Munich.

  23. 23.

    Federal University of Minas Gerais, Brazil.

  24. 24.

    Mike Reed has two doctorates, one from Auburn in 1970 under Ben Fitzpatrick on Set-theoretic Topology, and the one listed above. In addition to Reed’s Computer Science students listed above, he has had a number in topology, but we have decided not to list those here.

  25. 25.

    University College Cork.

  26. 26.

    Queen’s University, Kingston, Ontario.

  27. 27.

    University of Washington.

  28. 28.

    University of British Columbia.

  29. 29.

    Hansen supervised a number of students in Health-related topics at Groningen before undertaking his doctoral studies with Jul.

  30. 30.

    Alex Teruel set up the Parallel and Distributed Research Group at Simon Bolivar University, Venezuela. He supervised numerous MSc students there but advised them to do their PhDs abroad. He is happy to report that since a number of these people did this successfully and now have completed PhD students of their own, the fruits of Tony’s advisorship are thriving in Venezuela.

  31. 31.

    City University of New York.

  32. 32.

    Federal University of Pernambuco, Brazil.

Bibliography 1: Papers by Hoare

  1. Hoare, C.A.R.: Critique of ALGOL 68. ALGOL Bullet. 29, 27–29 (November 1968).

    Google Scholar 

  2. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580, 583 (October 1969).

    MATH  Google Scholar 

  3. Foley, M., Hoare, C.A.R.: Proof of a recursive program: Quicksort. BCS Comput. J. 14(4), 391–395 (November 1971).

    MATH  MathSciNet  Google Scholar 

  4. Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Engeler, E. (ed.), Symposium on Semantics of Algorithmic Languages – Lecture Notes in Mathematics 188, pp. 102–116. Springer (1971).

    Google Scholar 

  5. Hoare, C.A.R.: Proof of a program: Find. Commun. ACM 14(1), 39–45 (January 1971).

    MATH  Google Scholar 

  6. Dahl, O.-J., Dijkstra, E.W., Hoare, C.A.R. (eds.), Structured Programming. Academic (1972). London; San Diego: Academic Press, 1990, 1972.

    Google Scholar 

  7. Hoare, C.A.R.: A note on the FOR statement. BIT 12(3), 334–341 (1972).

    MATH  Google Scholar 

  8. Hoare, C.A.R.: Notes on data structuring. In Dahl, O.-J., Dijkstra, E.W., Hoare, C.A.R. (eds.), Structured Programming, pp. 83–174. Academic (1972). London; SanDiego: Academic Press, 1990, 1972.

    Google Scholar 

  9. Hoare, C.A.R.: Proof of a structured program: ‘The Sieve of Eratosthenes’. BCS, Computer J. 15(4), 321–325 (November 1972).

    MATH  MathSciNet  Google Scholar 

  10. Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(4), 271–281 (1972).

    MATH  Google Scholar 

  11. Hoare, C.A.R.: Towards a theory of parallel programming. In: Operating System Techniques pp. 61–71. Academic (1972).

    Google Scholar 

  12. Hoare, C.A.R.: Hints on programming language design. Technical Report STAN-CS-73-403, Stanford (October 1973).

    Google Scholar 

  13. Hoare, C.A.R.: A structured paging system. BCS Comput. J. 16(3), 209–215 (August 1973).

    MATH  Google Scholar 

  14. Hoare, C.A.R., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica 2(4), 335–355 (1973).

    Google Scholar 

  15. Hoare, C.A.R., Lauer, P.E.: Consistent and complementary formal theories of the semantics of programming languages. Acta Informatica 3(2), 135–153 (1974).

    MATH  MathSciNet  Google Scholar 

  16. Hoare, C.A.R.: Monitors: An operating system structuring concept. Commun. ACM 17(10), 549–557 (October 1974).

    MATH  Google Scholar 

  17. Hoare, C.A.R.: Parallel programming: An axiomatic approach. Comput. Languages 1(2), 151–160 (June 1975).

    MATH  MathSciNet  Google Scholar 

  18. Ashcroft, E.A., Clint, M., Hoare, C.A.R.: Remarks on “program proving: Jumps and functions”. Acta Informatica 6(3), 317–318 (1976).

    MATH  Google Scholar 

  19. Welsh, J., Sneeringer, W.J., Hoare, C.A.R.: Ambiguities and insecurities in PASCAL. Software Practice Experience 7(6), 685–96 (November–December 1977).

    MATH  Google Scholar 

  20. Francez, N., Hoare, C.A.R., Lehmann, D.J., de Roever, W.P.: Semantics of nondeterminism, concurrency and communication. J. Comput. System Sci. 19(3), 290–308 (December 1979).

    MATH  MathSciNet  Google Scholar 

  21. Hoare, C.A.R., Brookes, S.D., Roscoe, A.W.: A theory of communicating sequential processes. Technical Report PRG 16, Oxford University Computing Laboratory, Programming Research Group (1981).

    Google Scholar 

  22. Hoare, C.A.R.: A calculus of total correctness for communicating processes. The Sci. Computer Programming 1(1–2), 49–72 (October 1981).

    MATH  MathSciNet  Google Scholar 

  23. Hoare, C.A.R.: The emperor’s old clothes. Commun. ACM 24(2), 75–83 (February 1981).

    Google Scholar 

  24. Hoare, C.A.R., Olderog, E.R.: Specification-oriented semantics for communicating processes. In: Automata Languages and Programming 10th Colloquium, vol. 154 of Lecture Notes in Computer Science, pp. 561–572. Springer (1983).

    Google Scholar 

  25. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (July 1984).

    MATH  MathSciNet  Google Scholar 

  26. Hoare, C.A.R., Roscoe, A.W.: Programs as executable predicates. In: Proceedings of the International Conference on Fifth Generation Computer Systems, November 6–9 1984, Tokyo, Japan, pp. 220–228. ICOT (1984).

    Google Scholar 

  27. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985). 256 pp., ISBN 0-13-153271-5.

    MATH  Google Scholar 

  28. Hoare, C.A.R.: Programs are predicates. In: Hoare, C.A.R. Shepherdson, J.C. (eds.), Mathematical Logic and Programming Languages, pp. 141–154. Prentice-Hall (1985).

    Google Scholar 

  29. Hoare, C.A.R., He, J.: The weakest prespecification I. Fundamenta Informaticae 9(1), 51–84 (March 1986).

    MATH  MathSciNet  Google Scholar 

  30. He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In Robinet, B., Wilhelm, R. (eds.), ESOP ’86: Proceedings of the European Symposium on Programming, vol. 213 of Lecture Notes in Computer Science. Springer (1986).

    Google Scholar 

  31. Roscoe, A.W., Hoare, C.A.R.: Laws of occam programming. Monograph PRG-53,Oxford University Computing Laboratory, Programming Research Group (February 1986).

    Google Scholar 

  32. Hoare, C.A.R., Hayes, I.J., He, J., Morgan, C.C., Roscoe, A.W., Sanders, J.W., Sørensen, I.H., Spivey, J.M., Sufrin, B.A.: The laws of programming. Commun. of the ACM 30(8), 672–687 (August 1987). see Corrigenda in Commun. ACM 30(9), 770. * * * * * * * * * * * * * * * * * * * * *The following is a list of all Hoare’s papers since 1988, complementing the list published in [HJ89].

    MATH  Google Scholar 

  33. Hoare, C.A.R., Gordon, M.J.C.: Partial correctness of CMOS switching circuits: An exercise in applied logic. In: LICS, pp. 28–36 (1988).

    Google Scholar 

  34. Roscoe, A.W., Hoare, C.A.R.: The laws of occam programming. Theoret. Comput. Sci. 60, 177–229 (1988).

    MATH  MathSciNet  Google Scholar 

  35. He, J., Hoare, C.A.R.: Categorical semantics for programming languages. In: Mathematical Foundations of Programming Semantics, pp. 402–417 (1989).

    Google Scholar 

  36. Hoare, C.A.R., Jones, C.B.: Essays in Computing Science. Prentice Hall International, 1989.

    Google Scholar 

  37. Hoare, C.A.R.: The varieties of programming language. In: TAPSOFT, Vol.1, pages 1–18, 1989.

    Google Scholar 

  38. Bjørner, D., Hoare, C.A.R., Langmaack, H.: VDM ’90, VDM and Z – Formal Methods in Software Development, Third International Symposium of VDM Europe, Kiel, FRG, April 17–21, 1990, Proceedings, vol. 428 of Lecture Notes in Computer Science. Springer (1990).

    Google Scholar 

  39. Hoare, C.A.R.: Fixed points of increasing functions. Inf. Process. Lett. 34(3), 111–112 (1990).

    MATH  MathSciNet  Google Scholar 

  40. Hoare, C.A.R.: Let’s make models (abstract). In: CONCUR, p. 32 (1990).

    Google Scholar 

  41. Hoare, C.A.R.: A theory of conjunction and concurrency. In: PARBASE / Architectures, pp. 18–30 (1990).

    Google Scholar 

  42. Hoare, C.A.R.: A theory for the derivation of combinational CMOS circuit designs. Theoret. Comput. Sci. 90(1), 235–251 (1991).

    MATH  MathSciNet  Google Scholar 

  43. Hoare, C.A.R.: The transputer and occam: A personal story. Concurrency Practice Exp., 3(4), 249–264 (1991).

    Google Scholar 

  44. Martin, C.E., Hoare, C.A.R., He, J.: Pre-adjunctions in order enriched categories. Mathematical Struct. Comput. Sci. 1(2), 141–158 (1991).

    MATH  MathSciNet  Google Scholar 

  45. Zhou, Ch., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991).

    MATH  MathSciNet  Google Scholar 

  46. Hoare, C.A.R., Gordon, M.J.C. (eds.), Mechanised Reasoning and Hardware Design. Prentice Hall International Series in Computer Science. ISBN 0-13-572405-8 (1992).

    Google Scholar 

  47. Hoare, C.A.R.: Programs are predicates. In: FGCS, pp. 211–218 (1992).

    Google Scholar 

  48. Zhou, C., Hoare, C.A.R.: A model for synchronous switching circuits and its theory of correctness. Formal Methods System Design 1(1), 7–28 (1992).

    MATH  Google Scholar 

  49. He, J., Hoare, C.A.R.: From algebra to operational semantics. Inf. Process. Lett. 45(2), 75–80 (1993).

    MATH  MathSciNet  Google Scholar 

  50. Hoare, C.A.R., He, J., Sampaio, A.: Normal form approach to compiler design. Acta informatica 30(8), 701–739 (1993).

    MATH  MathSciNet  Google Scholar 

  51. Hoare, C.A.R.: Algebra and models. In: SIGSOFT FSE, pp. 1–8 (1993).

    Google Scholar 

  52. He, J., Hoare, C.A.R., Fränzle, M., Müller-Olm, M., Olderog, E.-R., Schenke, M., Hansen, M.R., Ravn, A.P., Rischel, H.: Provably correct systems. In: FTRTFT, pp. 288–335 (1994).

    Google Scholar 

  53. Hoare, C.A.R.: Editorial. J. Log. Comput. 4(3), 215–216 (1994).

    Google Scholar 

  54. Hoare, C.A.R., Page, I.: Hardware and software: The closing gap. In: Programming Languages and System Architectures, pp. 49–68 (1994).

    Google Scholar 

  55. Hoare, C.A.R.: Unification of theories: A challenge for computing science. In: COMPASS/ADT, pp. 49–57 (1995).

    Google Scholar 

  56. Burghard van Karger, B., Hoare, C.A.R.: Sequential calculus. Inf. Process. Lett 53(3), 123–130 (1995).

    Google Scholar 

  57. Hoare, C.A.R.: How did software get so reliable without proof? In: FME, pp. 1–17 (1996).

    Google Scholar 

  58. Hoare, C.A.R.: The logic of engineering design. Microprocess. Microprogramm. 41(8-9), 525–539 (1996).

    Google Scholar 

  59. Hoare, C.A.R.: Mathematical models for computing science. In: NATO ASI DPD, pp. 115–164 (1996).

    Google Scholar 

  60. Hoare, C.A.R.: The role of formal techniques: Past, current and future or how did software get so reliable without proof? (extended abstract). In: ICSE, pp. 233–234, (1996).

    Google Scholar 

  61. Hoare, C.A.R.: Unifying theories: A personal statement. ACM Comput. Surv. 28(4es) 46 (1996).

    Google Scholar 

  62. Wirth, N., Hoare, C.A.R.: A contribution to the development of ALGOL. Communi. of the ACM 9(6) 413–432 (June 1966).

    MATH  Google Scholar 

  63. Hoare, C.A.R., He, J.: Unifying theories for parallel programming. In: Euro-Par, pp. 15–30 (1997).

    Google Scholar 

  64. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall (1998).

    Google Scholar 

  65. He, J., Hoare, C.A.R.: Linking theories in probabilistic programming. Inf. Sci. 119, (3-4) 205–218 (1999).

    MATH  MathSciNet  Google Scholar 

  66. Hoare, C.A.R., He, J.: A trace model for pointers and objects. In: ECOOP, pp. 1–17 (1999).

    Google Scholar 

  67. Hoare, C.A.R.: Theories of programming: Top-down and bottom-up and meeting in the middle. In: Correct System Design, pp. 3–28 (1999).

    Google Scholar 

  68. Hoare, C.A.R.: Theories of programming: Top-down and bottom-up and meeting in the middle. In: World Congress on Formal Methods, pp. 1–27 (1999).

    Google Scholar 

  69. Péyton Jones, S.L., Reid, A., Henderson, F., Hoare, C.A.R., Marlow, S.: A semantics for imprecise exceptions. In: PLDI, pp. 25–36 (1999).

    Google Scholar 

  70. Seres, S., Spivey, M.J., Hoare, C.A.R.: Algebra of logic programming. In: ICLP, pp. 184–199 (1999).

    Google Scholar 

  71. He, J., Hoare, C.A.R.: Unifying theories of healthiness condition. In: APSEC, pp. 70–, 2000.

    Google Scholar 

  72. Hoare, C.A.R., He, J., Sampaio, A.: Algebraic derivation of an operational semantics. In: Proof, Language, and Interaction, pp. 77–98 (2000).

    Google Scholar 

  73. Hoare, C.A.R.: Assertions. In: IFM, pp. 1–2 (2000).

    Google Scholar 

  74. Hoare, C.A.R.: A hard act to follow. Higher-Order and Symbolic Comput 13(1/2), 71–72 (2000).

    MATH  Google Scholar 

  75. Hoare, C.A.R.: Legacy code. In: ICFEM, p. 75 (2000).

    Google Scholar 

  76. Hoare, C.A.R.: Growing use of assertions. In: TOOLS (38), p. 3 (2001).

    Google Scholar 

  77. Hoare, C.A.R.: Legacy. Inf. Process. Lett., 77(2-4):123–129, 2001.

    MathSciNet  Google Scholar 

  78. Boyer, R.S., Feijen, W.H.J., Gries, D., Hoare, C.A.R., Misra, J, Moore, J., Richards, H.: In: memoriam: Edsger w. Dijkstra 1930–2002. Commun. ACM 45(10):21–22 (2002).

    Google Scholar 

  79. Hoare, C.A.R.: Assertions in modern software engineering practice. In: COMPSAC, pp. 459–462 (2002).

    Google Scholar 

  80. Hoare, C.A.R.: Assertions in programming: From scientific theory to engineering practice. In: Soft-Ware, pp. 350–351 (2002).

    Google Scholar 

  81. Hoare, C.A.R.: Towards the verifying compiler. In: 10th Anniversary Colloquium of UNU/IIST, pp. 151–160 (2002).

    Google Scholar 

  82. Hoare, C.A.R.: Assertions: A personal perspective. IEEE Ann. History Comput. 25(2), 14–25 (2003).

    MathSciNet  Google Scholar 

  83. Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. J. ACM 50(1), 63–69 (2003). (This paper also appeared in a number of other publications).

    Google Scholar 

  84. Butler, M.J., Hoare, C.A.R., Ferreira, C.: A trace semantics for long-running transactions. In: 25 Years Communicating Sequential Processes, pp. 133–150 (2004).

    Google Scholar 

  85. Fournet, C., Hoare, C.A.R., Rajamani, S.K., Rehof, J.: Stuck-free conformance. In: CAV, pp. 242–254 (2004).

    Google Scholar 

  86. Hoare, C.A.R.: Process algebra: A unifying approach. In: 25 Years Communicating Sequential Processes, pp. 36–60 (2004).

    Google Scholar 

  87. Hoare, C.A.R.: Towards the verifying compiler. In: Essays in Memory of Ole-Johan Dahl, pp. 124–136 (2004).

    Google Scholar 

  88. Bruni, R., Butler, M.J., Ferreira, C., Hoare, C.A.R., Melgratti, H.C., Montanari, U.: Comparing two approaches to compensable flow composition. In CONCUR, pp. 383–397 (2005).

    Google Scholar 

  89. He, J., Hoare, C.A.R.: Linking theories of concurrency. In: ICTAC, pp. 303–317 (2005).

    Google Scholar 

  90. Hoare, C.A.R., Milner, R.: Grand challenges for computing research. Comput. J. 48(1), 49–52 (2005).

    Google Scholar 

  91. Hoare, C.A.R., Misra, J.: Verified software: Theories, tools, experiments vision of a grand challenge project. In: VSTTE, pp. 1–18 (2005).

    Google Scholar 

  92. Beckert, B., Hoare, C.A.R., Hähnle, R., Smith, D.R., Green, C., Ranise, S., Tinelli, C., Ball, T., Rajamani, S.K.: Intelligent systems and formal methods in software engineering. IEEE Intelligent Systems 21(6), 71–81 (2006).

    Google Scholar 

  93. Bicarregui, J., Hoare, C.A.R., Woodcock, J.C.P.: The verified software repository: A step towards the verifying compiler. Formal Asp. Comput. 18(2), 143–151(2006).

    MATH  Google Scholar 

  94. He, J., Hoare, C.A.R.: CSP is a retract of CCS. In: UTP, pp. 38–62 (2006). TCS 411 (issue 11--13), pp. 1311--1337, 2010doi:10.1016/j.tcs.2009.12.012

    Google Scholar 

  95. Hoare, C.A.R.: The ideal of verified software. In: CAV pp. 5–16 (2006).

    Google Scholar 

  96. Hoare, C.A.R.: Why ever CSP? Electr. Notes Theoret. Comput. Sci. 162, 209–215 (2006).

    Google Scholar 

  97. Vafeiadis, V., Herlihy, M., Hoare, C.A.R., Shapiro, M.: Proving correctness of highly.concurrent linearisable objects. In: PPOPP, pp. 129–136 (2006).

    Google Scholar 

  98. Hoare, C.A.R.: Fine-grain concurrency. In: CPA, pp. 1–19 (2007).

    Google Scholar 

  99. Hoare, C.A.R.: The ideal of program correctness: Third Computer Journal lecture. Comput. J. 50(3), 254–260 (2007).

    MathSciNet  Google Scholar 

  100. Hoare, C.A.R.: Science and engineering: A collusion of cultures. In: DSN, pp. 2–9 (2007).

    Google Scholar 

  101. Hoare, C.A.R., O’Hearn, P.W.: Separation logic semantics for communicating processes. Electr. Notes Theoret. Comput. Sci. 212:3–25 (2008).

    Google Scholar 

  102. Hoare, C.A.R.: Keynote: A vision for the science of computing. In: BCS Int. Acad. Conf., pp. 1–29 (2008).

    Google Scholar 

  103. Hoare, C.A.R.: Verification of fine-grain concurrent programs. Electr. Notes Theoret. Comput. Sci. 209, 165–171 (2008).

    MathSciNet  Google Scholar 

  104. Hoare, C.A.R.: Verified software: Theories, tools, experiments. In: ICECCS, p. 3 (2008).

    Google Scholar 

  105. Hoare, C.A.R., Misra, J.: Preface to special issue on software verification. ACM Comput. Surv. 41(4) (2009).

    Google Scholar 

  106. Hoare, C.A.R., Misra, J., Leavens, G.T., Shankar, N.: The verified software initiative: A manifesto. ACM Comput. Surv. 41(4), (2009).

    Google Scholar 

  107. Hoare, C.A.R., Mller, B., Struth, G., Wehrman, I.: Concurrent Kleene algebra. In: CONCUR, pp. 399–414 (2009).

    Google Scholar 

  108. Hoare, C.A.R., Möller, B., Struth, G., Wehrman, I.: Foundations of concurrent Kleene algebra. In: RelMiCS, pp. 166–186 (2009).

    Google Scholar 

  109. Hoare, C.A.R.: Viewpoint – retrospective: an axiomatic basis for computer programming. Commun. ACM 52(10), 30–32 (2009).

    Google Scholar 

  110. Wehrman, I., Hoare, C.A.R., O’Hearn, P.W.: Graphical models of separation logic. Inf. Process. Lett. 109(17), 1001–1004 (2009).

    MATH  MathSciNet  Google Scholar 

  111. Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press (1996).

    MATH  Google Scholar 

  112. Apt, K.R.: Ten years of Hoare’s logic: A survey – part I. ACM Trans. Programm. Languages Systems 3, 431–483 (1981).

    MATH  Google Scholar 

  113. Apt, K.R.: Ten years of Hoare’s logic: A survey – part II: Nondeterminism. Theoret. Comput. Sci., 28, 83–109 (1984).

    MATH  MathSciNet  Google Scholar 

  114. Bekič, H., Bjørner, D., Henhapl, W., Jones, C.B., Lucas, P.: A formal definition of a PL/I subset. Technical Report 25.139, IBM Laboratory Vienna (December 1974).

    Google Scholar 

  115. Bjørner, D., Jones, C.B. (eds.), The Vienna Development Method: The Meta-Language, vol. 61 of Lecture Notes in Computer Science. Springer (1978).

    Google Scholar 

  116. Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating processes (1985).

    Google Scholar 

  117. Brookes, S.D.: A mathematical theory of communicating processes. PhD thesis, University of Oxford (1983).

    Google Scholar 

  118. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976).

    MATH  Google Scholar 

  119. De Nicola, R., Hennessy, M.C.B.: Testing equivalences for processes (1983).

    Google Scholar 

  120. Floyd, R.W.: Assigning meanings to programs. In: Proc. Symp. in Applied Mathematics, Vol.19: Mathematical Aspects of Computer Science, pp. 19–32. American Mathematical Society (1967).

    Google Scholar 

  121. Goldsmith, M.H., Roscoe, A.W.: Transformation of occam programs. In: Design and Application of Parallel Digital Processors, 1988, pp. 180–188 (1988).

    Google Scholar 

  122. Goldstine, H.H., von Neumann, J.: Planning and coding of problems for an electronic computing instrument, 1947. Part II, Vol. 1 of a Report prepared for U.S. Army Ord. Dept.; republished as pp. 80–151 of [34].

    Google Scholar 

  123. Holt, R.C., Matthews, P.A., J.A, J.A., Cordy, J.R.: The Turing Programming Language: Design and Defintion. Prentice Hall International (1988).

    Google Scholar 

  124. Jones, C.B.: Software Development: A Rigorous Approach. Prentice Hall International (1980).

    MATH  Google Scholar 

  125. Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE, Annals of the History of Comput. 25(2), 26–49 (2003).

    Google Scholar 

  126. Jones, C.B.: Splitting atoms safely. Theoret. Comput. Sci. 357, 109–119 (2007).

    Google Scholar 

  127. King, J.C.: A Program Verifier. PhD thesis, Department of Computer Science, Carnegie-Mellon University (1969).

    Google Scholar 

  128. Lauer, P.E.: Consistent Formal Theories of the Semantics of Programming Languages. PhD thesis, Queen’s University of Belfast, 1971. Printed as TR 25.121, IBM Lab. Vienna.

    Google Scholar 

  129. INMOS Ltd. Occam Programming Manual. Prentice Hall (1984).

    Google Scholar 

  130. Lucas, P., Walk, K.: On the Formal Description of PL/I, vol. 6, Part 3 of Annual Review in Automatic Programming. Pergamon Press (1969).

    Google Scholar 

  131. McCarthy, J.: A basis for a mathematical theory for computation. In: Braffort, P., Hirschberg, D. (eds.) Computer Programming and Formal Systems, pp. 33–70. North-Holland (1963). (A slightly extended and corrected version of a talk given at the May 1961 Western Joint Computer Conference).

    Google Scholar 

  132. McCarthy, J.: A formal description of a subset of ALGOL. In: [33], pp. 1–12 (1966).

    Google Scholar 

  133. Milner, R.: Processes: a mathematical model of computing agents. In: Logic Colloquium.73. North Holland (1973).

    Google Scholar 

  134. Milner. R.: Flowgraphs and flow algebras. J. ACM 26(4), 794–818 (1979).

    MATH  MathSciNet  Google Scholar 

  135. Milner, R.: A Calculus of Communicating Systems. Springer, New York, Inc. Secaucus, NJ, USA (1982).

    Google Scholar 

  136. Plotkin, G.D.: A powerdomain construction. SIAM. Comput. 5, 452 (1976).

    MATH  MathSciNet  Google Scholar 

  137. Reilly, E.D.: Milestones in Computer Science and Information Technology. Greenwood Pub Group (2003).

    Google Scholar 

  138. Roscoe, A.W.: A mathematical theory of communicating processes. PhD thesis, University of Oxford (1982).

    Google Scholar 

  139. Roscoe, A.W.: Denotational Semantics for occam (1985).

    Google Scholar 

  140. Roscoe, A.W.: Occam in the specification and verification of microprocessors. Philosophical Transactions: Physical Sciences and Engineering, pp. 137–151 (1992).

    Google Scholar 

  141. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall (1997).

    Google Scholar 

  142. Roscoe, A.W.: Understanding Concurrent Systems. Springer (2010).

    MATH  Google Scholar 

  143. Steel, T.B.: Formal Language Description Languages for Computer Programming. North-Holland (1966).

    Google Scholar 

  144. Taub, A.H. (ed.), John von Neumann: Collected Works, vol. V: Design of Computers, Theory of Automata and Numerical Analysis. Pergamon Press (1963).

    Google Scholar 

  145. Turing. A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67–69. University Mathematical Laboratory, Cambridge (June 1949).

    Google Scholar 

  146. van Wijngaarden, A.: Numerical analysis as an independent science. BIT 6:66–81 (1966). (Text of 1964 talk).

    Google Scholar 

Download references

Acknowledgements

The authors are grateful to Tony Hoare and Robin Milner for their recollections about the development of process algebra, to David May, Gordon Plotkin, Brian Randell, Willem-Paul de Roever and others for their memories and comments, and to many of Tony’s academic descendants for contributing to the family tree below.

We are extremely grateful to Lucy Li of Oxford University Computing Laboratory who undertook the monumental task of assembling the family tree as well as helping us to put together the extended bibliography.

The first author’s research is supported by the EPSRC Platform Grant on “Trustworthy Ambient Systems” and EU FP7 “DEPLOY project”. The second author’s is supported by the EPSRC Grant “CSP Model Checking: New Technologies and Techniques” and by grants from the US ONR.

Author information

Authors and Affiliations

  1. School of Computing Science, Newcastle University, Newcastle, UK

    C. B. Jones

  2. Oxford University Computing Laboratory, Oxford, UK

    A. W. Roscoe

Authors
  1. C. B. Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. W. Roscoe
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to C. B. Jones .

Editor information

Editors and Affiliations

  1. Oxford University Computing Laboratory, Parks Road, Oxford, OX13QD, United Kingdom

    A.W. Roscoe

  2. Dept. Computing Science, University of Newcastle upon Tyne, Newcastle upon Tyne, NE17RU, United Kingdom

    Cliff B. Jones

  3. Microsoft Research Ltd., J. J. Thomson Avenue 7, Cambridge, CB30FB, United Kingdom

    Kenneth R. Wood

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer London

About this chapter

Cite this chapter

Jones, C.B., Roscoe, A.W. (2010). Insight, Inspiration and Collaboration. In: Roscoe, A., Jones, C., Wood, K. (eds) Reflections on the Work of C.A.R. Hoare. Springer, London. https://doi.org/10.1007/978-1-84882-912-1_1

Download citation

  • DOI: https://doi.org/10.1007/978-1-84882-912-1_1

  • Published:

  • Publisher Name: Springer, London

  • Print ISBN: 978-1-84882-911-4

  • Online ISBN: 978-1-84882-912-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation