TY  - BOOK
AU  - Jones, Cliff B.
TI  - Theories of Programming / : The Life and Works of Tony Hoare / 
T2  - ACM books, 
SN  - 3477355
PY  - 2021///]
CY  - [New York, NY, USA]
PB  - Association for Computing Machinery
KW  - Theories of Programming (Computer Programming)
KW  - Electronic books
N1  - Preface; PART I INTRODUCTION; 1 The 1980 ACM Turing Award Lecture; 2 Finding Effective Abstractions -- 2.1 Programming Languages -- 2.2 Founding the Field of Axiomatic Semantics -- 2.3 Concurrency -- 2.4 Unifying Theories of Programming -- References; PART II PROGRAM VERIFICATION; 3 Assessing the Success and Impact of Hoare's Logic -- 3.1 Early Approaches to Program Verification -- 3.2 Hoare's Logic -- 3.3 Hoare's Initial Contributions -- 3.4 Termination -- 3.5 Influence on Programming Methodology -- 3.6 Hoare's Reasoning About Recursive Procedures -- 3.7 Research on Soundness and Completeness -- 3.8 Reasoning About Arbitrary Procedures -- 3.9 Parallel Programs -- 3.10 Distributed Programs -- 3.11 Object-orientated Programs -- 3.12 Competing Approaches to Program Verification -- 3.13 Concluding Remarks -- References; 4 Preface to Special Issue on Software Verification; 5 The Verified Software Initiative: A Manifesto -- 5.1 Introduction -- 5.2 Executive Summary -- 5.3 Manifesto -- 5.4 Assessment -- 5.5 Conclusions; 6 The First Fifteen Years of the Verified Software Project -- 6.1 Introduction -- 6.2 The Roots of the Verified Software Initiative -- 6.3 Theory -- 6.4 Tools -- 6.5 Experiments -- 6.6 The Road Ahead -- References; 7 Verification in the Grand Challenge -- 7.1 Introduction -- 7.2 Tokeneer -- 7.3 Research Based on Tokeneer -- 7.4 Pilot Project: Hypervisor -- 7.5 What's Next?; PART III COMMUNICATING SEQUENTIAL PROCESSES; 8 Communicating Sequential Processes -- 8.1 Introduction -- 8.2 Concepts and Notations -- 8.3 Coroutines -- 8.4 Subroutines and Data Representations -- 8.5 Monitors and Scheduling -- 8.6 Miscellaneous -- 8.7 Discussion -- 8.8 Conclusion -- References; 9 CSP: A Practical Process Algebra -- 9.1 Introduction -- 9.2 Prehistory 1978-1991 -- 9.3 FDR1 1991-1996 : Communication, Fault Tolerance, and the Beginning of Time -- 9.4 FDR2 1994-2007 at FSEL: Protocols, Abstraction, and Industrial Applications -- 9.5 FDR2 into Academia: Exploring Implicit Checking and Timed CSP (2007-2012) -- 9.6 FDR3 and FDR4: Back to Basics and into the Cloud (2012-2019) -- 9.8 The Future: For CSP and Beyond (2019-) -- 9.9 Reflections on FDR -- References; PART IV TEACHING AND INDUSTRIAL AFFILIATIONS; 10 Teaching at Belfast and Oxford -- 10.1 Introduction -- 10.2 Queen's University Belfast -- 10.3 University of Oxford -- 10.4 Valediction -- References; 11 Software Specification -- 11.1 Precondition-Postcondition Specifications -- 11.2 Specification of Data Types -- 11.3 The Role of Specification -- 11.4 Abstraction in Specification -- 11.5 Specifying Operations -- 11.6 Abstract Data Types -- 11.7 Structuring Specifications Via Aspects -- 11.8 The IBM/CICS Project -- 11.9 Industry Influence on Research -- 11.10 Conclusions -- References; 12 CSP, Occam, and Inmos -- 12.1 Background -- 12.2 The Inmos System Language -- 12.3 Parallel Execution -- 12.4 Channels -- 12.5 Alternative -- 12.6 Timers -- 12.7 Subroutines -- 12.8 The Algebraic Specification -- 12.9 Formal Methods in Hardware Design -- 12.10 Hardware Design Languages -- 12.11 General Purpose Parallel Computers -- 12.12 Impact - 12.13 Tomorrow -- 12.14 Retrospect -- References; PART V RECENT RESEARCH DIRECTIONS; 13 Hoare and He's Unifying Theories of Programming -- 13.1 Origins of UTP -- 13.2 Retirement Symposium and UTP Book Launch -- 13.3 Introduction to UTP -- 13.4 Relational Calculus -- 13.5 Relational Semantics of a Programming Language -- 13.6 Designs -- 13.7 Galois Connections -- 13.8 Design Healthiness Conditions -- 13.9 The UTP School of Semantics -- References; 14 Trimming the Hedges: An Algebra to Tame Concurrency -- 14.1 Prologue -- 14.2 Prehistory -- 14.3 Concurrent Kleene Algebra -- 14.4 Interchange in Context -- 14.5 Series-parallel Pomsets, Completeness, and Decidability -- 14.6 Weak Interchange and Compositional Concurrency -- 14.7 Other Developments -- 14.8 Epilogue -- References; PART VI RETROSPECT AND PROSPECT; 15 Envoi; PART VII APPENDICES; Appendix A ACM Interview; Appendix B CV -- B.1 Early Years -- B.2 Professional Life -- B.3 Awards and Honours -- B.4 Other Professional Activities -- B.5 A Short Photo Album; Appendix C Doctoral Students; Appendix D List of Tony Hoare's Publications -- References; Appendix E Online Resources; Author's Biographies; Index; Abstract freely available; full-text restricted to subscribers or individual document purchasers; Also available in print
UR  - https://doi.org/10.1145/3477355
ER  -