000			06054nam a2200697 i 4500
001			9781450387316
003			ACM
005			20260528133338.0
008			211004s2021 nyu 001 0deng d
020			_a3477355
020			_a9781450387316 _qebook
020			_a9781450387309 _qepub
020			_z9781450387286 _qhardcover
020			_z9781450387293 _qpaperback
024	7		_a10.1145/3477355 _2doi
100	0		_aJones, Cliff B. _eeditor.
245	1	0	_aTheories of Programming / _bThe Life and Works of Tony Hoare / _cCliff B. Jones, Jayadev Misra.
250			_aFirst Edition
264		1	_a[New York, NY, USA] : _bAssociation for Computing Machinery; _c[2021].
300			_a1 PDF (xx, 430 pages) _bLuaTEX
490	1		_aACM books, _x2374-6777 ; _v#39
505	8		_aPreface
505	8		_aPART I INTRODUCTION
505	8		_a1 The 1980 ACM Turing Award Lecture
505	8		_a2 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
505	8		_aPART II PROGRAM VERIFICATION
505	8		_a3 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
505	8		_a4 Preface to Special Issue on Software Verification
505	8		_a5 The Verified Software Initiative: A Manifesto -- 5.1 Introduction -- 5.2 Executive Summary -- 5.3 Manifesto -- 5.4 Assessment -- 5.5 Conclusions
505	8		_a6 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
505	8		_a7 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?
505	8		_aPART III COMMUNICATING SEQUENTIAL PROCESSES
505	8		_a8 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
505	8		_a9 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
505	8		_aPART IV TEACHING AND INDUSTRIAL AFFILIATIONS
505	8		_a10 Teaching at Belfast and Oxford -- 10.1 Introduction -- 10.2 Queen's University Belfast -- 10.3 University of Oxford -- 10.4 Valediction -- References
505	8		_a11 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
505	8		_a12 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
505	8		_aPART V RECENT RESEARCH DIRECTIONS
505	8		_a13 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
505	8		_a14 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
505	8		_aPART VI RETROSPECT AND PROSPECT
505	8		_a15 Envoi
505	8		_aPART VII APPENDICES
505	8		_aAppendix A ACM Interview
505	8		_aAppendix 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
505	8		_aAppendix C Doctoral Students
505	8		_aAppendix D List of Tony Hoare's Publications -- References
505	8		_aAppendix E Online Resources
505	8		_aAuthor's Biographies
505	8		_aIndex
506			_aAbstract freely available; full-text restricted to subscribers or individual document purchasers.
530			_aAlso available in print.
538			_aMode of access: World Wide Web
538			_aSystem requirements: Adobe Acrobat Reader
650		0	_aTheories of Programming (Computer Programming)
655		0	_aElectronic books.
776	0	8	_iPrint version: _z9781450387286 _z9781450387293
830		0	_aACM books - Collection 2 ; _v#39.
856	4	0	_3Abstract with links to full text _uhttps://doi.org/10.1145/3477355
999			_c388 _d388