A Bibliography of Publications by, and about, Sir Charles Antony Richard Hoare

Nelson H. F. Beebe University of Utah Department of Mathematics, 110 LCB 155 S 1400 E RM 233 Salt Lake City, UT 84112-0090 USA

Tel: +1 801 581 5254 FAX: +1 801 581 4148

       E-mail: beebe@math.utah.edu, beebe@acm.org,
                  beebe@computer.org (Internet)
     WWW URL: https://www.math.utah.edu/~beebe/

18 May 2024 Version 1.10

Title word cross-reference

#13753 [Pri79].

∗ [DJ83]. i [Bro76, FR75]. k [SD16]. n [Bro76, FR75].

-safety [SD16]. -th [Bro76, FR75].

0 [Hor89]. 0-13-284027-8 [Hor89].

10 [Hoa71a]. 11th [Kap92, BJM09, GN12]. 14th [HJKM14]. 16th [AdA05]. 17th [IEE76, Hoa86b]. 18 [Pri79]. 1971 [Hoa71a, HP72]. 1980 [HJ16, Hoa21b]. 1983 [ACM83]. 1985 [Hoa86b]. 1991 [GH92]. 1994 [Bro96]. 1999 [Ryd99].

2.1 [Hoa66a]. 2.15s [Hoa70b]. 2/WG [MW08]. 2000 [HBS01, IEE00]. 2003 [HW04]. 2007 [Mül10]. 2007/2008 [Mül10]. 2008 [LL08, Mül10]. 2011 [Hoa12a, Hoa12b]. 2013 [JN13]. 20th [Cip00]. 25 [VT90]. 26th [IEE02]. 28/29 [BD01].

30 [HHH^{+}87a]. 33rd [HP12]. 35 [Pet91]. 3rd [IEE88].

4.20 [Bar75]. 489 [FR75]. 4th [WGF13].

56 [Pri79]. 5th [BF10].

60 [HW66]. 63 [Hoa61a]. 64 [Hoa61b]. 65 [Hoa61c]. 68 [Hoa68a, Hoa68e, WTD^{+}69]. 6th [BJM09].

70th [LWZ13]. 75th [JL11]. ’76 [ACM76]. 7th [dOSRS19].

8 [Hor89]. 85th [dOSRS19].

’90 [BHL90, BK90, RNT90]. ’99 [Ryd99].

A. [Hoa68c]. AADL [ZLW^{+}19]. AB21.3 [Krá66]. Abrupt [HJ00]. Abstraction [BNNN22]. Abstractions [JM21a]. Academic [Bar75, BF10]. Acceptance [EHP^{+}75a]. Achievement [Hoa12a, BO12, Hoa12b]. ACM [ACM83, HHH^{+}87a, Hoa12a, Hoa12b, HJ16, Hoa21b, LL08, Ryd99, Ash87, FR75, JM21c]. Act [Hoa00a]. Ad [WZX19]. Ada [FG84]. adaptation [Old83a]. add [Hoa86c]. Addenda [HW74]. Address [HH90e, Hoa91e, Hoa78e, Hoa90c, HH97c]. addressing [Hoa65a]. adjunctions [MHH91]. Advanced [Bro96, Mül10]. Afternoon [Dij82a]. Ago [McR97]. Aided [BGB12]. AKA [BJM09]. Algebra [BR21, HM19, Hoa92, Hoa93a, Hoa93b, Hoa95, Hoa96a, Hoa05b, Hoa05c, HSW19b, SSH99, Str21, vSH13, BJM09, GP94, HH93, HH90d, HH90e, HH92, HMSW09a, HMSW09b, HMSW11, HvS12a, HvSM^{+}14, HvSM^{+}16, HSW19a, Koz00]. Algebraic [Aic19, Gar95, HH87a, HH86a, Hoa87a, Hoa91a, HS94, HHS97, HJS00, HJKM14, DN13, GB96, HHBP90]. Algebras [BP03, But19]. ALGOL [WH66b, Hoa62b, Hoa63b, Hoa64c, HW66, Hoa68a, Hoa68e, S^{+}67, WH65, WH66a, WTD^{+}69, Hoa64a]. Algorithm [Bro76, FR75, GR96, Grü98, KP98, HH87a, NS77, Pri79, Pro95, VT90, Ver87, Bro76, Hoa61c, Hoa61a, Hoa61b]. Algorithms [Cip00, vd86, dH08]. Always [Pet91, VT90]. Always-true [Pet91, VT90]. Ambiguities [WSH77]. Amir [MP10]. amp [Hoa04b]. analysing [Nie87]. Analysis [FKMJ12, Hoa61d, RAR^{+}10]. Annual [IEE88, IEE02, ACM76, ACM83, IEE76]. Answer [Lew97, Thi06]. Antony [BO12, DRW00, Dij99, Fra02]. application [Hoa76a, HP12]. Applications [BJM09, EH89, HJ04, IEE02, Hoa10a, RNT90]. applied [HG88]. Approach [Grü98, Hoa89c, HHS93, Hoa05b, Hoa05c, Hoa71b, Hoa75c, Hoa76e, HHBP90, HGRA89, Rid09]. approaches [BBF^{+}05]. April [ACM83, BHL90, HJKM14]. APSEC [IEE00]. architectures [RNT90]. arithmetic [BT83]. Art [Bat76]. Asia [IEE00]. Asia-Pacific [IEE00]. assembly [NS06]. assertion [CSW89]. Assertional [Pet91, Sha93]. Assertions [Hoa00d, Hoa02j, Hoa02a, Hoa02i, Hoa02b, Hoa03a, Hoa03b]. Assessing [AO21, FG84]. associated [CSW89]. Asymptotic [GR96]. asynchronous [JHH89]. asynchronously [dB02]. asynchrony [HHJ90]. Atlanta [Ryd99]. atom [Hoa04b]. atomic [Win89]. Aug [EN74]. August [AdA05, BS76, Bro96, HP72, HBS01, IEE02, WGF13, Dij70]. Author [JM21d]. authorization [BN10]. Automated [BY92, BY96, Kap92, Sok87, CSW89, Kap92]. automorphisms [Hoa79]. Auxiliary [Kle99, vON02]. Award [Ash87, HJ16, Hoa21b, BO12, Hoa12b, Hoa12a]. Axiom [Cla79, Qia90]. Axiomatic [BT84b, Hoa69, HW72, HW73, HW74, Hoa83b, Hoa01a, Hoa02c, Hoa71b, Hoa74a, Hoa75c, Hoa76e, Hoa96e, Hoa96f, Hoa09]. Axiomatics [CK79]. Axiomatization [dH08]. Axiomatizations [CGH83].

B [Hor89]. Based [BT84b, KH82, Old81, BGB09]. basic [BHL^{+}96]. Basis [Hoa61d, Hoa69, Hoa83b, Hoa01a, Hoa02c, Hoa81c, Hoa96e, Hoa09]. Bazilevskii [Bae65]. BC [LL08]. be [PJ89]. Beach [RNT90]. Beauty [FvGGM90]. bedrock [Chl13]. before [Hoa71a, Hoa86b]. Behaviour [Hoa12c]. behind [Hoa73c]. being [Dij82a]. Belfast [HP72, Hoa71a, Suf21]. Best [Cip00]. better [Hoa72g]. Binary [Lew97]. Biographies [JM21d, Wei88]. Biographies/Index [JM21d]. Birthday [FvGGM90, JL11, LWZ13, dOSRS19]. Blocks [Hoa11]. Bonn [BD01]. Book [Ano87, Bar75, Bar74, Hoa63a, Hoa64a, Hoa70a, Hoa70b, Hoa77a, Hor89, Llo74, Bro73]. Boston [ACM83]. Bottom [Hoa99]. Bottom-Up [Hoa99]. Brian [JL11]. Broadcasting [Bro88]. Brooks [McR97]. Buffering [Bro88]. Business [FvGGM90]. Butterworths [Hoa70b].

C [Ano87, Bae65, Bar75, Bar74, Bro73, Hoa70b, Hor89, Llo74, Ros94, FG84, HG88, Hoa90d, Hoa91c, Hoa91d, Ols97]. C-MOS [HG88, Hoa90d, Hoa91c, Hoa91d]. C. [ACH76, Dij70, Dij74, Dij75, Dij77, Dij82d, Dij82a, Dij82b, Dijxx, Hoa82b, JRW10, Shu09]. CA [AdA05]. CADE [Kap92]. CADE-11 [Kap92]. Calculi [HvS12b, Old81, vSH13, HvS14, Kir82]. Calculus [Hoa81b, HSW19b, RWH01, WZX19, Hoa81a, HZ82, Hoa85b, HSW19a, Mil90, ZHR91, vKH95]. Call [dBH21]. Call-by-Value [dBH21]. Calls [Bri02, SLN07]. can [PJ89]. Canada [LL08]. Card [HS10]. Cartesian [SD16]. Case [Hoa64b]. Categorical [HH90a, HH90c, KN92, HH90b, Hoa90a]. categories [MHH91]. Category [Hoa89c]. Causality [HSW19b, HSW19a]. causally [SS95]. causally-ordered [SS95]. CBE [HW04]. CCS [HH10]. CE [GR97]. Century [Cip00]. certification [BGB09]. Certified [CSV07, NS06]. Certifying [CCC^{+}17]. Chain [Grü98]. Challenge [Hoa96i, Hoa03g, HM08, Hoa03h, Hoa05a, WBC^{+}21]. Challenges [HM19, Hoa04e, HM05]. Characterisation [HS94]. characterization [Old83b]. characterizations [MS89]. Charles [BO12, Dij99, Fra02]. chief [Hoa70b]. circuit [Hoa90d, Hoa91c, Hoa91d]. circuits [HG88, HZ90, ZH92]. CKA [MH15]. claims [CSW89]. class [Dijxx]. Classical [FY21, Ros94]. Clint [ACH76]. Closing [HP94b, HP94a]. Clothes [Hoa81f, Hoa87c]. Club [Dij82a]. Co [ZLW^{+}19]. Co-modelling [ZLW^{+}19]. code [BGB09, BY92, BY96, CSV07, Hoa00b, NS06, Thi06]. code-based [BGB09]. Coded [Sun96]. Coinitial [Hoa79]. collection [Hoa74d]. College [JN13]. Collusion [Hoa07c]. combinational [Hoa91c, Hoa91d]. Combining [GP94, Chl13]. Comm [HHH^{+}87a]. Command [EHP^{+}75c, Hoa75b, Hoa76d]. Comments [EHP^{+}75b, EHP^{+}75c, Pet91, Pri79, S^{+}67, VT90]. commercial [BY92]. Communicating [BHR84, Hoa78c, Hoa78a, Hoa78b, Hoa81b, HZ81, Hoa85a, Hoa86d, Hoa87a, Hoa02d, HO08, Hoa21a, KH82, OH86, EHT87, HH83, Hoa80b, Hoa80c, Hoa81a, Hoa81d, HZ82, Hoa83d, Hoa85d, Hoa91a, OH83, ZH81, dB02, AJS05, Hoa83c, Ano87]. Communication [Bro88, Hoa91b, Sil81, FHdR78, FHLdR79]. communications [Hoa93e]. commute [FM90]. Comparing [BBF^{+}05, FG84]. Comparisons [KP98]. Compensable [Hoa07a, Hoa10c, BBF^{+}05]. compilation [Hoa66c, HH92]. Compiler [HHS93, Hoa03e, Hoa03g, Hoa04f, BHW06, Hoa03f, Hoa03h, Hoa05a]. compiling [HHBP90, HH90d, HH90e]. Complementary [HL74]. Complete [CK79, DJ83, Old81, AMMO09, HH83]. Completeness [BT82c, Kir82, XSZ16, dBH21, BT82a, Gar95, Rod85]. Complexity [Hoa93c, dBH21, CK00]. composition [BBF^{+}05, FM90]. Compositional [Hoo92, DHD97, SU07]. computable [BG01]. computation [Jac15, Nie87]. Computations [Gut19]. Computer [BGB12, HJ04, Hoa69, Hoa71a, Hoa73a, Hoa76a, Hoa83b, Hoa89c, Hoa01a, HBS01, Hoa02c, HJKM14, IEE76, IEE88, IEE02, BJM09, DRW00, Hoa81c, Hoa86c, Hoa89b, Hoa96e, Hoa09, Hoa07b, Hoa70b]. Computer-Aided [BGB12]. Computing [ACM83, Dij82c, Hoa89a, Hoa96i, Hoa03g, Hoa04e, HM05, JL11, JN13, Pri79, Ano76, Hoa96d, HB98, Hoa03c, Hoa03h, Hoa05a, Hor89, ACM76]. Concept [Hoa74c, Hoa02e]. CONCUR [AdA05, AdA05, BK90]. Concurrency [BK90, But19, HM19, Hoa91b, Hoa10d, Str21, AdA05, CSA^{+}96, DHD97, FHdR78, FHLdR79, HH05, Hoa90e, Hoa91e, HH97c, Hoa10e, Hoa13b, TDB13]. Concurrent [Bri02, HMSW09a, HMSW11, Hoa12c, Lam80, Sha93, Hoa08, HMSW09b, HHM^{+}11, Hoa13c, HvSM^{+}14, Hoa14, HvSM^{+}16, Mil90, SNBD16, Sha06, Sti88, VHHS06]. condition [HH00, HM95]. conditions [SNBD16]. Conference [AdA05, BJM09, BF10, BD01, GN12, HP12, HJKM14, IEE00, IEE02, Kap92, MW08, Ryd99, Ano76, RNT90]. conformance [FHRR04]. conjunction [Hoa90e, Hoa91e]. Connecting [Gut19]. conservation [Hoa73b]. considerations [Pra76]. consistency [Gar95, HZ82]. Consistent [CK79, HL74]. Constrained [RWH01]. Construction [HBS01, GN12, vA98]. constructors [FM90]. Constructs [Cla79]. context [vA98]. Continuations [TT91, DN13]. Contradiction [Hoa78d]. Contribution [WH65, WH66a, WH66b, S^{+}67]. Contributions [BD01, BD02, BD01]. Control [EHP^{+}75c, Hoa93c, Hoa75b, Hoa76d]. conversation [DH94]. Copy [Old81]. Copying [vd86]. Correct [HHF^{+}94]. Correctness [Ano07a, Ano07b, Hoa81b, HZ81, Hoa01b, Hoa02f, Hoa07b, Old84, BY92, CCC^{+}17, Fok87, GB96, Hoa72f, Hoa75d, Hoa76f, Hoa81a, HZ82, HG88, HZ90, HH90d, HH90e, HH92, Hoa96g, SNBD16, VHHS06, ZH81, ZH92, dH08]. Corrigenda [HW74, HHH^{+}87a]. Corrigendum [Hoa78c]. cost [Hoa76c]. couple [Hoa85b]. courses [Hoa76h]. Crash [CCC^{+}17]. crashes [CCC^{+}17]. Critic [Lew97]. Critique [GM81, Hoa68a, O’D82]. cryptographic [BGB09, dH08]. CSP [AJS05, BR21, HH10, HM85, Hoa06b, LS84, May21, SH85]. Cultures [Hoa07c]. CV [Mis21]. Cyber [ZLW^{+}19]. Cyber-Physical [ZLW^{+}19]. Cyclic [BBC08].

D. [Dij77, Dij82d]. Dahl [Bar75, Bar74, Llo74, OKL04]. Data [BNNN22, HHS86, HH90b, Hoa68b, Hoa75a, Hoa90a, Hoa01b, Hoa02f, BT84a, Hoa72c, Hoa72f, Hoa75e, Hoa76f, HHS87, Hoa96g, HW11, LV96, Win89]. data-parallel [LV96]. Database [LL08, Qia90]. databases [RNT90]. Dawn [Day12a]. Deadlocks [SL97]. decidable [BT82b]. Decisions [HM19]. decomposition [Tak87]. Dedicated [JL11, LWZ13, Dij77, Dij82d, Dij99, dOSRS19, Dij82a]. deduction [Kap92]. Deductive [Bro96]. Definition [HW72, HW73, HW74, Hoa74a, Hoa96f]. delivered [Hoa71a, Hoa86b]. Denotational [Aic19]. Dependable [JL11]. dependent [NMS^{+}08]. Derivation [vd86, Hoa90d, Hoa91c, Hoa91d, HHS97, HJS00]. described [PJ89]. Design [EHP^{+}75b, HM19, Hoa73d, Hoa73e, Hoa73f, HH87b, Hoa87b, HJ91, HHS93, RWH01, Ryd99, Bro96, GH92, Hoa74b, Hoa74e, Hoa75b, Hoa76d, Hoa89b, Hoa96c, Hoa10a]. designs [Hoa90d, Hoa91c, Hoa91d]. determinism [HK80]. Deterministic [Mam16, dB02]. Developing [HM19]. Development [WH65, WH66a, WH66b, BHL90, S^{+}67]. Developments [Hoa91b, HvSM^{+}14, HvSM^{+}16]. dialog [EHT87]. did [Hoa96b]. Dijkstra [Bar75, Bar74, Llo74, AH22, BFG^{+}02, Day12a, FvGGM90, Hoa03d, Jac15]. Directed [Sil81]. directions [CSA^{+}96]. discipline [Dij76, Hoa73a]. disciplines [Hoa73b]. Discrete [KH82]. Discussion [Ano07a, Ano07b, GH92]. Discussions [MW08]. Distinguished [Hoa12a, BO12, Hoa12b]. Distributed [JMS87, HH87a, MP88, RAR^{+}10, Rid09, VT90, Ver87]. Distribution [GR96]. Doctoral [JM21e]. does [Hoa04d]. Doha [BJM09]. DOM [GSWZ08]. domain [FM90]. Down [Hoa99, Ols97]. Draft [Hoa68e, WTD^{+}69]. DSE [HJR04b, HJR04a]. durations [ZHR91]. Dynamic [BNNN22, dB02].

E. [Pri79]. ed [Hor89]. Edinburgh [IEE88]. Editor [Pet91, Wel97]. Editorial [Hoa72a, Hoa94b]. Editors [Cip00]. Edsger [AH22, BFG^{+}02, FvGGM90, Hoa03d, Hoa22]. Effective [CGH83, JM21a]. Effects [vON02]. Efficient [JH75]. eighth [ACM76]. elected [Dij82a]. Elements [Bro76, FR75, Pro95]. Elliott [Hoa62b, Hoa63b, Hoa64c]. embedded [NS06]. Emeritus [Anoxx]. emperor [Hoa87c, Hoa81f]. Engeering [IEE00]. Engineering [BHH^{+}06, BD01, BD02, BP03, BGHH05, Day12a, Hoa78d, HBS01, Hoa02i, Hoa07c, Ano76, Hoa73a, Hoa75f, Hoa78e, Hoa83e, Hoa93e, Hoa96c, HB98, Hoa02j, Mül10]. England [IEE02]. enriched [MHH91]. Envoi [Hoa21c]. Eratosthenes [Hoa72e]. Errata [WH66b]. Esprit [BHL^{+}96]. Essays [Hoa89a, JL11, LWZ13, MP10, OKL04, Ros94, Hor89]. EUROCOMP [Ano76]. Europe [BHL90]. European [Ano76]. Event [KH82]. ever [Hoa06b]. Evolution [vd86]. exception [CD82, Szc91]. Exceptions [PRH^{+}99, JRH^{+}99]. exchange [HHM^{+}11]. exclusion [PJ89]. executable [HR84]. exercise [Dij89, HG88]. Experiment [Dijxx]. Experiments [HM08, MW08]. Exploring [MH15]. expressed [SH85]. expressions [Hoa64b]. expressive [Hoo91]. Expressiveness [BT82a, Old83a, Rod85]. Extended [Hoo92]. Extending [HJR04b, HJR04a, Hoo94]. extensible [Chl13]. Extension [BK90].

F [Dij77, Dij82d]. fail [BT82b]. Fast [MH77]. Fault [JMS87]. Favorite [Ker84, Ker81]. FBCS [BO12]. February [Hoa71a, HW04]. Fellow [Dij82a]. Fifteen [MS21]. fifteenth [ACM83]. Fifty [AO19]. file [CCC^{+}17]. final [BHL^{+}96, WTD^{+}69]. FIND [Hoa71d, FKMJ12, Hoa61c, Pro95, KP98]. Finding [Bro76, FR75, JM21a]. Fine [Dij82d, Hoa10d, Hoa10e, Dij77, Hoa08]. Fine-Grain [Hoa10d, Hoa10e, Hoa08]. Fine-Grained [Dij82d, Dij77]. First [MW08, MS21, AJS05, Ash87]. Fixed [Hoa90b]. Fixpoints [Gut19]. flitting [Hoa04c]. Florida [RNT90]. flow [BBF^{+}05, HW11]. Floyd [AMMO09, BÉ91, CSW89, Pra76, Yin11]. Floyd-Hoare [AMMO09]. Follow [Hoa00a]. forecast [Hoa83a]. Foreword [Hoa76b, Hoa94a]. Form [HHS93]. Formal [BGB09, BHH^{+}06, HL74, Hoa87b, Hoa89b, LWZ13, OKL04, BHL90, Fok87]. formula [Dij99]. Forty [Hoa22]. Foundations [HMSW09b, IEE76, O’D82, HPGM93, HMSW11]. Fourier [MH77]. Fractional [Hoa04a]. Frame [Thi06]. framework [AMMO09]. Framing [BNNN22]. France [WGF13]. Francisco [AdA05]. Free [MH77, FHRR04]. FREng [BO12, HW04]. FRG [BHL90]. FRS [BO12]. Function [KN92]. Functions [CH72, Hoa72d, Hoa90b, ACH76].

Gap [HP94b, HP94a]. garbage [Hoa74d]. GC6 [HJR04b]. General [EHP^{+}75b, AMMO09, Csi81, Hoa73b]. generalization [Sti88]. generalized [NH86]. generative [Chl13]. generator [HM95]. Generic [Hoa13a]. genetically [BCK^{+}19]. Geometry [HSW19b, HSW19a]. Georgia [Ryd99]. Germany [Bro96, HP12, HJKM14]. get [Hoa96b]. global [Old84]. Good [Cla79]. GOTO [Lif84]. GPU [KI17]. grail [Hoa03c]. Grain [Hoa10d, Hoa08, Hoa10e]. Grained [Dij82d, Dij77]. Grand [Hoa03g, Hoa04e, HM05, HM08, Hoa03h, Hoa05a, WBC^{+}21]. grape [Hoa04c]. Graph [PP12]. Graphical [WHO09, ZLW^{+}19]. graphically [PJ89]. graphs [Hoa79]. gratitude [Dij77, Dij82d]. Gries [Sti88]. Guarantee [HM19]. guards [GP94]. Guest [Hoa72a, Hoa94b]. guide [Hoa70b].

H [Bro73]. Hall [Ano87, Hor89]. Hamburg [HP12]. hand [Hoa10b]. handling [CD82, Hoa65b, Hoa68f, Szc91]. Hard [Hoa00a]. hardback [Hor89]. Hardware [HP94b, HP94a, GH92]. healthiness [HH00]. Hedges [Str21]. held [BS76, Bro96, EN74, GH92]. Help [Hoa93c]. Hemel [Hor89]. Hempstead [Hor89]. Hierarchical [DH72, Dij71]. hierarchies [BS76]. High [Hoa73c, Hoa76c]. Higher [DJ83, Nau95, SLN07, TDB13]. higher-order [Nau95, SLN07, TDB13]. highly [VHHS06]. highly-concurrent [VHHS06]. Hints [Hoa73d, Hoa73e, Hoa73f, Hoa74b, Hoa75b, Hoa76d]. Historic [BD01, JL11]. histories [BGP11]. Hoare [Ano87, Bar75, Bar74, BO12, Bro73, Hor89, Pri79, dOSRS19, Ano07a, Ano07b, Anoxx, Apt81, AO19, AO21, AMMO09, AMO13, ACH76, Bae65, BGB12, BT82a, BT82b, BT82c, BT83, BT84b, BT84a, BK84, BCK^{+}19, BÉ91, BGP11, CCC^{+}17, CK79, CSW89, Chl13, Cla79, CGH83, Coe95, CK00, DH94, DJ83, DW84, DRW00, Day12b, DHD97, DN13, Dij70, Dij74, Dij75, Dij77, Dij82d, Dij82a, Dij82b, Dij89, Dij99, Dijxx, ED96, FY21, FM90, FKMJ12, Fra02, GSWZ08, GM81, GP94, GR96, Grü98, HV02, Hoa80a, Hoa82b, Hoo91, Hoo92, Hoo94, HGRA89, HJ00, Jac15, JRW10, Jon21, JM21f, Kir82, KP98, Kle99, KN92, KI17, Koz00, Krá66, Lam80, LS84, Llo74, Mam16, MP88, NMB06, NMB08, NS77, Nie87, Nip02, O’D82, Old81, Old83b]. Hoare [PP12, Pra76, Pro95, RWH01, Rod85, Ros94, SU07, SNBD16, Shu09, S^{+}67, Sok87, SD16, Sti88, Sun96, Szc91, Tak87, TDB13, Wan76, Wan78, Woo21, XSZ16, Yin11, dB02, dBH21, dH08, vH85, vO01, vON02]. Hoare-calculi [Kir82]. Hoare-like [BT82b, Nie87, Old81, Szc91]. Hoare-Logic [DJ83]. Hoare-Style [PP12, DHD97, DN13, SNBD16, TDB13]. Hoares [Apt84]. Hoc [WZX19]. HOL [vO01]. holy [Hoa03c]. honour [DRW00, Ros94]. horizons [HJR04b, HJR04a]. horizontal [DW84]. Houston [IEE76]. Hrsg [Bro73]. Hybrid [Fos19].

ICCSW’13 [JN13]. idea [Fet88]. Ideal [Ano07a, Ano07b, Hoa07b, Hoa06a]. If [Lew97]. IFIP [MW08]. Ignore [Wel97]. II [Apt84, BHL^{+}96, EHP^{+}75b, HH86c]. III [HBS01, EHP^{+}75c]. Impact [AO21]. imperative [NMS^{+}08]. Imperial [JN13]. Implementation [EHP^{+}75a, EHP^{+}75b, EHP^{+}75c, Ryd99]. implementations [Hoa82a]. Impossible [Cla79]. Imprecise [PRH^{+}99, JRH^{+}99]. Inadequacy [BG01]. inaugural [Hoa71a, Hoa86b]. inclusion [BK84]. Incompleteness [Wan78, Wan76]. Incomputability [HA72]. increasing [Hoa90b]. independent [vA98]. Index [JM21d]. indirect [Hoa65a]. inductive [CSW89]. Industrial [BF10]. Inform [Pet91, San05, VT90]. Infotech [Bat76]. initiative [HMLS09, HMLS21]. Inmos [May21]. Inner [But19]. input [Hoa63b]. input/output [Hoa63b]. inputs [XSZ16]. Insecurities [WSH77]. Institute [Bro96]. Intelligent [BHH^{+}06]. Intensive [BGHH05]. interesting [Hoa00c]. interface [MH15]. interfaces [BS76]. International [AdA05, Ano87, BJM09, BHL90, BF10, GN12, HP12, HJKM14, Hor89, IEE02, Kap92, dOSRS19, RNT90, WGF13, BS76, EN74]. Interpretation [KN92]. Interpreting [Mil90]. Interview [Fra02, JM21c, Shu09, BO12]. Introduction [Hoa77b, Sha93]. introductory [Hoa76h]. invariance [Pet91]. invariant [Pet91, VT90]. invariants [BG01]. invited [AJS05, Hoa00b, Hoa06a]. Ireland [HP72]. Iris [Hoa04c]. Isabelle [Fos19, vO01]. Isabelle/HOL [vO01]. Isabelle/UTP [Fos19]. ISBN [Hor89]. Isn’t [Ols97]. Issue [HM21, HM09]. Item [DDG^{+}70]. Iteration [BÉ91].

J [Bar75, Bar74, Llo74, Pri79]. J. [Dij77, Dij82d]. Jackson [Hoa10a]. Java [HJ00, Lew97, Ols97, RWH01, SL97, vO01]. Jifeng [LWZ13]. Johan [OKL04]. Jones [Hor89]. Journal [Hoa07b]. JSD [SH85]. July [AJS05, BS76, Bro96, HBS01, IEE88, Dij74]. Jumps [ACH76, CH72]. June [BD01, GN12, HP12, Kap92, LL08].

KDF9 [Hoa64a]. Kernels [KI17]. Key [HH97c]. Keynote [Hoa90c, HH90e, Hoa91e, Hoa78e]. Kiel [BHL90]. King [Hoa03c]. Kingdom [Hor89, JN13]. Kleene [BJM09, BJM09, HMSW09a, HMSW09b, HMSW11, HvSM^{+}14, HvSM^{+}16, Koz00]. knights [Hoa03c]. Knuth [Dij77, Dij82d].

Language [CK79, Cla79, DJ83, EHP^{+}75b, HW72, HW73, Hoa73d, Hoa73e, Hoa73f, HW74, HMM05, Ker84, Ryd99, Hoa72g, Hoa74a, Hoa74b, Hoa75b, Hoa76d, Hoa89d, HHBP90, Ker81, Sti88, Szc91, BS76, Hoa96f]. Languages [EHP^{+}75a, EHP^{+}75b, EHP^{+}75c, FG84, HL74, HS85, BT84a, HH90a, Hoa68d, Hoa70b, Hoa73c, Hoa76c, HH90c, SU07, Hoa70b]. LASER [Mül10]. Lauer [GM81]. law [Hoa73b, HHM^{+}11]. Laws [HHH^{+}87a, HHH^{+}87b, HHJ^{+}92, Hoa93c, HvS12b, Hoa13a, Hoa13b, Hoa14, RH86, HvS14, RH88]. LCF [Sok87]. Learning [Hoa02h]. lecture [Hoa71a, Hoa86b, Hoa07b, Hoa21b]. lectures [Mül10, Ash87]. Legacy [AH22, Hoa00b, Hoa01c]. Let [Hoa90c]. Lett [Pet91, VT90]. Letter [Dij70, Hoa66a, Hoa68c, Hoa82b, Pet91, Dij74, Dij75, Dij82b]. Letters [GR97, McR97, Ols97, SL97, Wel97]. level [Hoa68b, Hoa73c, HHBP90, SU07]. Life [AH22, JM21f, Hoa00c]. Like [HV02, BT82b, Hoa04d, LV96, Nie87, Old81, Old84, Szc91, Old83b]. Limitations [Hoa68d]. linear [AMO13]. linearisable [VHHS06]. linearizable [SNBD16]. Linking [HH97a, HH99a, HH05]. List [Jon21, vd86].

List-Copying [vd86]. Local [GSWZ08]. locality [HHM^{+}11]. Logic [Apt81, AO21, BNNN22, BT82c, BT84b, BÉ91, BP03, DJ83, FY21, HV02, HS85, HO08, HSW19b, HJ00, IEE88, Kle99, KN92, KI17, Lam80, LS84, Mam16, Sok87, dBH21, vON02, Apt84, AO19, AMO13, BN10, BT82a, BT82b, BT83, BT84a, BK84, BCK^{+}19, BBC08, CCC^{+}17, Chl13, Coe95, CK00, DW84, Day12b, ED96, GP94, HG88, Hoa96c, HH01, HSW19a, Hoo91, Hoo94, HGRA89, Koz00, MP88, Old83b, Pra76, Rod85, SU07, SSH99, SD16, Sti88, Sun96, Tak87, TDB13, WHO09, XSZ16, Yin11, dB02, dH08, vO01]. Logics [BGB12, CGH83, Nip02, O’D82, AMMO09]. London [AJS05, Ano76, Ano87, Bar75, JN13]. Long [BHF05]. Long-Running [BHF05]. loop [BG01]. love [Hoa02h]. low [SU07]. low-level [SU07].

M [Hoa70b]. M. [ACH76]. M1 [Bro76, FR75]. Machine [Hoa61d, BY92, Hoa04d]. Machines [Baz63, Bae65]. Madrid [GN12]. mail [HH86a, HH87b, HJ91]. make [Hoa90c]. Making [Dij82d, Dij77]. management [HM72a, HM72b]. mandatory [SLN07]. Manifesto [HMLS21, HMLS09]. manipulation [Hoa68g]. manual [Spi89]. March [HW04, RNT90]. Marienstatt [HJKM14]. Markov [Grü98]. Marktoberdorf [BS76, Bro96, HBS01]. Massachusetts [ACM83]. Mathematical [Bae65, Baz63, HS85, Hoa93c, Hoa96d, Day12b, Hoa81c]. Mathematics [GN12, Hoa86a, Hoa93c, Hoa85c, Hoa86b]. Maths [Hoa86c]. Matrix [JH75]. May [HJKM14, Ryd99, VT90]. means [Fok87]. mechanically [HM95]. mechanism [CD82, Szc91]. Mechanized [GH92, dH08]. Meeting [Hoa99, GH92, Hoa93e]. members [Hoa66a]. memoriam [BFG^{+}02]. Memory [MP10, OKL04]. men [Hoa73h]. menu [EHT87]. menu-dialog [EHT87]. Message [Hoa12a, Hoa12b, SS95]. message-passing [SS95]. metaprogramming [Chl13]. Method [Hoa61d, JH75, NS77, Pri79]. Methods [BHH^{+}06, BJM09, Hoa87b, HJKM14, LWZ13, OKL04, Wel97, vON02, BHL90, CSW89, Hoa89b, SLN07]. Miami [RNT90]. Michael [HW04, Hoa10a]. Microcomputer [EM81]. microprocessor [BY92, BY96]. microprograms [DW84]. Microsoft [DRW00]. Middle [Hoa99]. Millennial [DRW00]. Mind [Ros94]. Minority [DDG^{+}70, WTD^{+}69]. Mobile [WZX19]. modality [Win85]. Model [EHT87, HH99b, GB96, HH83, Hoa80b, Hoa80c, Hoa81d, HZ90, HJ99, MH15, NH86, SLN07, XSZ16, ZH92]. modelling [ZLW^{+}19]. Models [BP03, Hoa93b, Hoa12c, Hoa13a, RWH01, Hoa90c, Hoa92, Hoa93a, Hoa95, Hoa96a, Hoa96d, HW11, Hoo91, WHO09]. modern [Hoa02j]. modified [BCK^{+}19]. modifying [BN10, CSV07]. Modular [SLN07]. Monadic [Mam16, Jac15]. monads [Jac15]. Monitor [Wel97]. Monitors [Hoa74c, Hoa02e]. MOS [HG88, Hoa90d, Hoa91c, Hoa91d]. MPC [GN12]. MR [Pri79]. Multiple [Pro95]. Multiprocessors [EH89]. mutual [PJ89]. My [Ker84, Ker81].

Name [Cip00]. NanoJava [vON02]. NATO [Bro96, HBS01]. natural [BT82b, SU07]. Needham [HW04, HJ04]. Net [Hoa12c]. Nets [HP12]. network [HM85, MH85]. Networks [EM81, WZX19, dB02]. Neuhold [Pri79]. Newnes [Hoa70b]. Newnes-Butterworths [Hoa70b]. News [DDG^{+}70]. No [Bar75, HHH^{+}87a, Pri79]. non [HK80, SNBD16]. non-determinism [HK80]. non-linearizable [SNBD16]. Nondeterminism [Apt84, Nip02, FHdR78, FHLdR79, KH80]. Nondeterministic [Mam16, HGRA89]. nonstandard [HGRA89]. Normal [HHS93]. Northern [HP72]. notation [Spi89]. Note [Hoa72b, Krá66, CK00, Hoa65a]. Notes [Dij72, Hoa72c, Hoa83d, Hoa85d, Hoa86d, Hoa89c]. notion [Old83a]. novelties [Hoa85b]. November [BJM09]. Novosibirsk [EN74]. NY [Kap92]. nye [Kho89].

O [Bar75, Llo74]. O. [Bar74]. O.-J [Bar75, Llo74]. Object [Hoa12c, OKL04, BY96, NH86]. Object-Orientation [OKL04]. objectives [Hoa72d]. Objects [HH99b, HJ99, SNBD16, VHHS06]. Obtain [Cla79]. occam [Hoa91f, May21, RH86, RH88]. Occasion [JL11, LWZ13, AJS05, Dij82a, dOSRS19]. OCL [RWH01]. OCL-Constrained [RWH01]. October [GH92, Hoa86b, IEE76, MW08, dOSRS19]. Oh [Wei88]. Old [Hoa81f, Hoa87c]. Ole [OKL04]. Ole-Johan [OKL04]. one [Mil90]. Online [Gra21]. Open [Hoa82b, Dij75, Dij82b]. Operating [Bro73, Hoa72d, Hoa74c, HM82, Hoa02e, Hoa76g, HP72]. Operational [Aic19, HS94, vSH13, HH93, HHS97, HJS00, Rid09]. optimisation [JTH01]. Optimization [Hoa74d]. Orchestration [HMM05]. order [MS89, MHH91, Nau95, SLN07, TDB13]. ordered [SS95]. Ordering [Dij71]. Orientation [OKL04]. Oriented [OH86, OH83]. Origin [Bri02]. Original [BD01]. our [FvGGM90]. Outer [But19]. output [Hoa63b]. Overview [Hoa87b, KNM94]. Owicki [Sti88]. Oxford [DRW00, IEE02, Hoa86b, Suf21].

Pacific [IEE00]. pages [Bar75, Ano87]. paging [Hoa73g]. Paper [GM81, Pri79]. Papers [MW08, Ano76, WGF13, AJS05]. parable [Hoa74e]. Parallel [Hoa72h, Hoa75c, Hoa76e, HPGM93, HH97b, Hoa02g, Hoa80d, LV96, RNT90]. parameters [Hoa71b]. PARBASE [RNT90]. PARBASE-90 [RNT90]. Paris [WGF13]. PART [BF10, HM72a, HM72b, Ano76, Apt81]. Partial [HZ81, HG88, KN92, ZH81]. Partition [Hoa61a]. PASCAL [HW72, Hoa74a, Old84, FG84, HW73, Ker81, Ker84, Old83b, WSH77, HW74]. PASCAL-like [Old84, Old83b]. pass [Hoa66c]. passing [SS95]. Peano [BT83]. peeled [Hoa04c]. Perrot [Bro73]. Personal [Dij82c, Hoa91f, Hoa02a, Hoa03b, Hoa96j]. Perspective [Aic19, Dij82c, Hoa02a, Hoa03b, JaJ00]. perspectives [DRW00]. Peter [Hoa70b]. Petri [HP12]. Physical [ZLW^{+}19]. pictures [Dij99]. Pioneers [BD01, BD02, Wei88, BD01]. PL [Hoa66b]. PL/I [Hoa66b]. Playing [JTH01]. PLDI [Ryd99]. Pnueli [MP10]. PODS’08 [LL08]. Pointers [HH99b, HJ99, NS06, Thi06]. points [Hoa90b]. policies [BN10]. Polymorphism [NMB06, NMB08]. Port [Sil81]. Porto [dOSRS19]. Portugal [dOSRS19]. posledovatel′ [Kho89]. possess [BT82b]. possible [TT91]. possible-world [TT91]. power [FM90]. powerdomains [Win85]. pp [Pet91, VT90]. Practical [BR21, Sha06, Hoa70b, JTH01]. Practice [BF10, Hoa02i, Hoa02j]. praise [HvS12a]. Pre [MHH91]. Pre-adjunctions [MHH91]. Predicate [Hoa78f, Nau95, Dij82a]. predicates [Dij82a, HR84, Hoa84b, Hoa85e, Hoa93d]. Preface [Hoa86e, Hoa96e, Hoa96f, Hoa96g, Hoa96h, HM09, HM21, JM21b, Hoa96f]. Prentice [Ano87, Hor89]. Prentice-Hall [Ano87, Hor89]. presence [CCC^{+}17]. Presentation [BO12]. Presentations [Bae65]. presented [Ano76]. Prespecification [HH85, HHS87, HH86b, HH86c, HH87c]. Press [Bar75]. Price [Bar75, Hor89]. Principles [LL08]. Probabilistic [BGB12, HV02, WCF^{+}19, HH97a, HH99a, dH08]. problem [CSW89]. problems [PJ89]. Procedure [Bri02]. Procedures [DJ83, Hoa71b, Nip02, Fok87, Old83b, Old84]. Proceedings [ACM76, HP72, HBS01, Bro96, DRW00, IEE88, ACM83, AdA05, BJM09, BF10, GN12, HP12, HJKM14, IEE00, LL08, Ryd99, BHL90, Kap92, dOSRS19, RNT90]. Process [BR21, GP94, Hoa05b, Hoa05c, HvS12b, Pet91, VT90, HvS14]. Processes [BHR84, Dij71, Hoa78c, Hoa78b, Hoa81b, HZ81, Hoa85a, Hoa87a, Hoa02d, HO08, Hoa21a, KH82, OH86, AJS05, EHT87, HH83, Hoa78a, Hoa80b, Hoa80c, Hoa80d, Hoa81a, Hoa81d, HZ82, Hoa83d, Hoa91a, HHM^{+}11, JHH89, OH83, ZH81, dB02, Hoa83c, Ano87]. processing [HPGM93]. ProCoS [HHBP90, BHL^{+}96]. produce [Hoa04a]. profession [Hoa83e]. Professionalism [Hoa81e]. Professor [DRW00, Dij70, HJ16]. Program [Ano07a, Ano07b, ACH76, BNNN22, CH72, Fet88, Hoa71d, Hoa75d, Hoa87b, Hoa07b, HJ00, vA98, vd86, BK84, BBC08, Bro96, Chl13, Csi81, DH72, FH71, GN12, Hoa71c, Hoa72e, Hoa02b, MS89, NS77, Pri79]. Programmers [Hoa93c]. Programming [Bat76, Bri02, CK79, Cla79, DDH72, EN74, FG84, Hoa69, HW72, Hoa72h, HW73, Hoa73d, Hoa73e, Hoa73f, HW74, HL74, Hoa83b, Hoa83e, Hoa84a, HS85, Hoa86a, HHJ^{+}92, Hoa93c, Hoa94c, Hoa97, HH97b, HH98, Hoa99, Hoa01a, Hoa02c, Hoa02i, Hoa02g, HvS12b, Hoa13a, JM21f, KPH76, Ker84, LWZ13, O’D82, Ryd99, WGF13, Woo21, BT84a, Chl13, Dij72, Dij76, HH90a, HH97a, HH99a, Hoa64c, Hoa70b, Hoa72g, Hoa73a, Hoa73c, Hoa74a, Hoa74b, Hoa75b, Hoa75c, Hoa76c, Hoa76d, Hoa76e, Hoa76h, Hoa80a, Hoa81c, Hoa85c, Hoa86b, HHH^{+}87a, HHH^{+}87b, Hoa89d, HHBP90, HH90c, Hoa96f, HH01, Hoa09, Hoa13b, Hoa13c, Hoa14, HvS14, Ker81, NS06, dOSRS19, RH86, RH88, SSH99, Bar74, Hoa96e, Bar75, Llo74]. programmirovanie [DDH75]. Programs [BT84b, Csi81, GM81, HV02, HR84, Hoa84b, Hoa85e, Hoa93d, JMS87, Lam80, NN19, PP12, BT82b, BY92, CSW89, Hoa82a, Hoa86c, Hoa08, HGRA89, LV96, Lif84, NMS^{+}08, Nau95, Nie87, Old83b, Old84, SLN07, Sha06, SS95, Yin11]. Progress [Gut19]. Project [HM08, BHL^{+}96, MS21]. Proof [FH71, Hoa71c, Hoa71d, Hoa72f, Hoa72e, Hoa76f, Hoa96b, Hoa01b, Hoa02f, JMS87, Sok87, DHD97, Fok87, HH87a, HH86a, HH87b, HJ91, KNM94, Nie87, VT90, Ver87, Hoa96g]. Proofs [BGB12, Hoa87a, BGB09, BY92, BY96, BBC08, Gar95, Hoa75d, Hoa91a, LV96, Sha06, dH08]. Properties [Hoa78f, HH86a, SD16]. Proposal [Krá66, HW66]. propositional [CK00, Hoa85b]. Prospects [Hoa72g]. Protocols [HZ81]. prototyping [HHBP90]. protsessy [Kho89]. Provably [HHF^{+}94]. proves [HH90d, HH90e, HH92]. Proving [ACH76, BK84, CH72, VHHS06, CSW89, Hoa10b]. Publications [Bae65, Jon21]. purpose [Hoa72d].

Qatar [BJM09]. quality [Hoa72a]. Quantum [FY21, Yin11]. Quasiparallel [KPH76]. Queen [HP72, Hoa71a]. quest [Hoa03c]. Question [Lew97]. questions [Rod85]. queueing [Hoa73b]. quick [Pri79]. quick-sort [Pri79]. Quickselect [Pro95]. Quicksort [JaJ00, FH71, FKMJ12, Hoa61b, Hoa62a, Hoa96h, NS77].

R [Ano87, ACH76, Bae65, Bar75, Bar74, Bro73, Dij70, Dij74, Dij75, Dij77, Dij82d, Dij82a, Dij82b, Dijxx, Hoa82b, Hor89, JRW10, Llo74, Ros94, Shu09]. R. [Pri79]. RAMiCS [HJKM14]. Randell [JL11]. reactive [DHD97]. Real [EHP^{+}75a, EHP^{+}75b, EHP^{+}75c, Hoo92, Hoa75b, Hoa76d, Hoo94]. Real-Time [EHP^{+}75a, EHP^{+}75b, EHP^{+}75c, Hoo92, Hoa75b, Hoa76d, Hoo94]. Realizations [RWH01]. Reasoning [Sha93, dBH21, vH85, CSW89, DN13, GSWZ08, GH92, Pet91, TDB13]. receipt [Hoa12a, Hoa12b]. Recommendation [Hoa68e]. Record [Hoa65b, Hoa68f, Dijxx]. Recovery [Hoa11, HH87a]. Recursion [Mam16]. Recursive [Hoa75e, Nip02, FH71]. Reduction [JH75]. redundant [MP88]. reference [Spi89]. refined [HHS86]. Refinement [HH90d, HH90e, HH92, HHS86, HH90b, HHS87, Hoa90a, TDB13]. refinements [vA98]. Reflections [JRW10]. regular [HGRA89]. relation [GB96]. Relational [BNNN22, BGB12, BJM09, HJKM14]. Relations [BJM09, Fos19]. relative [Rod85]. Relatively [DJ83]. Reliability [BGH07, Hoa75a]. Reliable [Hoa96b]. RelMiCS [BJM09]. Rely [HM19]. Rely/Guarantee [HM19]. Remark [Bro76]. Remarks [ACH76]. Remote [Bri02]. Report [Bat76, DDG^{+}70, Hoa62b, Hoa68e, WTD^{+}69, BHL^{+}96]. repository [BHW06]. Representations [Hoa01b, Hoa02f, Hoa72f, Hoa76f, Hoa96g]. Reprint [Hoa83b, Hoa83c]. Research [BF10, Hoa03g, Hoa04e, HM05, BHL^{+}96, CSA^{+}96, Hoa03h, Hoa05a]. Researcher [Anoxx]. Resources [Gra21]. Responses [Ano07b]. Result [Wan78, Wan76]. resume [HHS86]. retract [HH10]. Retrospective [Hoa09]. Review [Ano87, Bar75, Bar74, Hoa70a, Hoa70b, Hoa77a, Hor89, Llo74, Bro73, Hoa64a]. Reviews [Hoa63a]. Revised [AJS05, MW08, WGF13]. Revisited [vON02, Kir82]. Rewriting [JTH01, Sun96]. Richard [BO12, Dij99, Fra02]. RoboChart [WCF^{+}19]. robust [GB96]. Roger [HJ04, HW04]. role [Hoa73h]. Roles [BGP11]. Royal [Dij82a, GH92]. rule [Old83a, Tak87]. Rules [JMS87, Old81, CD82, JTH01, Thi06]. Running [BHF05].

Safety [BLH11, Hoa86c, SD16]. Said [McR97]. Salute [FvGGM90]. San [AdA05]. Sanderson [Hoa70b]. Saratoga [Kap92]. Schemes [Mam16]. School [HBS01, BS76, JH75, Mül10]. Science [Hoa76a, Hoa84a, Hoa89a, Hoa96i, HBS01, Hoa07c, HJKM14, IEE76, IEE88, BJM09, DRW00, Hoa71a, Hoa96d, HB98, Hor89]. Sciences [HBS01]. Scientific [EH89, Hoa02i]. Scientists [Hoa89c]. scope [Hoa72d]. Scotland [IEE88]. sd&m [BD01]. second [MS89]. Security [BGB12, BGH07]. SELECT [Bro76, FR75]. Selected [Dij82c, MW08, WGF13]. Selection [GR96, Grü98]. self [CSV07]. self-modifying [CSV07]. Semantical [Pra76]. Semantics [Aic19, BT84b, BHF05, FHdR78, FHLdR79, GM81, HL74, HS94, HMM05, HO08, OH86, PRH^{+}99, WCF^{+}19, WZX19, HH90a, HH93, HH90c, HHS97, HJS00, Hoa13c, JRH^{+}99, OH83, SU07, TT91]. Semaphores [Bri02]. Seminar [HP72]. Sentences [Hoa61d, vH85]. Separation [HO08, BBC08, NMB06, NMB08, WHO09]. September [Ano76, BF10, HP72, JN13, Pet91]. Sequential [Ano87, BHR84, Dij71, Hoa78c, Hoa78b, Hoa83c, Hoa85a, Hoa86d, Hoa87a, Hoa02d, Hoa21a, KH82, LV96, vKH95, AJS05, EHT87, Hoa78a, Hoa80b, Hoa80c, Hoa81d, Hoa83d, Hoa85d, Hoa91a, ZH81]. Sequential-like [LV96]. Series [HBS01]. service [HM85, HH86a, HH87b, HJ91, MH85]. Set [Hoa68g]. setting [Csi81, HH90b, Hoa90a]. Seventh [IEE00, LL08]. several [Pro95]. shared [DHD97]. shifts [Hoa04a]. Side [vON02]. sieve [Hoa72e]. SIGACT [LL08]. SIGART [LL08]. SIGMOD [LL08]. SIGMOD-SIGACT-SIGART [LL08]. SIGPLAN [Hoa12a, Ryd99, BO12, Hoa12b]. Simple [CK79]. simplified [HM85, MH85]. Simulation [ED96, KH82]. Simulink [ZLW^{+}19]. Simulink/Stateflow [ZLW^{+}19]. Single [Hoa66c]. Sir [DRW00, HJ16, BO12, DH94]. size [Hoa74d]. Smallest [Bro76, FR75]. Smoothed [FKMJ12]. Smyth [FM90]. Society [GH92, Dij82a]. Software [BHH^{+}06, BD01, BD02, BP03, BGHH05, BGH07, BLH11, Day12a, HK21, Hoa74e, Hoa75f, Hoa78d, Hoa78e, HP94b, Hoa96b, HBS01, HM08, HM21, HMLS21, IEE00, IEE02, MW08, MS21, BHW06, BHL90, Hoa72a, Hoa93e, HP94a, HB98, Hoa02j, Hoa06a, HM09, HMLS09, Mül10, RAR^{+}10, Ano76]. solution [PJ89]. Solutions [Dij82d, Dij77]. Some [BT82b, Hoa78f, Hoa87b, Rod85]. Sorcery [Hoa84a]. Sorry [San05]. sort [Pri79]. sorting [Fok87]. Sound [DJ83, Old81, AMMO09, BT82b, Hoa04a]. Soundness [Sok87]. Space [HSW19b, HSW19a]. Spain [GN12]. Special [HM21, HM09]. Specific [EHP^{+}75c]. Specification [BLH11, HK21, HM85, MH85, OH83, OH86, ED96, HH87a, HH86a, HHBP90, RAR^{+}10]. Specification-Oriented [OH86, OH83]. Specifications [Hoa82a, Hoa87a, NN19, HH90d, HH90e, Hoa91a, SNBD16]. specified [SLN07]. Specifying [GM81]. spheres [Hoa04a]. Springs [Kap92]. stacks [BGP11]. standard [XSZ16]. Standardisation [EHP^{+}75a]. Startling [Hoa78d]. State [Bat76, BN10]. state-modifying [BN10]. Stateflow [ZLW^{+}19]. Statement [Hoa72b, Hoa96j]. statements [ED96, Lif84]. step [BHW06]. STOC [ACM76]. store [Hoa68b, HM72a, HM72b, Hoa74d]. Stories [Hoa00c]. Story [Hoa91f]. Strategic [CSA^{+}96]. Strict [Gut19]. Structure [HM82, Hoa76g]. Structured [Bar74, Bat76, DDH72, Hoa76h, Chl13, Dij72, Hoa72e, Hoa73g, Bar75, Llo74]. structures [BT82b, DH72, Hoa68b, Hoa75e]. Structuring [Hoa74c, Hoa02e, Hoa72c]. Strukturnoe [DDH75]. Stuck [FHRR04]. Stuck-free [FHRR04]. Student [JN13]. Students [JM21e]. Studer [Pri79]. Study [Bro96, Hoa10a]. stvuyushchie [Kho89]. Style [O’D82, PP12, DHD97, DN13, SNBD16, TDB13, dH08]. substitution [RAR^{+}10]. Success [AO21, GR97]. Successor [HW66]. suggested [Dijxx]. Summer [HBS01, BS76, Mül10]. Survey [Apt81, Apt84, HM72a, HM72b]. sweet [Hoa04a]. switching [HG88, HZ90, ZH92]. Switzerland [MW08]. Symposium [ACM83, BHL90, DRW00, EN74, IEE76, IEE88, LL08, dOSRS19, WGF13, ACM76, AJS05]. Synchronisation [Hoa80d]. synchronous [HZ90, ZH92]. synchrony [HHJ90]. Syntagmatic [Hoa61d]. Synthesizing [Hoa61d]. System [BGH07, Hoa74c, HM82, Hoa02e, Qia90, Wan78, CCC^{+}17, Chl13, Hoa63b, Hoa64c, Hoa73g, Hoa76g, Hoa89b, KNM94, Nie87, Szc91, Wan76]. Systems [BHH^{+}06, Bro73, BGHH05, BLH11, Cla79, EHP^{+}75a, EHP^{+}75b, EHP^{+}75c, HHF^{+}94, HJ04, HP72, Hoa86d, HBS01, Hoo92, LL08, Sha93, ZLW^{+}19, Ano76, AMO13, DHD97, EHT87, Hoa72d, Hoa85d, MS89, MP88, RAR^{+}10, Rid09].

TAIC [BF10]. talk [Hoa00b, Hoa06a]. Tame [Str21]. Tasks [Hoa93c]. TC [MW08]. Teaching [Suf21]. Tears [MH77]. technique [Hoa10a, JTH01]. Techniques [BF10, HP72, HM72a, HM72b, Bro73]. Technology [HJ04, Hoa76a, Hoa83a]. Tecton [KNM94]. Ten [Apt81, Apt84, McR97]. Term [Sun96]. Termination [HJ00, BBC08]. Testing [Aic19, Hoa10b, BF10]. tests [Koz00]. Texas [IEE76]. text [WTD^{+}69]. th [Bro76, FR75]. thanks [Hoa12a, Hoa12b]. Their [BD01, BT82b, Hoa72d, Hoa76a, RNT90]. Theme [Hoa82b, Dij75, Dij82b]. Theorems [BT82c]. Theoretical [EN74, HPGM93]. Theories [BK90, BÉ91, BGHH05, HL74, Hoa94c, Hoa96i, Hoa97, HH97b, HH98, Hoa99, HBS01, HM08, JM21f, LWZ13, MW08, WGF13, Woo21, HH97a, HH99a, HH00, HH05, Hoa96j, HH97c, HH01, dOSRS19]. Theory [ACM76, ACM83, Bae65, Baz63, BHR84, GR96, HP12, HJ04, Hoa72h, Hoa89c, Hoa02i, Hoa02g, AdA05, EHT87, HHJ90, HK80, HZ90, Hoa90e, Hoa90d, Hoa91e, Hoa91c, Hoa91d, Hoa10a, JHH89, KH80, NMB06, NMB08, ZH92]. there [Hoa81c]. think [Hoa04d]. Third [BHL90, Hoa07b]. thousand [Dij99]. Time [EHP^{+}75a, EHP^{+}75b, EHP^{+}75c, HSW19b, Hoo92, MP10, Hoa75b, Hoa76d, HSW19a, Hoo94, Nie87]. times [Hoa00c]. timetables [JH75]. Tolerant [JMS87]. Tomorrow [Hoa73h]. Tony [HJ16, dOSRS19, Ano07a, Ano07b, Anoxx, Day12b, Dij89, Jon21, JM21f]. Tools [HM08, MW08]. Top [Cip00, Hoa99]. Top-Down [Hoa99]. toppled [Hoa03c]. Total [Hoa81b, Hoa81a, HZ82]. Trace [BHF05, HH99b, HJ99]. Transactions [BHF05, Hoa07a, Hoa10c, Qia90]. Transform [MH77]. Transformations [vd86]. Transformers [Hoa78f, Dij82a, Nau95]. Translation [Hoa61d]. translator [Hoa62b]. Transputer [Hoa91f]. Traub [Dij77, Dij82d]. Tree [HMM05]. tribute [HJ04]. Trick [HS10]. Trimming [Str21]. triple [BGP11]. Triples [Hoo92]. true [Pet91, VT90]. Tuesday [Dij82a]. Turing [Ash87, HJ16, Hoa21b, Day12a]. Tutorial [GM81]. Twenty [LL08, Ash87]. Twenty-Seventh [LL08]. Two [BT82c, BT84a, BBF^{+}05, Hoa68b]. two-level [Hoa68b]. Type [DJ83, NMB06, NMB08]. types [BT84a, NMS^{+}08, Thi06, Win89].

UK [AJS05, BF10]. Unbounded [Nip02]. uncertainty [Hoa02h]. Unification [BK90, Hoa96i]. Unified [But19, Hoa94c, Hoa97, ZLW^{+}19]. Unifies [vSH13]. Unify [HvS12b, HvS14]. Unifying [HH00, Hoa96j, HH97c, HH97b, HH98, HH01, Hoa05b, Hoa05c, HW11, Hoa13c, TDB13, WGF13, Woo21, dOSRS19]. United [Hor89, JN13]. universe [Hoa04c]. University [Hoa71a, HP72, Hoa73h, Hoa86b]. Unraveling [HS10]. USA [AdA05, Kap92]. use [DW84, NS77, Pri79, SS95]. used [BY96]. Using [HV02, Hoo92, Sok87, ZLW^{+}19, BK84, CCC^{+}17, CSW89]. UTP [dOSRS19, WGF13, Fos19, WZX19].

Value [dBH21]. Vancouver [LL08]. variable [DHD97]. Variables [FY21, Kle99, vON02, Old84]. Variations [Dij75, Dij82b, Hoa82b]. varieties [Hoa89d]. various [MS89]. VDM [BHL90, BHL90, Coe95]. verifiable [HHBP90]. Verification [BLH11, Hoa08, HM21, Hoo92, HJ00, MP10, PP12, WBC^{+}21, CD82, DW84, Fet88, Hoa02b, HM09, HM95, Lif84, MS89, NS77, Pri79, SLN07, Szc91]. verifications [Csi81]. Verified [HM08, MW08, BHW06, Hoa06a, HMLS09, HM95, HMLS21, MS21]. verifier [Chl13]. Verifying [HV02, Hoa03e, Hoa03g, Hoa04f, RWH01, Rid09, SS95, Win89, BHW06, Hoa03f, Hoa03h, Hoa05a, SD16]. very [Fet88]. via [HJ00, RAR^{+}10]. Viewpoint [Hoa09]. viii [Ano87]. Virtual [vON02]. Vision [HM08]. Visions [Hoa04c]. VSTTE [MW08]. Vzaimodei [Kho89].

W [Bar75, Bar74, BFG^{+}02, FvGGM90, Llo74]. Was [Lew97]. Watered [Ols97]. way [Hoa73c]. Weak [MS89]. Weakest [HH85, HH86b, HH86c, HH87c]. Weakly [Hoo91]. WG [MW08, Hoa66a]. Which [Cla79, BT82b, PJ89]. while [BT82b, GM81, Sti88]. while-programs [BT82b]. Whitehead [Hoa79]. Whither [NN19]. widely [BY96]. Wijngaarden [Hoa68c]. Windows [GR97]. Windsor [BF10]. Winner [HJ16]. Wirth [S^{+}67]. Without [Hoa96b, Old84]. Work [AH22, JRW10]. Works [JM21f]. Workshop [JN13]. world [TT91]. worth [Dij99]. Writings [Dij82c]. Wybe [AH22, Hoa03d].

Ya [Bae65]. Years [Apt81, Hoa22, McR97, MS21, AJS05, Apt84, AO19, Ash87]. Yes [Hoa04d]. Ynot [NMS^{+}08]. Yu. [Bae65].

Z [BHL90, MH85, Spi89]. Zurich [MW08].

References

Ashcroft:1976:RPP

[ACH76] E. A. Ashcroft, M. Clint, and C. A. R. Hoare. Remarks on Program Proving: Jumps and Functions by M. Clint and C. A. R. Hoare. Acta Informatica, 6(3):317–318, August 10, 1976. CO-DEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic). See [CH72].

ACM:1976:SPE

[ACM76] ACM, editor. STOC ’76: Proceedings of the eighth annual ACM symposium on Theory of computing. ACM Press, New York, NY 10036, USA, 1976. ISBN 1-4503-7414-X. LCCN QA 76.6 A12

1976. URL http://dl.acm.org/citation.cfm?id=800113.

ACM:1983:PFA

[ACM83] ACM, editor. Proceedings of the fifteenth annual ACM Symposium on Theory of Computing, Boston, Massachusetts, April 25– 27, 1983. ACM Press, New York, NY 10036, USA, 1983. ISBN 0-89791-099-0. LCCN QA75.5.A14 1983. ACM order no. 508830.

Abadi:2005:CCT

[AdA05] Martín Abadi and Luca de Alfaro, editors. CONCUR 2005— concurrency theory: 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23–26, 2005, Proceedings, volume 3653 of Lecture Notes in Computer Science. Springer-Ver-lag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2005. ISBN 3-540-28309-9 (paperback), 3-540-31934-4 (e-book). LCCN QA76.58 .I53 2005.

Apt:2022:EWD

[AH22] Krzysztof R. Apt and Tony Hoare, editors. Edsger Wybe Dijkstra: His Life, Work, and Legacy, volume 45 of ACM books. ACM Press, New York, NY 10036, USA, 2022. ISBN 1-4503-9771-9 (paperback), 1-4503-9772-7 (epub), 1-4503-9773-5 (hardcover), 1-4503-9774-3 (e-book). ISSN 2374-6777. xxiv + 550 pp. LCCN DS119 .A685 2022.

Aichernig:2019:TPA

[Aic19] Bernhard K. Aichernig. A testing perspective on algebraic, denotational, and operational semantics. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 22–38. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.6 .U86 2019. URL http://link.

springer.com/.

Abdallah:2005:CSP

[AJS05] Ali E. Abdallah, Cliff B. Jones, and Jeff W. Sanders, editors. Communicating sequential processes. the first 25 years: symposium on the occasion of 25 years of CSP, London, UK, July 7–8, 2004. Revised invited papers, volume 3525 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2005. CODEN LNCSD9. ISBN 3-540-25813-2 (paperback), 3-540-32265-5 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.73.C75 S96

2004eb. URL http://www.springerlink.com/content/978-
3-540-25813-1;   http://www.springerlink.com/openurl.
asp?genre=issue&issn=0302-9743&volume=3525;   http://
www.springerlink.com/openurl.asp?genre=volume&id=doi:
10.1007/b136154.

Arthan:2009:GFS

[AMMO09] Rob Arthan, Ursula Martin, Erik A. Mathiesen, and Paulo Oliva. A general framework for sound and complete Floyd-Hoare logics. ACM Transactions on Computational Logic, 11(1):7:1–7:??, October 2009. CODEN ???? ISSN 1529-3785 (print), 1557-945X (electronic).

Arthan:2013:HLL

[AMO13] Rob Arthan, Ursula Martin, and Paulo Oliva. A Hoare logic for linear systems. Formal Aspects of Computing, 25(3):345–363, May 2013. CODEN FACME5. ISSN 0934-5043 (print), 1433-

299X (electronic). URL http://link.springer.com/article/
10.1007/s00165-011-0180-9.

Anonymous:1976:SSE

[Ano76] Anonymous, editor. Software systems engineering: (papers presented at the European computing conference, part of EURO-COMP ; London, September 1976). Online Conferences Ktd,, Uxbridge, UK, 1976. ISBN 0-903796-15-5. LCCN QA76.6 .E97 1976; TK5104 S98 1976.

Anonymous:1987:BRC

[Ano87] Anonymous. Book review: Communicating Sequential Processes, By C. A. R. Hoare. Prentice-Hall International, London, 1985, viii + 256 pages. Science of Computer Programming, 9(1):101– 105, August 1987. CODEN SCPGD4. ISSN 0167-6423 (print),

1872-7964 (electronic). URL http://www.sciencedirect.com/
science/article/pii/0167642387900281.

Anonymous:2007:DIPa

[Ano07a] Anonymous. Discussion on “The Ideal of Program Correctness” by Tony Hoare. The Computer Journal, 50(3):261–268, May 2007. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-2067

(electronic). URL http://comjnl.oxfordjournals.org/cgi/
content/full/50/3/261;   http://comjnl.oxfordjournals.
org/cgi/reprint/50/3/261. See [Hoa07b, Ano07b].

Anonymous:2007:DIPb

[Ano07b] Anonymous. Discussion on “The Ideal of Program Correctness”: Responses from Tony Hoare. The Computer Journal, 50(3):269–273, May 2007. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (electronic). URL http://comjnl.

oxfordjournals.org/cgi/content/full/50/3/269;   http:/
/comjnl.oxfordjournals.org/cgi/reprint/50/3/269.  See

[Hoa07b, Ano07a].

Anonymous:20xx:THE

[Anoxx] Anonymous. Tony Hoare: Emeritus researcher. Microsoft

Web site., 20xx. URL https://www.microsoft.com/en-us/
research/people/thoare/.

Apt:2019:FYH

[AO19] Krzysztof R. Apt and Ernst-Rüdiger Olderog. Fifty years of Hoare’s logic. Formal Aspects of Computing, 31(6):751–807, December 2019. CODEN FACME5. ISSN 0934-5043 (print), 1433-

299X (electronic). URL http://link.springer.com/article/
10.1007/s00165-019-00501-3.

Apt:2021:ASI

[AO21] Krzysztof R. Apt and Ernst-Rüdiger Olderog. Assessing the success and impact of Hoare’s logic. In Jones and Misra [JM21f], pages 41–76. ISBN 1-4503-8728-4. LCCN QA76.6.

Apt:1981:TYH

[Apt81] Krzysztof R. Apt. Ten years of Hoare’s logic: a survey — Part I. ACM Transactions on Programming Languages and Systems, 3 (4):431–483, October 1981. CODEN ATPSDT. ISSN 0164-0925 (print), 1558-4593 (electronic). See also Part II [Apt84].

Apt:1984:TYH

[Apt84] K. R. Apt. Ten years of hoares logic: a survey. II. nondeterminism. Theoretical Computer Science, 28(1–2):83–109, January 1984. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic). See also Part I [Apt81].

Ashenhurst:1987:ATA

[Ash87] Robert L. Ashenhurst, editor. ACM Turing Award Lectures: the first twenty years, 1966–1985. ACM Press anthology series. ACM Press and Addison-Wesley, New York, NY 10036, USA and Reading, MA, USA, 1987. ISBN 0-201-07794-9. xviii + 483 pp. LCCN QA76.24 .A33 1987.

Baer:1965:RPP

[Bae65] R. M. Baer. Recent publications and presentations: The Theory of Mathematical Machines, by Yu. Ya. Bazilevskii and C. A. R. Hoare. American Mathematical Monthly, 72(2):207, February 1965. CODEN AMMYAE. ISSN 0002-9890 (print), 1930-0972 (electronic).

Barth:1974:BRJ

[Bar74] W. Barth. Book review: O. J. Dahl, W. Dijkstra und C. A. R. Hoare, Structured Programming. Computing, 12(3):285, September 1974. CODEN CMPTA2. ISSN 0010-485X (print), 1436-5057 (electronic).

Barron:1975:BRS

[Bar75] D. W. Barron. Book review: Structured Programming, O.-J. Dahl, E. W. Dijkstra and C. A. R. Hoare, Academic Press, London, 1972. No. of pages: 220. Price: £4.20. Software—Practice and Experience, 5(3):314–315, July 1975. CODEN SPEXBL. ISSN 0038-0644 (print), 1097-024X (electronic).

Bates:1976:SPI

[Bat76] David Bates, editor. Structured Programming: Infotech State of the Art Report. Infotech International Limited, Maidenhead, Berkshire, UK, 1976. ISBN 0-85539-270-3. viii + 495 pp. LCCN QA76.6 .S85.

Bazilevskii:1963:TMM

[Baz63] Jurij Jakovlevič Bazilevskii, editor. Theory of Mathematical Machines. Pergamon Press, New York, NY, USA, 1963. xii + 264 pp. Translation from Russian by C. A. R. Hoare. Translation edited by J. M. Jackson.

Brotherston:2008:CPP

[BBC08] James Brotherston, Richard Bornat, and Cristiano Calcagno. Cyclic proofs of program termination in separation logic. ACM SIGPLAN Notices, 43(1):101–112, January 2008. CODEN SIN-ODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Bruni:2005:CTA

[BBF^{+}05] Roberto Bruni, Michael Butler, Carla Ferreira, Tony Hoare, Hernán Melgratti, and Ugo Montanari. Comparing two approaches to compensable flow composition. In Abadi and de Alfaro [AdA05], pages 383–397. ISBN 3-540-28309-9 (paperback), 3-540-31934-4 (e-book). LCCN QA76.58 .I53 2005.

Bernot:2019:GMH

[BCK^{+}19] G. Bernot, J.-P. Comet, Z. Khalis, A. Richard, and O. Roux. A genetically modified Hoare logic. Theoretical Computer Science, 765(??):145–157, April 18, 2019. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic). URL http://www.

sciencedirect.com/science/article/pii/S030439751830080X.

Broy:2001:PTC

[BD01] Manfred Broy and Ernst Denert, editors. Pioneers and Their Contributions to Software Engineering: sd&m Conference on Software Pioneers, Bonn, June 28/29, 2001, Original Historic Contributions. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2001. ISBN 3-540-42290-0 (print), 3-642-48354-2 (e-book). LCCN QA76.758.

Broy:2002:SPC

[BD02]  Manfred Broy and Ernst Denert, editors.  Software Pi-

oneers: Contributions to Software Engineering. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2002. ISBN 3-540-43081-4, 3-642-48354-2 (ebook), 3-642-59412-3 (e-book), 3-642-59413-1, 3-642-63970-4 (print). 728 pp. LCCN QA76.2.A2 S62 2002. URL

http://aleph.unisg.ch/hsgscan/hm00048094.pdf;   http:
//link.springer.com/10.1007/978-3-642-59412-0;   http:
//www.loc.gov/catdir/enhancements/fy0817/2002070484-d.
html;   http://www.springerlink.com/content/978-3-642-
48354-7;   z3950.loc.gov:7090/Voyager.

Bloom:1991:FHL

[BÉ91] Stephen L. Bloom and Zoltán Ésik. Floyd–Hoare logic in iteration theories. Journal of the ACM, 38(4):887–934, October 1991. CODEN JACOAH. ISSN 0004-5411 (print), 1557-735X (elec-

tronic). URL http://www.acm.org/pubs/toc/Abstracts/0004-
5411/115352.html.

Bottaci:2010:TAI

[BF10] Leonardo Bottaci and G. Fraser, editors. Testing: Academic and Industrial Conference — Practice and Research Techniques: 5th International Conference, TAIC PART 2010, Windsor, UK, September 4–6, 2010, Proceedings, volume 6303 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2010. ISBN 3-642-15584-7 (paperback), 3-642-15585-5 (e-book). LCCN QA76.76.T48 T47 2010.

Boyer:2002:MEW

[BFG^{+}02] R. S. Boyer, W. Feijen, D. Gries, C. A. R. Hoare, J. Misra, J. Moore, and H. Richards. In memoriam: Edsger W. Dijkstra 1930–2002. Communications of the ACM, 45(10):21–22, October 2002. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Blass:2001:ICL

[BG01] Andreas Blass and Yuri Gurevich. Inadequacy of computable loop invariants. ACM Transactions on Computational Logic, 2(1):1–11, 2001. CODEN ???? ISSN 1529-3785 (print), 1557-945X (elec-

tronic). URL http://www.acm.org/pubs/articles/journals/
tocl/2001-2-1/p1-blass/p1-blass.pdf;   http://www.acm.
org/pubs/citations/journals/tocl/2001-2-1/p1-blass/.

Barthe:2009:FCC

[BGB09] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Formal certification of code-based cryptographic proofs. ACM SIGPLAN Notices, 44(1):90–101, January 2009. CODEN SIN-ODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Barthe:2012:PRH

[BGB12] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Probabilistic relational Hoare logics for computer-aided security proofs. Lecture Notes in Computer Science, 7342:1–6, 2012. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (elec-

tronic). URL http://link.springer.com/chapter/10.1007/
978-3-642-31113-0_1/.

Broy:2007:SSR

[BGH07] Manfred Broy, Johannes Grunbauer, and Tony Hoare, editors. Software System Reliability and Security, volume 9 of NATO security through science series. D, Information and communication security. IOS Press, Amsterdam, The Netherlands, 2007. ISBN 1-4294-9223-6 (e-book), 1-4337-0874-4, 1-58603-731-5 (hardcover). ISSN 1574-5589 (print), 1879-8284 (electronic). LCCN

QA76.76R44 S66. URL http://catdir.loc.gov/catdir/toc/
fy0802/2007922976.html.

Broy:2005:ETS

[BGHH05] Manfred Broy, Johannes Grünbauer, David Harel, and Tony Hoare, editors. Engineering Theories of Software Intensive Systems. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2005. ISBN 1-4020-3530-6 (hardcover), 1-4020-3531-4 (paperback), 1-4020-3532-2 (e-book), 1-280-28396-3. LCCN QA76.758 .N385 2004.

Borgstrom:2011:RSH

[BGP11] Johannes Borgström, Andrew D. Gordon, and Riccardo Pucella. Roles, stacks, histories: a triple for Hoare. Journal of Functional Programming, 21(2):159–207, March 2011. CODEN JFPRES. ISSN 0956-7968 (print), 1469-7653 (elec-

tronic). URL https://www.cambridge.org/core/product/
23F4063DD70B051277741864576BF603.

Butler:2005:TSL

[BHF05] Michael Butler, Tony Hoare, and Carla Ferreira. A trace semantics for long-running transactions. In Abdallah et al. [AJS05], pages 133–150. CODEN LNCSD9. ISBN 3-540-25813-2 (paperback), 3-540-32265-5 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.73.C75 S96 2004eb. URL

http://www.springerlink.com/content/978-3-540-25813-1;
 http://www.springerlink.com/openurl.asp?genre=issue&
issn=0302-9743&volume=3525;   http://www.springerlink.
com/openurl.asp?genre=volume&id=doi:10.1007/b136154.

Beckert:2006:ISF

[BHH^{+}06] Bernhard Beckert, Tony Hoare, Reiner Hahnle, Douglas Smith, Cordell Green, Silvio Ranise, Cesare Tinelli, Thomas Ball, and Sriram Rajamani. Intelligent systems and formal methods in software engineering. IEEE Intelligent Systems, 21(6):71–81, November 2006. ISSN 1541-1672 (print), 1941-1294 (electronic).

Bjorner:1990:VVZ

[BHL90] Dines Bjørner, C. A. R. Hoare, and Hans Langmaack, editors. VDM ’90: VDM and Z: formal methods in software development: Third International Symposium of VDM Europe, Kiel, FRG, April 17–21, 1990: proceedings, volume 428 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1990. CODEN LNCSD9. ISBN 0-8186-0853-6 (paperback), 0-8186-4853-8 (microfiche), 0-8186-8853-X (case). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.76.D47 V36 1990. URL http:

//link.springer-ny.com/link/service/series/0558/tocs/
t0428.htm;   http://www.springerlink.com/content/978-
0-387-52513-6;   http://www.springerlink.com/openurl.
asp?genre=issue&issn=0302-9743&volume=428;   https://
link.springer.com/book/10.1007/3-540-52513-0.

Bowen:1996:PIP

[BHL^{+}96] J. P. Bowen, C. A. R. Hoare, H. Langmaack, E-R Olderog, and A. P. Ravn. A Procos II project final report: Esprit basic research project 7071. Bulletin of the European Association for Theoretical Computer Science (EATCS), 59:??, ???? 1996. ISSN 0252-9742.

Brookes:1984:TCS

[BHR84] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. Journal of the ACM, 31(3): 560–599, July 1984. CODEN JACOAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Bicarregui:2006:VSR

[BHW06] J. C. Bicarregui, C. A. R. Hoare, and J. C. P. Woodcock. The verified software repository: a step towards the verifying compiler. Formal Aspects of Computing, 18(2):143–151, June 2006. CODEN FACME5. ISSN 0934-5043 (print), 1433-299X (elec-

tronic). URL http://link.springer.com/article/10.1007/
s00165-005-0079-4.

Berghammer:2009:RKA

[BJM09] Rudolf Berghammer, Ali Mohamed Jaoua, and Bernhard Möller, editors. Relations and Kleene algebra in computer science: 11th International Conference on Relational Methods in Computer Science, RelMiCS 2009, and 6th International Conference on Applications of Kleene Algebra, AKA 2009, Doha, Qatar, November 1–5, 2009, Proceedings, volume 5827 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2009. ISBN 3-642-04638-X, 3-642-04639-8 (e-book). LCCN QA10 .I58 2009.

Bergstra:1984:PPI

[BK84] J. A. Bergstra and J. W. Klop. Proving program inclusion using Hoare’s logic. Theoretical Computer Science, 30(1):1–48, April 1984. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Baeten:1990:CTC

[BK90] J. C. M. Baeten and J. W. Klop, editors. CONCUR ’90 — Theories of Concurrency: Unification and Extension, volume 458 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1990. ISBN 0-387-53048-7, 3-540-53048-7, 3-540-46395-X (e-book). ISSN 0302-9743. vii + 536 pp. LCCN QA267 .C5927 1990.

Broy:2011:SSS

[BLH11] Manfred Broy, Christian Leuxner, and Tony Hoare, editors. Software and Systems Safety — Specification and Verification, volume 30 of NATO Science for Peace and Security Series - D: Information and Communication Security. IOS Press, Amsterdam, The Netherlands, 2011. ISBN 1-60750-710-2 (hardcover), 1-60750-711-0 (e-book). ISSN 1874-6268 (print), 1879-8292 (electronic). LCCN QA76.9.A25 S64 2011; QA76.76.P76 S64 2011.

URL http://www.gbv.de/dms/tib-ub-hannover/655827013.
pdf;   https://ebooks.iospress.nl/volume/software-and-
systems-safety.

Becker:2010:LSM

[BN10] Moritz Y. Becker and Sebastian Nanz. A logic for state-modifying authorization policies. ACM Transactions on Information and System Security, 13(3):20:1–20:??, July 2010. CODEN ATISBQ. ISSN 1094-9224 (print), 1557-7406 (electronic).

Banerjee:2022:RPL

[BNNN22] Anindya Banerjee, Ramana Nagasamudram, David Naumann, and Mohammad Nikouei. A relational program logic with data abstraction and dynamic framing. ACM Transactions on Programming Languages and Systems, 44(4):25:1–25:??, December 2022. CO-DEN ATPSDT. ISSN 0164-0925 (print), 1558-4593 (electronic).

URL https://dl.acm.org/doi/10.1145/3551497.

Black:2012:PSD

[BO12] Andrew P. Black and Peter W. O’Hearn. Presentation of the SIG-PLAN distinguished achievement award to Sir Charles Antony Richard Hoare, FRS, FREng, FBCS; and interview. ACM SIG-PLAN Notices, 47(1):1–2, January 2012. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Broy:2003:MAL

[BP03] Manfred Broy and Markus Pizka, editors. Models, Algebras and Logic of Engineering Software, volume 191 of NATO science series. Series III, Computer and systems sciences. IOS Press, Amsterdam, The Netherlands, 2003. ISBN 1-58603-342-5, 4-274-90589-6 (Ohmsha). LCCN QA76.76.D47 N37 2002.

URL http://books.google.com/books?id=TK1QAAAAYAAJ;

http://books.google.com/books?id=U6VQAAAAMAAJ;   http:
//catalog.hathitrust.org/api/volumes/oclc/53998323.html.

Brookes:2021:CPP

[BR21] Stephen D. Brookes and A. W. Roscoe. CSP: a practical process algebra. In Jones and Misra [JM21f], pages 187–222. ISBN 1-4503-8728-4. LCCN QA76.6.

BrinchHansen:2002:OCP

[Bri02] Per Brinch Hansen, editor. The Origin of Concurrent Programming: From Semaphores to Remote Procedure Calls. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2002. ISBN 0-387-95401-5, 1-4419-2986-X, 1-4757-3472-7, 1-4757-3472-7. x + 534 pp. LCCN QA76.642 .O75 2002. URL

http://link.springer.com/10.1007/978-1-4757-3472-0.

Brockhaus:1973:BRC

[Bro73] M. Brockhaus. Book review: C. A. R. Hoare und R. H. Perrot (Hrsg.), Operating Systems Techniques. Computing, 11(1):99, March 1973. CODEN CMPTA2. ISSN 0010-485X (print), 1436-5057 (electronic).

Brown:1976:RAA

[Bro76] Theodore Brown. Remark on “Algorithm 489: The Algorithm SE-LECT — for Finding the i-th Smallest of n Elements [M1]”. ACM Transactions on Mathematical Software, 2(3):301–304, September 1976. CODEN ACMSCU. ISSN 0098-3500 (print), 1557-7295 (electronic). See [FR75].

Broy:1988:BBC

[Bro88] Manfred Broy. Broadcasting buffering communication. Computer Languages, 13(1):31–47, ???? 1988. CODEN COLADA. ISSN 0096-0551 (print), 1873-6742 (electronic).

Broy:1996:DPD

[Bro96] Manfred Broy, editor. Deductive program design: proceedings of the NATO Advanced Study Institute on Deductive Program Design, held in Marktoberdorf, Germany, July 26–August 7, 1994. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1996. ISBN 3-540-60947-4 (hardcover). LCCN QA76.9.D5 D38 1996.

Bauer:1976:LHI

[BS76] Friedrich Ludwig Bauer and Klaus Samelson, editors. Language hierarchies and interfaces: international summer school [held July 23 to August 2, 1975 in Marktoberdorf], volume 46 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1976. ISBN 0-387-07994-7 (New York), 3-540-07994-7 (Berlin), 3-540-37972-X (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic).

LCCN QA76.6 .L335. URL http://link.springer-ny.com/
link/service/series/0558/tocs/t0046.htm;   http://www.
springerlink.com/content/978-0-387-07994-3;   http://
www.springerlink.com/openurl.asp?genre=book&isbn=978-
3-540-07994-1;   http://www.springerlink.com/openurl.
asp?genre=issue&issn=0302-9743&volume=46.

Bergstra:1982:ECH

[BT82a] J. A. Bergstra and J. V. Tucker. Expressiveness and the completeness of Hoare’s logic. Journal of Computer and System Sciences, 25(3):267–284, December 1982. CODEN JCSSBM. ISSN 0022-0000 (print), 1090-2724 (electronic). URL http://www.

sciencedirect.com/science/article/pii/0022000082900137.

Bergstra:1982:SNS

[BT82b] J. A. Bergstra and J. V. Tucker. Some natural structures which fail to possess a sound and decidable Hoare-like logic for their whileprograms. Theoretical Computer Science, 17(3):303–315, March 1982. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Bergstra:1982:TTA

[BT82c] J. A. Bergstra and J. V. Tucker. Two theorems about the completeness of Hoare’s logic. Information Processing Letters, 15(4): 143–149, October 31, 1982. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Bergstra:1983:HLP

[BT83] J. A. Bergstra and J. V. Tucker. Hoare’s logic and Peano’s arithmetic. Theoretical Computer Science, 22(3):265–284, February 1983. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Bergstra:1984:HLP

[BT84a] J. A. Bergstra and J. V. Tucker. Hoare’s logic for programming languages with two data types. Theoretical Computer Science, 28 (1–2):215–221, January 1984. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Bergstra:1984:ASP

[BT84b] Jan A. Bergstra and J. V. Tucker. The axiomatic semantics of programs based on Hoare’s logic. Acta Informatica, 21(3):293– 320, October 1984. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic).

Butterfield:2019:IOA

[But19] Andrew Butterfield. The inner and outer algebras of unified concurrency. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 157–175. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN

QA76.6 .U86 2019. URL http://link.springer.com/.

Boyer:1992:ACP

[BY92] R. S. Boyer and Yuan Yu. Automated correctness proofs of machine code programs for a commercial microprocessor. In Kapur [Kap92], pages 416–430. ISBN 3-540-55602-8. LCCN QA76.9.A96I57 1992.

Boyer:1996:APO

[BY96] Robert S. Boyer and Yuan Yu. Automated proofs of object code for a widely used microprocessor. Journal of the ACM, 43(1):166– 192, January 1996. CODEN JACOAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Chajed:2017:CFS

[CCC^{+}17] Tej Chajed, Haogang Chen, Adam Chlipala, M. Frans Kaashoek, Nickolai Zeldovich, and Daniel Ziegler. Certifying a file system using Crash Hoare logic: correctness in the presence of crashes. Communications of the ACM, 60(4):75–84, April 2017. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). URL

http://cacm.acm.org/magazines/2017/4/215044/fulltext.

Cocco:1982:MEH

[CD82] N. Cocco and S. Dulli. A mechanism for exception handling and its verification rules. Computer Languages, 7(2):89–102, ???? 1982.

CODEN COLADA. ISSN 0096-0551 (print), 1873-6742 (electronic).

Clarke:1983:EAH

[CGH83] Edmund M. Clarke, Jr., Steven M. German, and Joseph Y. Halpern. Effective axiomatizations of Hoare logics. Journal of the ACM, 30(3):612–636, July 1983. CODEN JACOAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Clint:1972:PPJ

[CH72] M. Clint and C. A. R. Hoare. Program proving: Jumps and functions. Acta Informatica, 1(3):214–224, ???? 1972. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic). See remarks [ACH76].

Chlipala:2013:BSP

[Chl13] Adam Chlipala. The bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. ACM SIGPLAN Notices, 48(9):391–402, September 2013. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Cipra:2000:BCE

[Cip00] Barry A. Cipra. The best of the 20th Century: Editors name top 10 algorithms. SIAM News, 33(4):1–2, May 2000. ISSN 0036-1437.

URL https://archive.siam.org/pdf/news/637.pdf.

Cherniavsky:1979:CCH

[CK79] John C. Cherniavsky and Samuel N. Kamin. A complete and consistent Hoare axiomatics for a simple programming language. Journal of the ACM, 26(1):119–128, January 1979. CODEN JA-COAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Cohen:2000:NCP

[CK00] Ernie Cohen and Dexter Kozen. A note on the complexity of propositional Hoare logic. ACM Transactions on Computational Logic, 1(1):171–174, July 2000. CODEN ???? ISSN 1529-3785 (print), 1557-945X (electronic). URL http://www.acm.org/

pubs/citations/journals/tocl/2000-1-1/p171-cohen/.

Clarke:1979:PLC

[Cla79] Edmund Melson Clarke, Jr. Programming language constructs for which it is impossible to obtain good Hoare axiom systems. Journal of the ACM, 26(1):129–147, January 1979. CODEN JACOAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Coenen:1995:HLV

[Coe95] J. Coenen. Hoare’s logic and VDM. Formal Aspects of Computing, 7(1):91–105, January 1995. CODEN FACME5. ISSN 0934-5043 (print), 1433-299X (electronic). URL http://link.springer.

com/article/10.1007/BF01214625.

Cleaveland:1996:SDC

[CSA^{+}96] Rance Cleaveland, Scott A. Smolka, Rajeev Alur, Jos Baeten, Jan A. Bergstra, Eike Best, Rocco De Nicola, Helen Gill, Roberto Gorrieri, Mohamed G. Gouda, Jan Friso Groote, Tom A. Henzinger, C. A. R. Hoare, Maj. David Luginbuhl, Albert Meyer, Dale Miller, Jayadev Misra, Faron Moller, Ugo Montanari, Amir Pnueli, Sanjiva Prasad, Vaughan R. Pratt, Joseph Sifakis, Bernhard Steffen, Bent Thomsen, Frits Vaandrager, Moshe Vardi, and Pierre Wolper. Strategic directions in concurrency research. ACM Computing Surveys, 28(4):607–625, December 1996. CODEN CMSVAN. ISSN 0360-0300 (print), 1557-7341 (elec-

tronic). URL http://www.acm.org/pubs/citations/journals/
surveys/1996-28-4/p607-cleaveland/.

Csirmaz:1981:PPV

[Csi81] L. Csirmaz. Programs and program verifications in a general setting. Theoretical Computer Science, 16(2):199–210, November 1981. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Cai:2007:CSM

[CSV07] Hongxu Cai, Zhong Shao, and Alexander Vaynberg. Certified selfmodifying code. ACM SIGPLAN Notices, 42(6):66–77, June 2007. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Chisholm:1989:ARP

[CSW89] G. H. Chisholm, B. T. Smith, and A. S. Wojcik. An automated reasoning problem associated with proving claims about programs using Floyd–Hoare inductive assertion methods. Journal of Automated Reasoning, 5(4):533–540, December 1989. CODEN JA-REEW. ISSN 0168-7433 (print), 1573-0670 (electronic). URL

http://link.springer.com/article/10.1007/BF00243137.

Daylight:2012:DSE

[Day12a] Edgar G. Daylight. The Dawn of Software Engineering: from Turing to Dijkstra. Lonely Scholar, Heverlee, Belgium, 2012. ISBN 94-91386-02-6. vi + 239 pp. LCCN QA76.17 .D38 2012. Edited by Kurt De Grave.

Daylight:2012:THM

[Day12b] Edgar G. Daylight. Tony Hoare and mathematical logic. In The Dawn of Software Engineering: from Turing to Dijkstra [Day12a], chapter 4, pages 79–104. ISBN 94-91386-02-6. LCCN QA76.17 .D38 2012. Edited by Kurt De Grave.

deBoer:2002:HLD

[dB02] F. S. de Boer. A Hoare logic for dynamic networks of asynchronously communicating deterministic processes. Theoretical Computer Science, 274(1–2):3–41, March 6, 2002. CO-DEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

URL http://www.elsevier.com/gej-ng/10/41/16/227/27/28/
abstract.html.

deBoer:2021:CCR

[dBH21] Frank S. de Boer and Hans-Dieter A. Hiep. Completeness and complexity of reasoning about call-by-value in Hoare logic. ACM Transactions on Programming Languages and Systems, 43(4): 17:1–17:35, December 2021. CODEN ATPSDT. ISSN 0164-0925 (print), 1558-4593 (electronic). URL https://dl.acm.org/doi/

10.1145/3477143.

Dijkstra:1970:NIM

[DDG^{+}70] Edsger W. Dijkstra, ?. Duncan, Jan V. Garwick, C. A. R. Hoare, Brian Randell, G. Seegmueller, Władisław M. Turski, and Michael Woodger. News item — minority report. ALGOL Bulletin (Amsterdam: Mathematisch Centrum), 31:7, March 1970. CODEN ALGOBG. ISSN 0084-6198. Item AB31.1.1.

Dahl:1972:SP

[DDH72] Ole-Johan Dahl, Edsger W. Dijkstra, and C. A. R. (Charles Antony Richard) Hoare, editors. Structured Programming, volume 8 of A.P.I.C. Studies in Data Processing. Academic Press, New York, USA, third edition, 1972. ISBN 0-12-200550-3 (hardcover), 0-12-200556-2 (paperback). viii + 220 pp. LCCN

QA76.6 .D33 1972. URL https://dl.acm.org/doi/pdf/10.

5555/1243380. Second printing.

Dahl:1975:CSP

[DDH75] Ole-Johan Dahl, Edsger Dijkstra, and C. A. R. Hoare, editors. Strukturnoe programmirovanie. Matematicheskoe Obespechenie ÈVM. [Monographs in Mathematical Computer Software]. Izdat. “Mir”, Moscow, USSR, 1975. ISBN 2-01-507541-0. 247 pp. Translated from the English by S. D. Zeleneckiĭ, V. V. Martynjuk and L. V. Uhov, Edited by È. Z. Ljubimskiĭ and V. V. Martynjuk.

Dahl:1972:HPS

[DH72] Ole-Johan Dahl and C. A. R. Hoare. Hierarchical program structures. In Dahl et al. [DDH72], chapter III, pages 175–220. ISBN 0-12-200550-3 (hardcover), 0-12-200556-2 (paperback). LCCN

QA76.6 .D33 1972. URL https://dl.acm.org/doi/10.5555/

1243380.1243383. Second printing.

Dale:1994:CST

[DH94] Tony Dale and C. A. R. Hoare. A conversation with Sir Tony Hoare. Web site, 1994. URL https://www.infoq.com/

interviews/tony-hoare-qcon-interview/.

denHartog:2008:TMC

[dH08] Jerry den Hartog. Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic Hoare style logic. Science of Computer Programming, 74(1–2):52–63, December 1, 2008. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic).

DeBoer:1997:HSC

[DHD97] F. S. De Boer, U. Hannemann, and W.-P. De Roever. Hoarestyle compositional proof systems for reactive shared variable concurrency. Lecture Notes in Computer Science, 1346:267– ??, 1997. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-

3349 (electronic). URL http://link.springer-ny.com/link/
service/series/0558/bibs/1346/13460267.htm;   http://
link.springer-ny.com/link/service/series/0558/papers/
1346/13460267.pdf.

Dijkstra:1970:LPC

[Dij70] Edsger W. Dijkstra. Letter to professor C. A. R. Hoare (31 August 1970). Circulated privately., August 1970. URL http://www.cs.

utexas.edu/users/EWD/ewd02xx/EWD292.PDF.

Dijkstra:1971:HOS

[Dij71] Edsger W. Dijkstra. Hierarchical ordering of sequential processes. Acta Informatica, 1(2):115–138, October 1971. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic). Reprinted in Operating Systems Techniques, C. A. R. Hoare and R. H. Perrot, Eds., Academic Press, 1972, pp. 72–93. This paper introduces the classical synchronization problem of Dining Philosophers.

Dijkstra:1972:NSP

[Dij72] Edsger W. Dijkstra. Notes on structured programming. In Dahl et al. [DDH72], chapter I, pages 1–82. ISBN 0-12-200550-3 (hardcover), 0-12-200556-2 (paperback). LCCN QA76.6 .D33 1972.

URL https://dl.acm.org/doi/pdf/10.5555/1243380. Second

printing.

Dijkstra:1974:LCR

[Dij74] Edsger W. Dijkstra. [a letter to C. A. R. Hoare, 13 July 1974]. Circulated privately., July 1974. URL http://www.cs.utexas.

edu/users/EWD/ewd04xx/EWD432.PDF.

Dijkstra:1975:VTO

[Dij75] Edsger W. Dijkstra. Variations on a theme: an open letter to C. A. R. Hoare. Published as [Dij82b]., July 1975. URL http://

www.cs.utexas.edu/users/EWD/ewd05xx/EWD501.PDF.

Dijkstra:1976:DP

[Dij76] Edsger W. Dijkstra. A discipline of programming. Prentice-Hall Series in Automatic Computation. Prentice-Hall, Upper Saddle River, NJ 07458, USA, 1976. ISBN 0-13-215871-X. xvii + 217 pp. LCCN QA76.6 .D54. With a foreword by C. A. R. Hoare.

Dijkstra:1977:MSM

[Dij77] Edsger W. Dijkstra. On making solutions more and more finegrained (in gratitude dedicated to C. A. R. Hoare, D. E. Knuth, and J. F. Traub.). Published as [Dij82d]., May 1977. URL http:

//www.cs.utexas.edu/users/EWD/ewd06xx/EWD622.PDF.

Dijkstra:1982:PTP

[Dij82a] Edsger W. Dijkstra. From predicate transformers to predicates (Dedicated by the Tuesday Afternoon Club to C. A. R. Hoare at the occasion of his being elected Fellow of the Royal Society). Circulated privately., April 1982. URL http://www.cs.utexas.

edu/users/EWD/ewd08xx/EWD821.PDF.

Dijkstra:1982:VTO

[Dij82b] Edsger W. Dijkstra. Variations on a theme: an open letter to C. A. R. Hoare. In Selected Writings on Computing: a Personal Perspective [Dij82c], pages 132–140. ISBN 0-387-90652-5 (New York), 3-540-90652-5 (Berlin). LCCN QA76.24 .D54 1982. Including a paper co-authored by C. S. Schölten.

Dijkstra:1982:SWC

[Dij82c] Edsger Wybe Dijkstra. Selected Writings on Computing: a Personal Perspective. Texts and Monographs in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1982. ISBN 0-387-90652-5 (New York), 3-540-90652-5 (Berlin). xvii + 362 pp. LCCN QA76.24 .D54 1982. Including a paper co-authored by C. S. Schölten.

Dijkstra:1982:MSMa

[Dij82d] Prof. Dr. Edsger W. Dijkstra. On making solutions more and more fine-grained (In gratitude dedicated to C. A. R. Hoare, D. E. Knuth, and J. F. Traub). In Selected Writings on Computing: a Personal Perspective [Dij82c], pages 292–307. ISBN 0-387-90652-5 (New York), 3-540-90652-5 (Berlin). LCCN QA76.24 .D54

1982. URL http://link.springer.com/chapter/10.1007/978-

1-4612-5695-3_53. Including a paper co-authored by C. S. Schölten.

Dijkstra:1989:ETH

[Dij89] Edsger W. Dijkstra. On an exercise of Tony Hoare’s. Circulated privately., September 1989. URL http://www.cs.utexas.edu/

users/EWD/ewd10xx/EWD1062.PDF.

Dijkstra:1999:FWT

[Dij99] Edsger W. Dijkstra. A formula is worth a thousand pictures (dedicated to Charles Antony Richard Hoare). Circulated pri-

vately., June 1999. URL http://www.cs.utexas.edu/users/
EWD/ewd12xx/EWD1280a.PDF.

Dijkstra:20xx:ERC

[Dijxx] Edsger W. Dijkstra. An experiment with the “record class” as suggested by C. A. R. Hoare. Circulated privately., 20xx. URL

http://www.cs.utexas.edu/users/EWD/ewd01xx/EWD132.PDF.

Damm:1983:SRH

[DJ83] Werner Damm and Bernhard Josko. A sound and relatively ∗complete Hoare-logic for a language with higher type procedures. Acta Informatica, 20(1):59–101, October 1983. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic).

Delbianco:2013:HSR

[DN13] Germán Andrés Delbianco and Aleksandar Nanevski. Hoare-style reasoning with (algebraic) continuations. ACM SIGPLAN Notices, 48(9):363–376, September 2013. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Ribeiro:2019:UTP

[dOSRS19] Pedro (Pedro Fernando de Oliveira Salazar) Ribeiro and Augusto Sampaio, editors. Unifying theories of programming: 7th International Symposium, UTP 2019, dedicated to Tony Hoare on the occasion of his 85th birthday, Porto, Portugal, October 8, 2019: proceedings, volume 11885 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2019. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic).

LCCN QA76.6 .U86 2019. URL http://link.springer.com/.

Davies:2000:MPC

[DRW00] Jim Davies, A. W. Roscoe, and Jim Woodcock, editors. Millennial perspectives in computer science: proceedings of the 1999 Oxford– Microsoft Symposium in honour of Professor Sir Antony Hoare. Palgrave, Basingstoke, UK, 2000. ISBN 0-333-92230-1. LCCN QA75.5 .O8 2000.

Dasgupta:1984:UHL

[DW84] Subrata Dasgupta and Alan Wagner. The use of Hoare logic in the verification of horizontal microprograms. International Journal of Computer and Information Sciences, 13(6):461–490, December 1984. CODEN IJCIAH. ISSN 0091-7036.

Engelhardt:1996:SSS

[ED96] K. Engelhardt and W.-P. De Roever. Simulation of specification statements in Hoare logic. Lecture Notes in Computer Science, 1113:324–335, 1996. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic).

Elliott:1989:SAM

[EH89] R. J. (Roger J.) Elliott and C. A. R. (Charles Antony Richard) Hoare, editors. Scientific Applications of Multiprocessors. Prentice-Hall, Upper Saddle River, NJ 07458, USA, 1989. ISBN 0-13-795774-2. vi + 143 pp. LCCN Q183.9 .S29 1989.

Enslow:1975:ILRa

[EHP^{+}75a] P. H. Enslow, C. A. R. Hoare, J. Palme, D. Parnas, and I. Pyle. Implementation languages for real-time systems — I. Standardisation — its implementation and acceptance. Report ERO-2-75-Vol-1, Euro. Res. Office, London, UK, 1975. URL https://apps.dtic.

mil/sti/citations/ADA008977.

Enslow:1975:ILRb

[EHP^{+}75b] P. H. Enslow, C. A. R. Hoare, J. Palme, D. Parnas, and I. Pyle. Implementation languages for real-time systems — II. language design — general comments. Report ERO-2-75-Vol-2, Euro. Res.

Office, London, UK, 1975. URL https://apps.dtic.mil/sti/
citations/ADA008978.

Enslow:1975:ILRc

[EHP^{+}75c] P. H. Enslow, C. A. R. Hoare, J. Palme, D. Parnas, and I. Pyle. Implementation languages for real-time systems — III. command and control languages — specific comments. Report ERO-2-75-Vol-3, Euro. Res. Office, London, UK, 1975. URL https://apps.

dtic.mil/sti/citations/ADA009081.

Enikeev:1987:MTC

[EHT87] A. I. Enikeev, C. A. R. Hoare, and A. Teruel. Model of a theory of communicating sequential processes for menu-dialog systems. Mathematica, 3(??):??, ???? 1987.

Ekanadham:1981:MN

[EM81] K. Ekanadham and A. Mahjoub. Microcomputer networks. The Computer Journal, 24(1):17–24, February 1981. CODEN CM-PJA6. ISSN 0010-4620 (print), 1460-2067 (electronic). URL http:

//comjnl.oxfordjournals.org/content/24/1/17.full.pdf+
html;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
24/Issue_01/tiff/17.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_24/Issue_01/tiff/18.tif;   http://
www3.oup.co.uk/computer_journal/hdb/Volume_24/Issue_01/
tiff/19.tif;   http://www3.oup.co.uk/computer_journal/

hdb/Volume_24/Issue_01/tiff/20.tif;   http://www3.oup.
co.uk/computer_journal/hdb/Volume_24/Issue_01/tiff/21.
tif;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
24/Issue_01/tiff/22.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_24/Issue_01/tiff/23.tif;   http://
www3.oup.co.uk/computer_journal/hdb/Volume_24/Issue_01/
tiff/24.tif.

Ershov:1974:IST

[EN74] Andrei Ershov and Valery Aleksandrovich Nepomniaschy, editors. International Symposium on Theoretical Programming [held in Novosibirsk, Aug. 7–11, 1972], volume 5 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1974. ISBN 0-387-06720-5 (New York paperback), 3-540-06720-5 (Berlin paperback). LCCN QA76 .I5798 1972.

Fetzer:1988:PVV

[Fet88] James H. Fetzer. Program verification: the very idea. Communications of the ACM, 31(9):1048–1063, September 1988. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (elec-

tronic). URL http://www.acm.org/pubs/toc/Abstracts/0001-

0782/48530.html. Comment 1 by Schlenk, Sun May 21 18:41:04 1989. Discusses two views: Programs can be derived from specs through mathematical methods (Hoare) versus verification as a social process (DeMillo, Lipton, Perlis). There is a response to this paper in CACM April 89.

Feuer:1984:CAP

[FG84] Alan R. Feuer and Narain Gehani, editors. Comparing and Assessing Programming Languages: Ada, C, and Pascal. Prentice-Hall software series. Prentice-Hall, Upper Saddle River, NJ 07458, USA, 1984. ISBN 0-13-154840-9 (paperback), 0-13-154857-3 (hardcover). xiv + 271 pp. LCCN QA76.73.A35 C66 1984.

Foley:1971:PRP

[FH71] M. Foley and C. A. R. Hoare. Proof of a recursive program: Quicksort. The Computer Journal, 14(4):391–395, November 1971. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-

2067 (electronic). URL http://comjnl.oxfordjournals.org/
content/14/4/391.full.pdf+html;   http://www3.oup.co.
uk/computer_journal/hdb/Volume_14/Issue_04/140391.sgm.
abs.html;   http://www3.oup.co.uk/computer_journal/hdb/

Volume_14/Issue_04/tiff/391.tif;   http://www3.oup.co.
uk/computer_journal/hdb/Volume_14/Issue_04/tiff/392.tif;
 http://www3.oup.co.uk/computer_journal/hdb/Volume_14/
Issue_04/tiff/393.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_14/Issue_04/tiff/394.tif;   http:/
/www3.oup.co.uk/computer_journal/hdb/Volume_14/Issue_
04/tiff/395.tif.

Francez:1978:SNC

[FHdR78] Nissim Francez, C. A. R. Hoare, and Willem P. de Roever. Semantics of nondeterminism, concurrency and communication. In Mathematical foundations of computer science, 1978 (Proc. Seventh Sympos., Zakopane, 1978), volume 64 of Lecture Notes in Computer Science, pages 191–200. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1978.

Francez:1979:SNC

[FHLdR79] Nissim Francez, C. A. R. Hoare, Daniel J. Lehmann, and Willem P. de Roever. Semantics of nondeterminism, concurrency, and communication. Journal of Computer and System Sciences, 19(3):290– 308, December 1979. CODEN JCSSBM. ISSN 0022-0000 (print),

1090-2724 (electronic). URL http://www.sciencedirect.com/
science/article/pii/0022000079900060.

Fournet:2004:SFC

[FHRR04] Cédric Fournet, Tony Hoare, Sriram K. Rajamani, and Jakob Rehof. Stuck-free conformance. In Computer aided verification, volume 3114 of Lecture Notes in Computer Science, pages 242–254. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2004.

Fouz:2012:SAQ

[FKMJ12] Mahmoud Fouz, Manfred Kufleitner, Bodo Manthey, and Nima Zeini Jahromi. On smoothed analysis of Quicksort and Hoare’s Find. Algorithmica, 62(3–4):879–905, April 2012. CODEN ALGOEJ. ISSN 0178-4617 (print), 1432-0541 (electronic). URL

http://www.springerlink.com/openurl.asp?genre=article&
issn=0178-4617&volume=62&issue=3&spage=879.

Flannery:1990:HSP

[FM90] Kevin E. Flannery and Johannes J. Martin. The Hoare and Smyth power domain constructors commute under composition. Journal of Computer and System Sciences, 40(2):125–135, April 1990. CODEN JCSSBM. ISSN 0022-0000 (print), 1090-2724

(electronic). URL http://www.sciencedirect.com/science/
article/pii/0022000090900089.

Fokkinga:1987:CPS

[Fok87] Maarten M. Fokkinga. A correctness proof of sorting by means of formal procedures. Science of Computer Programming, 9(3):263– 270 (or 263–269??), December 1987. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic).

Foster:2019:HRI

[Fos19] Simon Foster. Hybrid relations in isabelle/UTP. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 130–153. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.6 .U86 2019.

URL http://link.springer.com/.

Floyd:1975:AAA

[FR75] Robert W. Floyd and Ronald L. Rivest. ACM Algorithm 489: The algorithm SELECT — for finding the i-th smallest of n elements [M1]. Communications of the ACM, 18(3):173, March 1975. CO-DEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). See also [Bro76].

Frana:2002:ICA

[Fra02] Philip Frana. An interview with Charles Antony Richard Hoare. Technical Report OH 357, Charles Babbage Institute Center for the History of Information Processing University of Minnesota, Minneapolis, MN, USA, July 17, 2002. 43 pp. URL http://

pascal.hansotten.com/uploads/hoare/oh357th.pdf.

Feijen:1990:BOB

[FvGGM90] W. H. J. Feijen, A. J. M. van Gasteren, David Gries, and J. Misra, editors. Beauty is our Business: a Birthday Salute to Edsger W. Dijkstra. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1990. ISBN 0-387-97299-4, 3-540-97299-4, 1-4612-8792-8 (print), 1-4612-4476-5 (online). ISSN 0172-603X. xix + 453 pp. LCCN QA76 .B326 1990. URL http://www.

zentralblatt-math.org/zmath/en/search/?an=0718.68004.

Feng:2021:QHL

[FY21] Yuan Feng and Mingsheng Ying. Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing (TQC), 2(4):16:1–16:43, December 2021. CODEN ???? ISSN 2643-6809 (print), 2643-6817 (electronic). URL https://dl.acm.org/doi/

10.1145/3456877.

Gardiner:1995:APC

[Gar95] P. H. B. Gardiner. Algebraic proofs of consistency and completeness. Theoretical Computer Science, 150(1):161–191, October 16, 1995. CODEN TCSCDI. ISSN 0304-3975 (print),

1879-2294 (electronic). URL http://www.elsevier.com/cgi-
bin/cas/tree/store/tcs/cas_sub/browse/browse.cgi?year=
1995&volume=150&issue=1&aid=1845.

Gritzner:1996:RAM

[GB96] Thomas F. Gritzner and Rudolf Berghammer. A relation algebraic model of robust correctness. Theoretical Computer Science, 159 (2):245–270, June 03, 1996. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic). URL http://www.elsevier.com/

cgi-bin/cas/tree/store/tcs/cas_sub/browse/browse.cgi?
year=1996&volume=159&issue=2&aid=2001.

Gordon:1992:MRH

[GH92] M. J. C. Gordon and Charles A. R. Hoare. Mechanized reasoning and hardware design: a discussion; (meeting held at the Royal Society on 3 and 4 October 1991). Prentice-Hall international series in computer science. Prentice-Hall, Upper Saddle River, NJ 07458, USA, 1992. ISBN 0-13-572405-8. 151 pp. LCCN

TK7895.M5 M4 1992. URL http://www.gbv.de/dms/bowker/
toc/9780135724057.pdf.

Greif:1981:SSW

[GM81] Irene Greif and Albert R. Meyer. Specifying the semantics of while programs: a tutorial and critique of a paper by Hoare and Lauer. ACM Transactions on Programming Languages and Systems, 3 (4):484–507, October 1981. CODEN ATPSDT. ISSN 0164-0925 (print), 1558-4593 (electronic).

Gibbons:2012:MPC

[GN12] Jeremy Gibbons and Pablo Nogueira, editors. Mathematics of program construction: 11th International Conference, MPC 2012, Madrid, Spain, June 25–27, 2012, Proceedings, volume 7342 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2012.

CODEN LNCSD9. ISBN 3-642-31112-1 (print), 3-642-31113-X (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.9.M65 M63 2012. URL http://link.springer.

com/chapter/10.1007/978-3-642-31113-0_2/.

Groote:1994:PAG

[GP94] Jan Friso Groote and Alban Ponse. Process algebra with guards: Combining Hoare logic with process algebra. Formal Aspects of Computing, 6(2):115–164, March 1994. CODEN FACME5. ISSN 0934-5043 (print), 1433-299X (electronic). URL http://link.

springer.com/article/10.1007/BF01221097.

Grubel:1996:ADT

[GR96] Rudolf Grübel and Uwe Rösler. Asymptotic distribution theory for Hoare’s selection algorithm. Advances in Applied Probability, 28(1):252–269, March 1996. CODEN AAPBBD. ISSN 0001-8678 (print), 1475-6064 (electronic). URL http://www.jstor.

org/stable/1427920.

Gozum:1997:LWC

[GR97] Marvine E. Gozum and Sorel Reisman. Letters: Windows CE success. Computer, 30(5):10, May 1997. CODEN CPTRB4. ISSN 0018-9162 (print), 1558-0814 (electronic). Response to [Lew97].

Gray:2021:OR

[Gra21] Margaret Gray. Online resources. In Jones and Misra [JM21f], pages 411–412. ISBN 1-4503-8728-4. LCCN QA76.6.

Grubel:1998:HSA

[Grü98] Rudolf Grübel. Hoare’s selection algorithm: a Markov chain approach. Journal of Applied Probability, 35(1):36–45, March 1998. CODEN JPRBAM. ISSN 0021-9002 (print), 1475-6072 (elec-

tronic). URL http://www.jstor.org/stable/3215544.

Gardner:2008:LHR

[GSWZ08] Philippa A. Gardner, Gareth D. Smith, Mark J. Wheelhouse, and Uri D. Zarfaty. Local Hoare reasoning about DOM. In Lenzerini and Lembo [LL08], pages 261–270. ISBN 1-60560-932-3, 1-60558-108-9. LCCN QA76.9.D3.

Guttmann:2019:CFC

[Gut19] Walter Guttmann. Connecting fixpoints of computations with strict progress. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 62–79. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic).

LCCN QA76.6 .U86 2019. URL http://link.springer.com/.

Hoare:1972:I

[HA72] C. A. R. Hoare and D. C. S. Allison. Incomputability. ACM Computing Surveys, 4(3):169–178, September 1972. CODEN CMSVAN. ISSN 0010-4892.

Hoare:1998:SCE

[HB98] Tony Hoare and Jan A. Bergstra. The science of computing and the engineering of software. Nederlandse Organisatie voor Wetenschappelijke Onderzoek, The Hague, The Netherlands, 1998. ISBN ???? 50 pp. Huygens Lecture.

Hoare:2001:ETS

[HBS01] C. A. R. Hoare, Manferd Broy, and Ralf Steinbrüggen, editors. Engineering Theories of Software Construction. NATO Science Series III: Computer and Systems Sciences. Proceedings of the 2000 Marktoberdorf Summer School. 25 July–6 August 2000. IOS Press, Amsterdam, The Netherlands, 2001. ISBN 1-58603-172-4 (IOS Press), 4-274-90435-0 (Ohmsha). LCCN QA76.758 .E55 2001.

Hoare:1988:PCC

[HG88] C. A. R. Hoare and M. J. C. Gordon. Partial correctness of C-MOS switching circuits: an exercise in applied logic. In IEEE [IEE88], pages 28–36. ISBN 0-8186-0853-6 (paperback); 0-8186-4853-8 (microfiche). LCCN QA76.9.M35 S94 1988. Computer Society order number 853. IEEE catalog number 88CH2608-8.

Hortala-Gonzalez:1989:HLN

[HGRA89] M. T. Hortala-Gonzalez and M. Rodriguez-Artalejo. Hoare’s logic for nondeterministic regular programs: a nonstandard approach. Theoretical Computer Science, 68(3):277–302, November 12, 1989. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Hehner:1983:MCM

[HH83] E. C. R. Hehner and C. A. R. Hoare. A more complete model of communicating processes. Theoretical Computer Science, 26(1– 2):105–120, September 1983. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Hoare:1985:WP

[HH85] C. A. R. Hoare and Jifeng He. Weakest prespecification. Technical Monograph PRG-44, Oxford University Computing Laboratory, Programming Research Group, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, June 1985. iii + 60 pp. URL http:

//www.cs.ox.ac.uk/files/3320/PRG44.pdf.

Hoare:1986:ASP

[HH86a] C. A. R. Hoare and J. He. Algebraic specification and proof of properties of a mail service. In L. Meertens, editor, IFIP WG 2.1 Working Conference on Program Specification and Transformations, Bad-Tölz, W. Germany 15–17 April, pages ??–? North-Holland Publishing Co., Amsterdam, The Netherlands, 1986. URL

https://dl.acm.org/doi/10.5555/28195.28214.

Hoare:1986:WPa

[HH86b] C. A. R. Hoare and Jifeng He. The weakest prespecification. I. Fundamenta Informaticae, 9(1):51–84, March 1986. CODEN FU-MAAJ. ISSN 0169-2968 (print), 1875-8681 (electronic).

Hoare:1986:WPb

[HH86c] C. A. R. Hoare and Jifeng He. The weakest prespecification. II. Fundamenta Informaticae, 9(2):217–252, ???? 1986. CODEN FU-MAAJ. ISSN 0169-2968 (print), 1875-8681 (electronic).

He:1987:ASP

[HH87a] Jifeng He and C. A. R. Hoare. Algebraic specification and proof of a distributed recovery algorithm. Distributed Computing, 2(1):1– 12, March 1987. CODEN DICOEB. ISSN 0178-2770 (print), 1432-

0452 (electronic). URL https://link.springer.com/article/
10.1007/BF01786251.

Hoare:1987:DPM

[HH87b] C. A. R. Hoare and J. He. Design and proof of a mail service. In O. Friesen and F. Golshani, editors, 6th Annual International Phoenix Conference on Computers and Communications — Conference Proceedings Scottsdale, AZ, USA 25–27 February, 1987, pages 272–275. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 1987. URL https://

dl.acm.org/doi/10.5555/107155.107170.

Hoare:1987:WP

[HH87c] C. A. R. Hoare and Jifeng He. The weakest prespecification. Information Processing Letters, 24(2):127–132, January 30, 1987. CO-DEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

He:1990:CSP

[HH90a] Jifeng He and C. A. R. Hoare. Categorical semantics for programming languages. In Mathematical foundations of programming semantics (New Orleans, LA, 1989), volume 442 of Lecture Notes in Computer Science, pages 402–417. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1990.

He:1990:DRC

[HH90b] Jifeng He and C. A. R. Hoare. Data refinement in a categorical setting. Technical Monograph PRG-90, Oxford University Computing Laboratory, Programming Research Group, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, 1990. ISBN 0-902928-68-6. 15 pp.

Hoare:1990:CSP

[HH90c] C. A. R. Hoare and J. He. Categorical semantics for programming languages. In ????, editor, Mathematical Foundations of Programming Semantics, volume 442 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1990.

Hoare:1990:RAPa

[HH90d] C. A. R. Hoare and J. He. Refinement algebra proves correctness of compiling specifications. Technical Report TR-6-90, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, 1990.

Hoare:1990:RAPb

[HH90e] C. A. R. Hoare and J. He. Refinement algebra proves correctness of compiling specifications: Keynote address. In ????, editor, Lecture Notes of International Summer School at Markorbdorf, 1990, page ?? Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1990. Published in colloboration with the British Computer Society, London.

Hoare:1992:RAP

[HH92] C. A. R. Hoare and Jifeng He. Refinement algebra proves correctness of compilation. In Manfred Broy, editor, Programming and mathematical method (Marktoberdorf, 1990), volume 88 of NATO ASI Series F: Computer and Systems Sciences, pages 245–269. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1992.

He:1993:AOS

[HH93] Jifeng He and C. A. R. Hoare. From algebra to operational semantics. Information Processing Letters, 45(2):75–80, February 26, 1993. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

He:1997:LTP

[HH97a] Jifeng He and C. A. R. Hoare. Linking theories in probabilistic programming. In ????, editor, Proceeding of SBLP’97, page ?? ????, ????, 1997. See also [HH99a].

Hoare:1997:UTPb

[HH97b] C. A. R. Hoare and Jifeng He. Unifying theories for parallel programming. In C. Lengauer and M. Griebl, editors, Euro-Par’97 Parallel Processing, volume 1300 of Lecture Notes in Computer Science, pages 15–30. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1997. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic).

Hoare:1997:UTC

[HH97c] C. A. R. Hoare and Jifeng He. Unifying theories of concurrency: Key address. In C. Lengauer and M. Griebl, editors, Europar 97 Parallel Processing, volume 1300 of Lecture Notes in Computer Science, page ?? Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1997.

Hoare:1998:UTP

[HH98] C. A. R. Hoare and Jifeng He. Unifying Theories of Programming. Prentice Hall Series in Computer Science. Prentice Hall, London, UK, 1998. ISBN 0-13-458761-8 (paperback). xix + 298 pp. LCCN QA76.6.H5735 1998.

He:1999:LTP

[HH99a] Jifeng He and C. A. R. Hoare. Linking theories in probabilistic programming. Information Sciences, 119(3–4):205–218, October 1999. CODEN ISIJBC. ISSN 0020-0255 (print), 1872-

6291 (electronic). URL https://doi.org/10.1016/s0020-0255%
2899%2900015-8.

Hoare:1999:TMPb

[HH99b] C. A. R. Hoare and Jifeng He. A trace model for pointers and objects. In R. Guerraoui, editor, ECOOP’ 99 — Object-Oriented Programming, volume 1628 of Lecture Notes in Computer Science, pages 1–18. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1999. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic). URL http:

//link.springer-ny.com/link/service/series/0558/bibs/
1628/16280001.htm;   http://link.springer-ny.com/link/
service/series/0558/papers/1628/16280001.pdf.

He:2000:UTH

[HH00] Jifeng He and C. A. R. Hoare. Unifying theories of healthiness condition. In IEEE [IEE00], pages 70–81. ISBN 0-7695-0915-0, 0-7695-0916-9 (casebound), 0-7695-0917-7 (microfiche). ISSN 1530-1362. LCCN QA76.758 .A77 2000.

Hoare:2001:UTL

[HH01] C. A. R. Hoare and Jifeng He. Unifying theories for logic programming. In Hoare et al. [HBS01], page ?? ISBN 1-58603-172-4 (IOS Press), 4-274-90435-0 (Ohmsha). LCCN QA76.758 .E55 2001.

He:2005:LTC

[HH05] Jifeng He and C. A. R. Hoare. Linking theories of concurrency. In Dang Van Hung and Martin Wirsing, editors, Theoretical Aspects of Computing — ICTAC 2005 Second International Colloquium Hanoi Vietnam October 17–21 2005 Proceeding, volume 3722 of Lecture Notes in Computer Science, pages 303–317. Springer-Ver-lag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2005.

He:2010:CRC

[HH10] Jifeng He and Tony Hoare. CSP is a retract of CCS. Theoretical Computer Science, 411(11–13):1311–1337, March 6, 2010. CO-DEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Hoare:1990:AAV

[HHBP90] C. A. R. Hoare, J. He, J. P. Bowen, and P. K. Pandya. An algebraic approach to verifiable compiling specification and prototyping of the ProCoS level 0 programming language. In ????, editor, ESPRIT ’90 Conference Proceedings, pages 804–818. Kluwer Academic Publishers Group, Norwell, MA, USA, and Dordrecht, The Netherlands, 1990.

He:1994:PCS

[HHF^{+}94] Jifeng He, C. A. R. Hoare, Martin Fränzle, Markus Müller-Olm, Ernst-Rüdiger Olderog, Michael Schenke, Michael R. Hansen, Anders P. Ravn, and Hans Rischel. Provably correct systems. Lecture Notes in Computer Science, 863:288–335, 1994. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic).

Hoare:1987:CLP

[HHH^{+}87a] C. A. R. Hoare, I. J. Hayes, Jifeng He, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sorensen, J. M. Spivey, and B. A. Sufrin. Corrigenda: “Laws of programming” [Comm. ACM 30 (1987), no. 8, 672–686]. Communications of the ACM, 30(9):770, September 1987. CODEN CACMA2. ISSN 0001-0782 (print),

1557-7317 (electronic). URL http://www.acm.org/pubs/toc/
Abstracts/0001-0782/30407.html. See [HHH^{+}87b].

Hoare:1987:LP

[HHH^{+}87b] C. A. R. Hoare, I. J. Hayes, Jifeng He, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sørensen, J. M. Spivey, and B. A. Sufrin. Laws of programming. Communications of the ACM, 30(8):672–686, August 1987. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). URL http://www.acm.org/

pubs/toc/Abstracts/0001-0782/27653.html. See corrigendum

[HHH^{+}87a].

He:1990:TSA

[HHJ90] J. He, C. A. R. Hoare, and M. B. Josephs. A theory of synchrony and asynchrony. In ????, editor, Programming Concepts and Methods, pages 459–478. North-Holland Publishing Co., Amsterdam, The Netherlands, 1990.

Hoare:1992:LP

[HHJ^{+}92] C. A. R. Hoare, I. J. Hayes, He Jifeng, C. C. Morgan, A. W. Roscoe, J. W. Sanders, I. H. Sorenson, J. M. Spivey, and B. A. Sufrin. Laws of programming. In Manfred Broy, editor, Programming and Mathematical Method, pages 95–122. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1992.

Hoare:2011:LEL

[HHM^{+}11] C. A. R. Hoare, Akbar Hussain, Bernhard Möller, Peter W. O’Hearn, Rasmus Lerchedahl Petersen, and Georg Struth. On locality and the exchange law for concurrent processes. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011— Concurrency theory: 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011, Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 250–264. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2011.

He:1986:DRR

[HHS86] J. He, C. A. R. Hoare, and J. W. Sanders. Data refinement refined resume. In ESOP 86, pages 187–196. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1986.

Hoare:1987:PDR

[HHS87] C. A. R. Hoare, Jifeng He, and J. W. Sanders. Prespecification in data refinement. Information Processing Letters, 25(2):71–76, May 6, 1987. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Hoare:1993:NFA

[HHS93] C. A. R. Hoare, Jifeng He, and A. C. A. Sampaio. Normal form approach to compiler design. Acta Informatica, 30(8):701–739, November 1993. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic).

Hoare:1997:ADO

[HHS97] C. A. R. Hoare, Jifeng He, and A. Sampiao. Algebraic derivation of an operational semantics. In ????, editor, Milner’s Festschrift, page ?? MIT Press, Cambridge, MA, USA, 1997.

Hoare:1991:DPM

[HJ91] C. A. R. Hoare and He Jifeng. Design and proof of a mail service. In Hoare [Hoa91b], page ?? ISBN 0-201-17232-1. LCCN QA76.58 .D48 1991. Prepared with LaTEX.

Hoare:1999:TMPa

[HJ99] C. A. R. Hoare and He Jifeng. A trace model for pointers and objects. In Calculational system design (Marktoberdorf, 1998), volume 173 of NATO Sci. Ser. F Comput. Syst. Sci., pages 3–23. IOS, Amsterdam, 1999.

Huisman:2000:JPV

[HJ00] Marieke Huisman and Bart Jacobs. Java program verification via a Hoare logic with abrupt termination. Lecture Notes in Computer Science, 1783:284–??, 2000. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic). URL http://link.springer-ny.

com/link/service/series/0558/bibs/1783/17830284.htm;
http://link.springer-ny.com/link/service/series/0558/
papers/1783/17830284.pdf.

Herbert:2004:CST

[HJ04] Andrew Herbert and Karen Spärck Jones, editors. Computer Systems: Theory, Technology, and Applications; a tribute to Roger Needham. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2004. ISBN 0-387-20170-X. xvii + 338 pp. LCCN QA76.9.S88 H45 2004.

Hoare:2016:PST

[HJ16] C. A. R. Hoare and Cliff B. Jones. Professor Sir Tony Hoare: ACM Turing Award Winner 1980. Online video interview.,

November 24, 2016. URL https://amturing.acm.org/pdf/
HoareTuringTranscript.pdf.

Hofner:2014:RAM

[HJKM14] P. Höfner, Peter Jipsen, Wolfram Kahl, and Martin Eric Müller, editors. Relational and Algebraic Methods in Computer Science: 14th International Conference, RAMiCS 2014, Marienstatt, Germany, April 28–May 1, 2014, Proceedings, volume 8428 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2014. ISBN 3-319-06250-6 (paperback), 3-319-06251-4 (e-book). LCCN QA8.9-QA10.3; QA76.9.M35 R36 2014. URL https://doi.org/10.

1007/978-3-319-06251-8.

Hoare:2004:EHDb

[HJR04a] C. A. R. Hoare, C. B. Jones, and B. Randell. Extending the horizons of DSE. In Grand Challenges. UKCRC, page ?? ????, 2004.

URL http://www.nesc.ac.uk/esi/events/Grand_Challenges/
gcconf04/submissions/23.pdf.

Hoare:2004:EHDa

[HJR04b] Tony Hoare, Cliff Jones, and Brian Randell. Extending the horizons of DSE (GC6). Technical Report CS-TR-853, University of Newcastle upon Tyne, School of Computing Science, Claremont Tower, Claremont Road, Newcastle upon Tyne, NE1 7RU, UK.,

February 5, 2004. 6 pp. URL http://homepages.cs.ncl.ac.uk/
cliff.jones/publications/NU-TRs/CS-TR-853.pdf.

Hoare:2000:ADO

[HJS00] C. A. R. Hoare, He Jifeng, and Augusto Sampaio. Algebraic derivation of an operational semantics. In Gordon Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, language, and interaction: Essays in Honour of Robin Milner, Found. Comput. Ser., pages 77–98. MIT Press, Cambridge, MA, USA, 2000.

Hoare:1980:TND

[HK80] C. A. R. Hoare and J. R. Kennaway. A theory of non-determinism. In ????, editor, Proceedings ICALP ’80, volume 85 of Lecture Notes in Computer Science, pages 338–350. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1980.

Hayes:2021:SS

[HK21] Ian J. Hayes and Steve King. Software specification. In Jones and Misra [JM21f], pages 251–270. ISBN 1-4503-8728-4. LCCN QA76.6.

Hoare:1974:CCF

[HL74] C. A. R. Hoare and Peter E. Lauer. Consistent and complementary formal theories of the semantics of programming languages. Acta Informatica, 3(2):135–153, June 22, 1974. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic).

Hoare:1972:SSMa

[HM72a] C. A. R. Hoare and R. M. McKeag. A survey of store management techniques: Part 1. In Hoare and Perrott [HP72], pages 117–131. ISBN 0-12-350650-6. LCCN QA76.6 .I57 1971; TA168. URL http:

//brinch-hansen.net/papers/1971a.pdf.

Hoare:1972:SSMb

[HM72b] C. A. R. Hoare and R. M. McKeag. A survey of store management techniques: Part 2. In Hoare and Perrott [HP72], pages 132–151. ISBN 0-12-350650-6. LCCN QA76.6 .I57 1971; TA168. URL http:

//brinch-hansen.net/papers/1971a.pdf.

Hoare:1982:SOS

[HM82] C. A. R. Hoare and R. M. McKeag. Structure of an operating system. In M. Broy and G. Schmidt, editors, Theoretical Foundations of Programming Methodology – Lecture Notes of an International Summer School, Germany, 1981, pages 643–658. D. Reidel, Dordrecht, The Netherlands; Boston, MA, USA; Lancaster, UK; Tokyo, Japan, 1982.

Hoare:1985:SSN

[HM85] C. A. R. Hoare and C. C. Morgan. Specification of a simplified network service in CSP. In B. T. Denvir, W. T. Harwood, and M. I. Jackson, editors, he Analysis of Concurrent Systems, Cambridge, September 1983, Proceedings, volume 207 of Lecture Notes in Computer Science, pages 345–353. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1985. URL

https://dl.acm.org/doi/10.5555/647694.731194.

Homeier:1995:MVV

[HM95] Peter V. Homeier and David F. Martin. A mechanically verified verification condition generator. The Computer Journal, 38(2): 131–141, ???? 1995. CODEN CMPJA6. ISSN 0010-4620 (print),

1460-2067 (electronic). URL http://comjnl.oxfordjournals.
org/content/38/2/131.full.pdf+html;   http://www3.oup.
co.uk/computer_journal/Volume_38/Issue_02/Vol38_02.body.
html#AbstractHomeier.

Hoare:2005:GCC

[HM05] Tony Hoare and Robin Milner. Grand challenges for computing research. The Computer Journal, 48(1):49–52, January 2005. CO-DEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (electronic).

URL http://www3.oup.co.uk/computer_journal/hdb/Volume_
48/Issue_01/bxh065.sgm.abs.html;   http://www3.oup.co.
uk/computer_journal/hdb/Volume_48/Issue_01/pdf/bxh065.
pdf.

Hoare:2008:VST

[HM08] Tony Hoare and Jay Misra. Verified software: Theories, tools, experiments vision of a grand challenge project. In Meyer and Woodcock [MW08], pages 1–18. ISBN 3-540-69147-2 (paperback), 3-540-69149-9 (e-book). ISSN 0302-9743. LCCN

QA76.76.V47 V78 2008eb. URL http://link.springer.com/
openurl?genre=book\%26isbn=978-3-540-69147-1;   http:

//VH7QX3XE2P.search.serialssolutions.com/?V=1.0\%26L=
VH7QX3XE2P\%26S=JCs\%26C=TC0000320630\%26T=marc\%26tab=
BOOKS.

Hoare:2009:PSI

[HM09] C. A. R. Hoare and Jayadev Misra. Preface to special issue on software verification. ACM Computing Surveys, 41(4):18:1–18:3, October 2009. CODEN CMSVAN. ISSN 0360-0300 (print), 1557-7341 (electronic).

Hayes:2019:DAR

[HM19] Ian J. Hayes and Larissa A. Meinicke. Developing an algebra for rely/guarantee concurrency: Design decisions and challenges. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 176– 197. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.6

.U86 2019. URL http://link.springer.com/.

Hoare:2021:PSI

[HM21] C. A. R. Hoare and Jayadev Misra. Preface to special issue on software verification. In Jones and Misra [JM21f], pages 77–80. ISBN 1-4503-8728-4. LCCN QA76.6.

Hoare:2009:VSI

[HMLS09] C. A. R. Hoare, Jayadev Misra, Gary T. Leavens, and Natarajan Shankar. The verified software initiative: a manifesto. ACM Computing Surveys, 41(4):22:1–22:8, October 2009. CODEN CMSVAN. ISSN 0360-0300 (print), 1557-7341 (electronic).

Hoare:2021:VSI

[HMLS21] Tony Hoare, Jayadev Misra, Gary T. Leavens, and Natarajan Shankar. The Verified Software Initiative: a manifesto. In Jones and Misra [JM21f], pages 81–92. ISBN 1-4503-8728-4. LCCN QA76.6.

Hoare:2005:TSO

[HMM05] Tony Hoare, Galen Menzel, and Jayadev Misra. A tree semantics of an orchestration language. In Broy et al. [BGHH05], pages 331– 350. ISBN 1-4020-3530-6 (hardcover), 1-4020-3531-4 (paperback), 1-4020-3532-2 (e-book), 1-280-28396-3. LCCN QA76.758 .N385

Hoare:2009:CKA

[HMSW09a] C. A. R. Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene algebra. In Mario Bravetti and Gianluigi Zavattaro, editors, CONCUR 2009 — Concurrency Theory: 20th International Conference, CONCUR 2009, Bologna, Italy, September 1–4, 2009, Proceedings, volume 5710 of Lecture Notes in Computer Science, pages 399–414. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2009.

Hoare:2009:FCK

[HMSW09b] C. A. R. Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Foundations of concurrent Kleene algebra. In Berghammer et al. [BJM09], pages 166–186. ISBN 3-642-04638-X, 3-642-04639-8 (e-book). LCCN QA10 .I58 2009.

Hoare:2011:CKA

[HMSW11] Tony Hoare, Bernhard Möller, Georg Struth, and Ian Wehrman. Concurrent Kleene algebra and its foundations. Journal of Logic and Algebraic Programming, 80(6):266–296, 2011. ISSN 1567-8326 (print), 1873-5940 (electronic).

Hoare:2008:SLS

[HO08] Tony Hoare and Peter O’Hearn. Separation logic semantics for communicating processes. Electronic Notes in Theoretical Computer Science, 212:3–25, April 2008. ISSN 1571-0661.

Hoare:1961:AP

[Hoa61a] C. A. R. Hoare. Algorithm 63: Partition. Communications of the ACM, 4(7):321, July 1961. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Hoare:1961:AQ

[Hoa61b] C. A. R. Hoare. Algorithm 64: Quicksort. Communications of the ACM, 4(7):321, July 1961. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Hoare:1961:AF

[Hoa61c] C. A. R. Hoare. Algorithm 65: Find. Communications of the ACM, 4(7):321–322, July 1961. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Hoare:1961:MSS

[Hoa61d] C. A. R. Hoare. A method of synthesizing sentences in machine translation on the basis of syntagmatic analysis. Foreign Developments in Machine Translation and Information Processing, USSR, ??(95):??, 1961. Translated from Mashinnii Perevod i Prikladnaya Linguistika No. 6, pp. 80–88).

Hoare:1962:Q

[Hoa62a] C. A. R. Hoare. Quicksort. The Computer Journal, 5(1):10–15, April 1962. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-

2067 (electronic). URL http://comjnl.oxfordjournals.org/
content/5/1/10.full.pdf+html;   http://www3.oup.co.uk/
computer_journal/hdb/Volume_05/Issue_01/050010.sgm.abs.
html;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
05/Issue_01/tiff/10.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_05/Issue_01/tiff/11.tif;   http://
www3.oup.co.uk/computer_journal/hdb/Volume_05/Issue_01/
tiff/12.tif;   http://www3.oup.co.uk/computer_journal/
hdb/Volume_05/Issue_01/tiff/13.tif;   http://www3.oup.
co.uk/computer_journal/hdb/Volume_05/Issue_01/tiff/14.
tif;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
05/Issue_01/tiff/15.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_05/Issue_01/tiff/16.tif.

Hoare:1962:REA

[Hoa62b] C. A. R. Hoare. Report on the Elliott ALGOL translator. The Computer Journal, 5(2):127–129, July 1962. CO-DEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (elec-

tronic). URL http://comjnl.oxfordjournals.org/content/5/
2/127.full.pdf+html;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_05/Issue_02/050127.sgm.abs.html;
http://www3.oup.co.uk/computer_journal/hdb/Volume_05/
Issue_02/tiff/127.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_05/Issue_02/tiff/128.tif;   http:/
/www3.oup.co.uk/computer_journal/hdb/Volume_05/Issue_
02/tiff/129.tif.

Hoare:1963:BR

[Hoa63a] C. A. R. Hoare. Book reviews. The Computer Journal, 6(2): 143, August 1963. CODEN CMPJA6. ISSN 0010-4620 (print),

1460-2067 (electronic). URL http://comjnl.oxfordjournals.
org/content/6/2/143.full.pdf+html.

Hoare:1963:EAI

[Hoa63b] C. A. R. Hoare. The Elliott ALGOL input/output system. The Computer Journal, 5(4):345–348, January 1963. CO-DEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (elec-

tronic). URL http://comjnl.oxfordjournals.org/content/5/
4/345.full.pdf+html;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_05/Issue_04/050345.sgm.abs.html;
http://www3.oup.co.uk/computer_journal/hdb/Volume_05/
Issue_04/tiff/345.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_05/Issue_04/tiff/346.tif;   http:/
/www3.oup.co.uk/computer_journal/hdb/Volume_05/Issue_
04/tiff/347.tif;   http://www3.oup.co.uk/computer_journal/
hdb/Volume_05/Issue_04/tiff/348.tif.

Hoare:1964:BRA

[Hoa64a] C. A. R. Hoare. Book review: Algol on the KDF9. The Computer Journal, 7(2):154, ???? 1964. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (electronic). URL http://comjnl.

oxfordjournals.org/content/7/2/154.full.pdf+html.

Hoare:1964:CE

[Hoa64b] C. A. R. Hoare. Case expressions. ALGOL Bulletin (Amsterdam: Mathematisch Centrum), 21(??):20–22, ???? 1964. CODEN ALGOBG. ISSN 0084-6198.

Hoare:1964:EAP

[Hoa64c] C. A. R. Hoare. The Elliott ALGOL programming system. In P. Wegner, editor, Introduction to System Programming, pages 156–166. Academic Press, New York, USA, 1964. URL https://

archive.org/details/introductiontosy00wegn/page/2.

Hoare:1965:NIA

[Hoa65a] C. A. R. Hoare. A note on indirect addressing. ALGOL Bulletin (Amsterdam: Mathematisch Centrum), 21(??):63–65, November 1965. CODEN ALGOBG. ISSN 0084-6198. URL https://

archive.computerhistory.org/resources/text/algol/algol_
bulletin/A21/P38.HTM.

Hoare:1965:RH

[Hoa65b] C. A. R. Hoare. Record handling. ALGOL Bulletin (Amsterdam: Mathematisch Centrum), 21(??):39–69, ???? 1965. CODEN

ALGOBG. ISSN 0084-6198. URL https://dl.acm.org/doi/10.
5555/1061032.1061041.

Hoare:1966:LWM

[Hoa66a] C. A. R. Hoare. Letter to WG 2.1 members. Unknown, 1966.

Hoare:1966:P

[Hoa66b] C. A. R. Hoare. PL/I. In Proceedings of the ACTP Summer School on Software, June 1966, pages 1–25. ????, ????, 1966. URL http:

//www.cs.ox.ac.uk/files/6072/H66%20-%20PL1.pdf.

Hoare:1966:SPC

[Hoa66c] C. A. R. Hoare. Single pass compilation. In Proceedings of the ACTP Summer School on Software, June 1966, pages 1–12. ????,

????, 1966. URL https://www.cs.ox.ac.uk/files/6073/H66%
20-%20Single.pdf.

Hoare:1968:CA

[Hoa68a] C. A. R. Hoare. Critique of ALGOL 68. ALGOL Bulletin (Amsterdam: Mathematisch Centrum), 29(??):27–29, November 1968. CODEN ALGOBG. ISSN 0084-6198. URL https://archive.

computerhistory.org/resources/text/algol/algol_bulletin/
A29/P34.HTM.

Hoare:1968:DST

[Hoa68b] C. A. R. Hoare. Data structures in two-level store. In Proceedings of the IFIP Congress, Edinburgh, 1968, pages 322–329. North-Holland Publishing Co., Amsterdam, The Netherlands, 1968. URL

https://dblp.org/rec/conf/ifip/Hoare68.

Hoare:1968:LVW

[Hoa68c] C. A. R. Hoare. Letter to A. van Wijngaarden. Unknown, ????

1968.

Hoare:1968:LL

[Hoa68d] C. A. R. Hoare. Limitations on languages. Computer Weekly, ?? (??):??, ???? 1968. CODEN ???? ISSN 0010-4787.

Hoare:1968:RDR

[Hoa68e] C. A. R. Hoare. Recommendation on draft report on ALGOL 68. Unknown, ???? 1968.

Hoare:1968:RH

[Hoa68f] C. A. R. Hoare. Record handling. In F. Genuys, editor, Programming Languages, pages 291–347. Academic Press, New York, USA,

Hoare:1968:SM

[Hoa68g] C. A. R. Hoare. Set manipulation. ALGOL Bulletin (Amsterdam: Mathematisch Centrum), 27(??):29–37, ???? 1968. URL https:/

/dl.acm.org/doi/10.5555/1061098.1061105.

Hoare:1969:ABC

[Hoa69] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–580, 583, October 1969. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Hoare:1970:BR

[Hoa70a] C. A. R. Hoare. Book review. The Computer Journal, 13(2): 170, ???? 1970. CODEN CMPJA6. ISSN 0010-4620 (print),

1460-2067 (electronic). URL http://comjnl.oxfordjournals.
org/content/13/2/170.full.pdf+html.

Hoare:1970:BRC

[Hoa70b] C. A. R. Hoare. Book review: Computer languages: a practical guide to the chief programming languages: Peter C. Sanderson, M. A. Newnes-Butterworths £2.15s. Computer Physics Communications, 1(6):477, December 1970. CODEN CPHCBZ. ISSN 0010-4655 (print), 1879-2944 (electronic). URL http://www.

sciencedirect.com/science/article/pii/0010465570900275.

Hoare:1971:CSI

[Hoa71a] C. A. R. Hoare. Computer science: an inaugural lecture delivered before the Queen’s University of Belfast on 10 February 1971, volume 62 of New Lecture. The Queen’s University, Belfast, Northern Ireland, 1971. ISBN 0-85389-051-X. 17 pp. LCCN AS122.B4 A3 no. 62 QA76. Inaugural lecture, 10.2.1971.

Hoare:1971:PPA

[Hoa71b] C. A. R. Hoare. Procedures and parameters: an axiomatic approach. In E. Engeler, editor, Symposium on Semantics of Algorithmic Languages, volume 188 of Lecture Notes in Mathematics, pages 102–116. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1971. CODEN LNMAA2. ISBN 3-540-05377-8 (print), 3-540-36499-4 (e-book). ISSN 0075a-8434 (print), 1617-9692 (electronic). URL http://link.springer.

com/chapter/10.1007/BFb0059696/.

Hoare:1971:PP

[Hoa71c] C. A. R. Hoare. Proof of a program. Communications of the ACM, 14(1):39–45, January 1971. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Hoare:1971:PPF

[Hoa71d] C. A. R. Hoare. Proof of a program: FIND. Communications of the ACM, 14(1):39–45, January 1971. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). URL http://doi.acm.

org/.

Hoare:1972:GEQ

[Hoa72a] C. A. R. Hoare. Guest editorial: The quality of software. Software —Practice and Experience, 2(2):103–105, April 1972. CODEN SPEXBL. ISSN 0038-0644 (print), 1097-024X (electronic).

Hoare:1972:NS

[Hoa72b] C. A. R. Hoare. A note on the For statement. BIT, 12 (3):334–341, September 1972. CODEN BITTEL, NBITAB. ISSN 0006-3835 (print), 1572-9125 (electronic). URL http:

//www.springerlink.com/openurl.asp?genre=article&issn=
0006-3835&volume=12&issue=3&spage=334.

Hoare:1972:NDS

[Hoa72c] C. A. R. Hoare. Notes on data structuring. In Dahl et al. [DDH72], chapter II, pages 83–174. ISBN 0-12-200550-3 (hardcover), 0-12-200556-2 (paperback). LCCN QA76.6 .D33 1972. URL https://

dl.acm.org/doi/10.5555/1243380.1243382. Second printing.

Hoare:1972:OSTb

[Hoa72d] C. A. R. Hoare. Operating systems: their purpose, objectives, functions and scope. In Hoare and Perrott [HP72], pages 11–28. ISBN 0-12-350650-6. LCCN QA76.6 .I57 1971; TA168. URL http:

//brinch-hansen.net/papers/1971a.pdf.

Hoare:1972:PSP

[Hoa72e] C. A. R. Hoare. Proof of a structured program: “The sieve of Eratosthenes”. The Computer Journal, 15(4):321–325, November 1972. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-

2067 (electronic). URL http://comjnl.oxfordjournals.org/
content/15/4/321.full.pdf+html;   http://www3.oup.co.
uk/computer_journal/hdb/Volume_15/Issue_04/150321.sgm.

abs.html;   http://www3.oup.co.uk/computer_journal/hdb/
Volume_15/Issue_04/tiff/321.tif;   http://www3.oup.co.
uk/computer_journal/hdb/Volume_15/Issue_04/tiff/322.tif;
 http://www3.oup.co.uk/computer_journal/hdb/Volume_15/
Issue_04/tiff/323.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_15/Issue_04/tiff/324.tif;   http:/
/www3.oup.co.uk/computer_journal/hdb/Volume_15/Issue_
04/tiff/325.tif.

Hoare:1972:PCD

[Hoa72f] C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4):271–281, November 1972. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic).

Hoare:1972:PBP

[Hoa72g] C. A. R. Hoare. Prospects for a better programming language. In Christma Boon, editor, High level languages: international computer state of the art report, volume 7, pages 327–343. Infotech Information Ltd.,, Maidenhead, Berkshire, UK, 1972. ISBN 0-85539-060-3. LCCN QA76.7 .H52.

Hoare:1972:TTP

[Hoa72h] C. A. R. Hoare. Towards a theory of parallel programming. In Hoare and Perrott [HP72], pages 61–71. ISBN 0-12-350650-6. LCCN QA76.6 .I57 1971; TA168. URL http://brinch-hansen.

net/papers/1971a.pdf.

Hoare:1973:CPE

[Hoa73a] C. A. R. Hoare. Computer programming as an engineering discipline. Electronics and Power, 19(14):316–320, August 1973. CO-DEN ELPWAQ. ISSN 0013-5127 (print), 2053-7883 (electronic).

Hoare:1973:GCL

[Hoa73b] C. A. R. Hoare. A general conservation law for queueing disciplines. Information Processing Letters, 2(3):82–85, August ??, 1973. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Hoare:1973:HLP

[Hoa73c] C. A. R. Hoare. High level programming languages, the way behind. In D. Simpson, editor, High Level Programming Languages — The Way Ahead, page ?? NCC Publications, Manchester, UK,

Hoare:1973:HPLa

[Hoa73d] C. A. R. Hoare. Hints on programming language design. Technical report, Stanford University, Stanford, CA, USA, 1973. URL

https://dl.acm.org/doi/book/10.5555/892013.

Hoare:1973:HPLb

[Hoa73e] C. A. R. Hoare. Hints on programming language design. DTIC Document ??, ????, ????, ???? 1973.

Hoare:1973:HPLc

[Hoa73f] C. A. R. Hoare. Hints on programming language design. Invited Address at SIGACT/SIGPLAN Symposium on Principles of Programming Languages, Boston, 1973.

Hoare:1973:SPS

[Hoa73g] C. A. R. Hoare. A structured paging system. The Computer Journal, 16(3):209–215, August 1973. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (electronic). URL http:

//comjnl.oxfordjournals.org/content/16/3/209.full.pdf+
html;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
16/Issue_03/160209.sgm.abs.html;   http://www3.oup.co.
uk/computer_journal/hdb/Volume_16/Issue_03/tiff/209.tif;
 http://www3.oup.co.uk/computer_journal/hdb/Volume_16/
Issue_03/tiff/210.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_16/Issue_03/tiff/211.tif;   http:/
/www3.oup.co.uk/computer_journal/hdb/Volume_16/Issue_
03/tiff/212.tif;   http://www3.oup.co.uk/computer_journal/
hdb/Volume_16/Issue_03/tiff/213.tif;   http://www3.oup.
co.uk/computer_journal/hdb/Volume_16/Issue_03/tiff/214.
tif;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
16/Issue_03/tiff/215.tif.

Hoare:1973:TMR

[Hoa73h] C. A. R. Hoare. Tomorrow’s men: The role of the university. Computer Weekly, 7:??, July 1973. CODEN ???? ISSN 0010-4787. Educational Supplement.

Hoare:1974:ADP

[Hoa74a] C. A. R. Hoare. An axiomatic definition of the programming language PASCAL. In Ershov and Nepomniaschy [EN74], pages 1–16. ISBN 0-387-06720-5 (New York paperback), 3-540-06720-5 (Berlin paperback). LCCN QA76 .I5798 1972.

Hoare:1974:HPL

[Hoa74b] C. A. R. Hoare. Hints on programming language design. In C. J. Bunyan, editor, State of the Art Report 20: Computer Systems Reliability, pages 505–534. Pergamon/Infotech, ????, 1974.

Hoare:1974:MOS

[Hoa74c] C. A. R. Hoare. Monitors: an operating system structuring concept. Communications of the ACM, 17(10):549–557, October 1974. CODEN CACMA2. ISSN 0001-0782 (print), 1557-

7317 (electronic). URL https://www.classes.cs.uchicago.
edu/archive/2020/winter/33100-1/papers/hoare-monitors.

pdf. Erratum in Communications of the ACM, Vol. 18, No. 2 (February), p. 95, 1975. This paper contains one of the first solutions to the Dining Philosophers problem.

Hoare:1974:OSS

[Hoa74d] C. A. R. Hoare. Optimization of store size for garbage collection. Information Processing Letters, 2(6):165–166, April ??, 1974. CO-DEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Hoare:1974:SDP

[Hoa74e] C. A. R. Hoare. Software design: a parable. Software World, 5 (9–10):53–56, ???? 1974. CODEN SOFWBG. ISSN 0038-0652.

URL https://people.dsv.su.se/~jpalme/s1/hoare.pdf.

Hoare:1975:DR

[Hoa75a] C. A. R. Hoare. Data reliability. ACM SIGPLAN Notices, 10(6): 528–533, June 1975. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Hoare:1975:HDP

[Hoa75b] C. A. R. Hoare. Hints on the design of a programming language for real-time command and control. In ????, editor, Implementation Languages for Real-Time Systems: II. Language Design–General Comments, volume ERO-2-75. ????, ????, 1975. ISBN ????

Hoare:1975:PPA

[Hoa75c] C. A. R. Hoare. Parallel programming: an axiomatic approach. Computer Languages, 1(2):151–160, June 1975. CODEN CO-LADA. ISSN 0096-0551 (print), 1873-6742 (electronic).

Hoare:1975:PCP

[Hoa75d] C. A. R. Hoare. Program correctness proofs. In B. Shaw, editor, Formal Aspects of Computing Science, Newcastle upon Tyne, 3–6 September, 1974, pages 7–45. University of Newcastle-upon-Tyne, Newcastle-upon-Tyne, UK, 1975.

Hoare:1975:RDS

[Hoa75e] C. A. R. Hoare. Recursive data structures. International Journal of Computer and Information Sciences, 4(2):105–132, June 1975. CODEN IJCIAH. ISSN 0091-7036.

Hoare:1975:SE

[Hoa75f] C. A. R. Hoare. Software engineering. The Computer Bulletin, 2(6):6–7, December 1975. CODEN COBUAH. ISSN 0010-4531 (print), 1464-357X (electronic).

Hoare:1976:CST

[Hoa76a] C. A. R. Hoare. Computer science and technology and their application. The Computer Journal, 19(2):172, May 1976. CO-DEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (electronic).

URL http://comjnl.oxfordjournals.org/content/19/2/172.
full.pdf+html.

Hoare:1976:F

[Hoa76b] C. A. R. Hoare. Foreword. In A discipline of programming [Dij76], page xi. ISBN 0-13-215871-X. LCCN QA76.6 .D54. With a foreword by C. A. R. Hoare.

Hoare:1976:HCP

[Hoa76c] C. A. R. Hoare. The high cost of programming languages. In Anonymous [Ano76], pages 413–429. ISBN 0-903796-15-5. LCCN QA76.6 .E97 1976; TK5104 S98 1976.

Hoare:1976:HDP

[Hoa76d] C. A. R. Hoare. Hints on the design of a programming language for real-time command and control. In J. P. Spencer, editor, Real-time Software: International State of the Art Report, pages 685–699. Infotech International, ????, 1976.

Hoare:1976:PPA

[Hoa76e] C. A. R. Hoare. Parallel programming: An axiomatic approach. In Bauer and Samelson [BS76], pages 11–42. ISBN 0-387-07994-7 (New York), 3-540-07994-7 (Berlin), 3-540-37972-X (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic).

LCCN QA76.6 .L335. URL http://link.springer-ny.com/
link/service/series/0558/tocs/t0046.htm;   http://www.
springerlink.com/content/978-0-387-07994-3;   http://
www.springerlink.com/openurl.asp?genre=book&isbn=978-
3-540-07994-1;   http://www.springerlink.com/openurl.
asp?genre=issue&issn=0302-9743&volume=46.

Hoare:1976:PCD

[Hoa76f] C. A. R. Hoare. Proof of correctness of data representations. In Bauer and Samelson [BS76], pages 183–193. ISBN 0-387-07994-7 (New York), 3-540-07994-7 (Berlin), 3-540-37972-X (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic).

LCCN QA76.6 .L335. URL http://link.springer-ny.com/
link/service/series/0558/tocs/t0046.htm;   http://www.
springerlink.com/content/978-0-387-07994-3;   http://
www.springerlink.com/openurl.asp?genre=book&isbn=978-
3-540-07994-1;   http://www.springerlink.com/openurl.
asp?genre=issue&issn=0302-9743&volume=46.

Hoare:1976:SOS

[Hoa76g] C. A. R. Hoare. The structure of an operating system. In Bauer and Samelson [BS76], pages 242–265. ISBN 0-387-07994-7 (New York), 3-540-07994-7 (Berlin), 3-540-37972-X (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic).

LCCN QA76.6 .L335. URL http://link.springer-ny.com/
link/service/series/0558/tocs/t0046.htm;   http://www.
springerlink.com/content/978-0-387-07994-3;   http://
www.springerlink.com/openurl.asp?genre=book&isbn=978-
3-540-07994-1;   http://www.springerlink.com/openurl.
asp?genre=issue&issn=0302-9743&volume=46.

Hoare:1976:SPI

[Hoa76h] C. A. R. Hoare. Structured programming in introductory programming courses. In Bates [Bat76], pages 255–263. ISBN 0-85539-270-3. LCCN QA76.6 .S85.

Hoare:1977:BR

[Hoa77a] C. A. R. Hoare. Book review. The Computer Journal, 20(2): 180, ???? 1977. CODEN CMPJA6. ISSN 0010-4620 (print),

1460-2067 (electronic). URL http://comjnl.oxfordjournals.
org/content/20/2/180.2.full.pdf+html.

Hoare:1977:I

[Hoa77b] C. A. R. Hoare. Introduction. In R. H. Perrott, editor, Software Engineering — Proceedings of a Symposium held at the Queen’s University of Belfast 1976, volume 14 of A P I C Studies in Data Processing, pages 7–14. Academic Press, New York, USA, 1977.

Hoare:1978:CSPa

[Hoa78a] C. A. R. Hoare. Communicating sequential processes. In B. Shaw, editor, Digital Systems Design. Proceedings of the Joint IBM University of Newcastle upon Tyne Seminar, 6–9 September 1977, pages 145–56. Newcastle University, Newcastle upon Tyne, UK, 1978.

Hoare:1978:CSPb

[Hoa78b] C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, August 1978. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). See corrigendum [Hoa78c].

Hoare:1978:CCS

[Hoa78c] C. A. R. Hoare. Corrigendum: “Communicating Sequential Processes”. Communications of the ACM, 21(11):958, November 1978. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). See [Hoa78b].

Hoare:1978:ESS

[Hoa78d] C. A. R. Hoare. The engineering of software: a startling contradiction. In Programming Methodology, pages 37–41. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1978.

Hoare:1978:SEK

[Hoa78e] C. A. R. Hoare. Software engineering: a keynote address. In ????, editor, 3rd International Conference on Software Engineering, Atlanta, GA., USA, 10–12 May, pages 1–4. ACM Press, New York,

NY 10036, USA, 1978. URL https://dl.acm.org/doi/10.5555/
800099.803183.

Hoare:1978:SPP

[Hoa78f] C. A. R. Hoare. Some properties of predicate transformers. Journal of the ACM, 25(3):461–480, July 1978. CODEN JACOAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Hoare:1979:CGW

[Hoa79] A. H. M. Hoare. Coinitial graphs and Whitehead automorphisms. Canadian Journal of Mathematics = Journal canadien de mathématiques, 31(??):112–123, ???? 1979. CODEN CJMAAB. ISSN 0008-414X (print), 1496-4279 (electronic).

Hoare:1980:HP

[Hoa80a] C. A. R. Hoare. Hoare on programming. Computer World UK, ?? (??):??–???, ???? 1980. Text of an interview.

Hoare:1980:MCSa

[Hoa80b] C. A. R. Hoare. A model for communicating sequential processes. Working paper 80-1, Wollongong University, Wollongong, NSW, Australia, 1980. 27 + 14 handwritten pp. URL https://ro.uow.

edu.au/compsciwp/14.

Hoare:1980:MCSb

[Hoa80c] C. A. R. Hoare. A model for communicating sequential processes. In R. M. McKeag and A. M. MacNaghten, editors, On the Construction of Programs, pages 229–254. Cambridge University Press, Cambridge, UK, 1980.

Hoare:1980:SPP

[Hoa80d] C. A. R. Hoare. Synchronisation of parallel processes. In F. K. Hanna, editor, Advanced Techniques for Microprocessor Systems, pages 108–111. Peter Peregrinus, ????, 1980.

Hoare:1981:CTCa

[Hoa81a] C. A. R. Hoare. A calculus of total correctness for communicating processes. Technical monograph PRG-23, Oxford University. Computing Laboratory. Programming Research Group, Oxford, UK, 1981. ?? pp.

Hoare:1981:CTCb

[Hoa81b] C. A. R. Hoare. A calculus of total correctness for communicating processes. Science of Computer Programming, 1(1–2):49–72, October 1981. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic).

Hoare:1981:TMB

[Hoa81c] C. A. R. Hoare. Is there a mathematical basis for computer programming? NAG Newsletter, 2:6–15, 1981. CODEN ???? ISSN 0269-0780.

Hoare:1981:MCS

[Hoa81d] C. A. R. Hoare. A model for communicating sequential processes. Technical Report PRG-22, Programming Research Group, Oxford University, Oxford, UK, June 1981. iv + 28 pp. URL http://www.

cs.ox.ac.uk/publications/publication3766-abstract.html.

Hoare:1981:P

[Hoa81e] C. A. R. Hoare. Professionalism. The Computer Bulletin, 2(29): 2–4, ???? 1981. CODEN COBUAH. ISSN 0010-4531 (print), 1464-357X (electronic). Invited Talk given at BCS 81.

Hoare:1981:EOC

[Hoa81f] Charles Antony Richard Hoare. The Emperor’s old clothes. Communications of the ACM, 24(2):75–83, 1981. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). URL https://

www.cs.fsu.edu/~engelen/courses/COP4610/hoare.pdf. This

is the 1980 ACM Turing Award Lecture, delivered at ACM’80, Nashville, Tennessee, October 27, 1980.

Hoare:1982:SPI

[Hoa82a] C. A. R. Hoare. Specifications, programs and implementations. Technical Monograph PRG-29, Oxford University Computing Laboratory, Programming Research Group, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, June 1982. iv + 29 pp. URL

http://www.cs.ox.ac.uk/files/3295/PRG29.pdf.

Hoare:1982:VTO

[Hoa82b] C. A. R. Hoare. Variations on a theme: an open letter to C. A. R. Hoare. In Selected Writings on Computing: a Personal Perspective [Dij82c], pages 132–140. ISBN 0-387-90652-5 (New York), 3-540-90652-5 (Berlin). LCCN QA76.24 .D54

1982. URL http://link.springer.com/chapter/10.1007/978-

1-4612-5695-3_23. Including a paper co-authored by C. S. Schölten.

Hoare:1983:TF

[Hoa83a] C. A. R. Hoare. 1983 technology forecast. Electronic Design, ??(??):??, January 1983. CODEN ELODAW. ISSN 0013-4872 (print), 1944-9550 (electronic).

Hoare:1983:ABC

[Hoa83b] C. A. R. Hoare. An axiomatic basis for computer programming (reprint). Communications of the ACM, 26(1):53–56, January 1983. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). Reprint of [Hoa69].

Hoare:1983:CSP

[Hoa83c] C. A. R. Hoare. Communicating Sequential Processes (reprint). Communications of the ACM, 26(1):100–106, 1983. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). Reprint of [Hoa78b].

Hoare:1983:NCS

[Hoa83d] C. A. R. Hoare. Notes on communicating sequential processes. Technical Monograph PRG-33, Oxford University Computing Laboratory, Programming Research Group, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, August 1983. ii + 23 pp.

URL http://www.cs.ox.ac.uk/files/3301/PRG33.pdf.

Hoare:1983:PEP

[Hoa83e] C. A. R. Hoare. Programming is an engineering profession. In P. J. L. Wallis, editor, State of the Art Report 11, No 3: Software Engineering, pages 77–84. Pergamon/Infotech, ????, 1983.

URL http://www.cs.ox.ac.uk/files/3293/PRG27.pdf. Oxford

Technical Monograph PRG-27.

Hoare:1984:PSS

[Hoa84a] C. A. R. Hoare. Programming: Sorcery or science? IEEE Software, 1(2):5–12, 15–16, April 1984. CODEN IESOEG. ISSN 0740-7459 (print), 1937-4194 (electronic).

Hoare:1984:PP

[Hoa84b] C. A. R. Hoare. Programs are predicates. Philosophical Transactions of the Royal Society A: Mathematical, Physical, and Engineering Sciences, 312(1522):475–489, 1984. CODEN PTRMAD, PTMSFB. ISSN 0080-4614. With discussion, Mathematical logic and programming languages.

Hoare:1985:CSP

[Hoa85a] C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall International Series in Computer Science. Prentice-Hall International, Englewood Cliffs, NJ, USA and London, UK, 1985. ISBN 0-13-153271-5 (hardcover), 0-13-153289-8 (paperback). viii + 256 pp. LCCN QA76.6 .H57 1985. URL https://dl.acm.org/ doi/book/10.5555/3921. With a foreword by Edsger W. Dijkstra.

Hoare:1985:CNP

[Hoa85b] C. A. R. Hoare. A couple of novelties in the propositional calculus. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 31(2):173–178, ???? 1985. CODEN ZMLGAQ. ISSN 0044-3050.

Hoare:1985:MP

[Hoa85c] C. A. R. Hoare. The mathematics of programming. In Foundations of software technology and theoretical computer science (New Delhi, 1985), volume 206 of Lecture Notes in Computer Science, pages 1–18. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1985. URL https://dl.acm.org/

doi/10.5555/646823.706892.

Hoare:1985:NCS

[Hoa85d] C. A. R. Hoare. Notes on communicating sequential systems. In Manfred Broy, editor, Control Flow and Data Flow: Concepts of Distributed Programming. Proceedings of NATO Advanced Study Institute International Summer School, Marktoberdorf, 31 July–12 August, 1984, volume 14 of NATO Adv. Sci. Inst. Ser. F: Comput. Systems Sci., pages 123–204. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1985.

Hoare:1985:PP

[Hoa85e] C. A. R. Hoare. Programs are predicates. In Hoare and Shepherdson [HS85], pages 141–155. ISBN 0-13-561465-1. LCCN

QA76.6 .M3646 1985. URL https://dl.acm.org/doi/abs/10.

5555/3721.3729. A Discussion Meeting of the Royal Society of London.

Hoare:1986:MP

[Hoa86a] C. A. R. Hoare. Mathematics of programming. Byte Magazine, 10(8):115–149, August 1986. CODEN BYTEDJ. ISSN 0360-5280 (print), 1082-7838 (electronic).

Hoare:1986:MPI

[Hoa86b] C. A. R. Hoare. The mathematics of programming: an inaugural lecture delivered before the University of Oxford on 17th October 1985. Oxford University Press, Walton Street, Oxford OX2 6DP, UK, 1986. ISBN 0-19-951550-6 (paperback). 25 pp. LCCN QA76.6 .H573 1986.

Hoare:1986:MAS

[Hoa86c] C. A. R. Hoare. Maths add safety to computer programs. New Scientist, ??(1526):53–59, ???? 1986. CODEN NWSCAL. ISSN 0262-4079 (print), 1364-8500 (electronic).

Hoare:1986:NCS

[Hoa86d] C. A. R. Hoare. Notes on communicating sequential systems. In Manfred Broy, editor, Control Flow and Data Flow: Concepts of Distributed Programming: Concepts of Distributed Programming. Proceedings of NATO Advanced Study Institute International Summer School, Marktoberdorf, 31 July–12 August 1984, volume 14 of Springer Study Edition, pages 123–204. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1986.

Hoare:1986:P

[Hoa86e] C. A. R. Hoare. Preface. Distributed Computing, 1(1):1, March 1986. CODEN DICOEB. ISSN 0178-2770 (print), 1432-0452 (elec-

tronic). URL https://link.springer.com/article/10.1007/
BF01843564.

Hoare:1987:ASP

[Hoa87a] C. A. R. Hoare. Algebraic specifications and proofs for communicating sequential processes. In Manfred Broy, editor, Logic of programming and calculi of discrete design (Marktoberdorf, 1986), volume 36 of NATO Adv. Sci. Inst. Ser. F: Comput. Systems Sci., pages 277–301. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1987.

Hoare:1987:OSF

[Hoa87b] C. A. R. Hoare. An overview of some formal methods for program design. Computer, 20(9):85–91, September 1987. CODEN CPTRB4. ISSN 0018-9162 (print), 1558-0814 (electronic).

Hoare:1987:EOC

[Hoa87c] Charles Antony Richard Hoare. The emperor’s old clothes. In Ashenhurst [Ash87], pages 143–161. ISBN 0-201-07794-9. LCCN QA76.24 .A33 1987. ACM Turing Award lecture.

Hoare:1989:ECS

[Hoa89a] C. A. R. Hoare. Essays in Computing Science. Prentice Hall International Series in Computer Science. Prentice Hall International, Englewood Cliffs, NJ, USA, 1989. ISBN 0-13-284027-8. xii + 412

pp. LCCN QA76 .H56 1989. URL https://dl.acm.org/doi/10.

5555/63445. With a foreword by David Gries, Edited and with a preface by C. B. Jones.

Hoare:1989:FMC

[Hoa89b] C. A. R. Hoare. Formal methods in computer system design. Computer Physics Communications, 57(1–3):206–210, December 2, 1989. CODEN CPHCBZ. ISSN 0010-4655 (print), 1879-2944

(electronic). URL http://www.sciencedirect.com/science/
article/pii/0010465589902130.

Hoare:1989:NAC

[Hoa89c] C. A. R. Hoare. Notes on an approach to category theory for computer scientists. In Manfred Broy, editor, Constructive methods in computing science (Marktoberdorf, 1988), volume 55 of NATO Adv. Sci. Inst. Ser. F: Comput. Systems Sci., pages 245– 305. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1989.

Hoare:1989:VPL

[Hoa89d] C. A. R. Hoare. The varieties of programming language. In Josep Díaz and Fernando Orejas, editors, TAPSOFT ’89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, Barcelona, Spain, March 13-17, 1989 Volume 1: Advanced Seminar on Foundations of Innovative Software Development I and Colloquium on Trees in Algebra and Programming (CAAP ’89), volume 351 of Lecture Notes in Computer Science, pages 1–18. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1989. URL https://link.springer.

com/content/pdf/10.1007/3-540-50939-9_121.pdf.

Hoare:1990:DRC

[Hoa90a] C. A. R. Hoare. Data refinement in a categorical setting. Technical Monograph PRG-90, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, 1990.

Hoare:1990:FPI

[Hoa90b] C. A. R. Hoare. Fixed points of increasing functions. Information Processing Letters, 34(3):111–112, April 9, 1990. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Hoare:1990:LMM

[Hoa90c] C. A. R. Hoare. Let’s make models: Keynote address. In Baeten and Klop [BK90], page 32. ISBN 0-387-53048-7, 3-540-53048-7, 3-540-46395-X (e-book). ISSN 0302-9743. LCCN QA267 .C5927 1990.

Hoare:1990:TDC

[Hoa90d] C. A. R. Hoare. A theory for the derivation of C-MOS circuit designs. In Feijen et al. [FvGGM90], chapter 22, pages 193– 205. ISBN 0-387-97299-4, 3-540-97299-4, 1-4612-8792-8 (print), 1-4612-4476-5 (online). ISSN 0172-603X. LCCN QA76 .B326 1990.

URL http://www.zentralblatt-math.org/zmath/en/search/?

an=0718.68004. Reprinted in [Hoa91c].

Hoare:1990:TCC

[Hoa90e] C. A. R. Hoare. A theory of conjunction and concurrency. In Rishe et al. [RNT90], pages 304–309. ISBN 0-8186-2035-8 (hardcover), 0-8186-6035-X (microfiche). LCCN QA76.9.D3 P3473 199.

Hoare:1991:ASP

[Hoa91a] C. A. R. Hoare. Algebraic specifications and proofs for communicating sequential processes. In Developments in Concurrency and Communication [Hoa91b], page ?? ISBN 0-201-17232-1. LCCN QA76.58 .D48 1991. Prepared with LaTEX.

Hoare:1991:DCC

[Hoa91b] C. A. R. Hoare, editor. Developments in Concurrency and Communication. Addison-Wesley, Reading, MA, USA, 1991. ISBN 0-201-17232-1. xiv + 336 pp. LCCN QA76.58 .D48 1991. Prepared with LaTEX.

Hoare:1991:TDCa

[Hoa91c] C. A. R. Hoare. A theory for the derivation of combinational C-MOS circuit designs. In D. Bjørner and V. Kotov, editors, Images of Programming: Dedicated to the Memory of A. P. Ershov: Papers Collected Under the Auspices of IFIP TC2, page ?? North-Holland Publishing Co., Amsterdam, The Netherlands, 1991.

Hoare:1991:TDCb

[Hoa91d] C. A. R. Hoare. A theory for the derivation of combinational C-MOS circuit designs. Theoretical Computer Science, 90(1):235– 251, November 11, 1991. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic). Reprint of [Hoa90d].

Hoare:1991:TCC

[Hoa91e] C. A. R. Hoare. A theory of conjunction and concurrency: Keynote address. In ????, editor, Parallel Architectures (Parbase ’90), pages 18–27. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 1991.

Hoare:1991:TOP

[Hoa91f] C. A. R. Hoare. The transputer and occam: a personal story. Concurrency: Practice and Experience, 3(4):249–264, August 1991. CODEN CPEXEI. ISSN 1040-3108 (print), 1096-9128 (electronic).

Hoare:1992:AM

[Hoa92] C. A. R. Hoare. Algebra and models. In Manfred Broy, editor, Program Design Calculi, volume 118 of NATO Advanced Science Institutes Series F, pages 161–195. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1992.

Hoare:1993:AMa

[Hoa93a] C. A. R. Hoare. Algebra and models. ACM SIGSOFT Software Engineering Notes, 18(5):1–8, December 1993. CODEN SFENDP. ISSN 0163-5948 (print), 1943-5843 (electronic).

Hoare:1993:AMb

[Hoa93b] C. A. R. Hoare. Algebra and models. In Program Design Calculi, volume 118 of NATO ASI Series (Series F: Computer and Systems Sciences), pages 161–195. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1993.

Hoare:1993:MPM

[Hoa93c] C. A. R. Hoare. Mathematics of programming: Mathematical laws help programmers control the complexity of tasks. In T. R. Colburn, J. H. Fetzer, and T. L. Rankin, editors, Program Verification: Fundamental Issues in Computer Science, volume 14 of Studies in Cognitive Systems, pages 135–154. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1993. ISBN 94-010-4789-8; 94-011-1793-4. LCCN QA76.76.V47 .P764 1993.

Hoare:1993:PP

[Hoa93d] C. A. R. Hoare. Programs are predicates. ICOT Journal, 38(??): 2–15, ???? 1993. ISSN 0910-707X. Invited Lecture.

Hoare:1993:WSE

[Hoa93e] C. A. R. Hoare. Why software engineering at a communications meeting? In D. E. N. Davies, C. Hilsum, and A. W. Rudge, editors, Communications After AD 2000, pages 215–224. The Royal Society and Chapman Hall, ????, 1993.

Hoare:1994:F

[Hoa94a] C. A. R. Hoare. Foreword. In J. P. Bowen, editor, Real-Time Safety Critical Systems: Towards Verified Systems, volume 2, pages xvii– xviii. Elsevier, Amsterdam, The Netherlands, 1994.

Hoare:1994:GE

[Hoa94b] C. A. R. Hoare. Guest editorial. Journal of Logic and Computation, 4(3):215–216, 1994. CODEN JLCOEU. ISSN 0955-792X (print), 1465-363X (electronic).

Hoare:1994:UTP

[Hoa94c] C. A. R. Hoare. Unified theories of programming. Draft manuscript later published in [Hoa97]., 1994.

Hoare:1995:AM

[Hoa95] C. A. R. Hoare. Algebra and models. In I. Wand and Robin Milner, editors, Computing Tomorrow, pages 158–187. Cambridge University Press, Cambridge, UK, 1995.

Hoare:1996:AM

[Hoa96a] C. A. R. Hoare. Algebra and models. In Computing tomorrow, pages 158–187. Cambridge Univ. Press, Cambridge, 1996.

Hoare:1996:HDS

[Hoa96b] C. A. R. Hoare. How did software get so reliable without proof? In Marie-Claude Gaudel and James Woodcock, editors, FME’96: Industrial Benefit and Advances in Formal Methods, volume 1051 of Lecture Notes in Computer Science, pages 1–17. Springer-Ver-lag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1996. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic).

Hoare:1996:LED

[Hoa96c] C. A. R. Hoare. The logic of engineering design. Microprocessing and Microprogramming, 41(8-9):525–539, April 1996. CODEN MMICDT. ISSN 0165-6074 (print), 1878-7061 (electronic).

Hoare:1996:MMC

[Hoa96d] C. A. R. Hoare. Mathematical models for computing science. In Broy [Bro96], pages 115–164. ISBN 3-540-60947-4 (hardcover). LCCN QA76.9.D5 D38 1996.

Hoare:1996:PAB

[Hoa96e] C. A. R. Hoare. Preface to An axiomatic basis for computer programming. In ????, editor, Great Papers in Computer Science, chapter 137, page ?? West Publishing Co., ????, 1996.

Hoare:1996:PPA

[Hoa96f] C. A. R. Hoare. Preface to Preface to An axiomatic definition of the programming language. In ????, editor, Great Papers in Computer Science, chapter 139, page ?? West Publishing Co., ????, 1996.

Hoare:1996:PPC

[Hoa96g] C. A. R. Hoare. Preface to Proof of correctness of data representations. In ????, editor, Great Papers in Computer Science, chapter 138, page ?? West Publishing Co., ????, 1996.

Hoare:1996:PQ

[Hoa96h] C. A. R. Hoare. Preface to Quicksort. In ????, editor, Great Papers in Computer Science, chapter 140, page ?? West Publishing Co., ????, 1996.

Hoare:1996:UTC

[Hoa96i] C. A. R. Hoare. Unification of theories: a challenge for computing science. In Magne Haveraaen, Olaf Owe, and Ole-Johan Dahl, editors, Recent Trends in Data Type Specification (11th Workshop on Specification of Abstract Data Types 1995), volume 1130 of Lecture Notes in Computer Science, pages 49–57. Springer-Ver-lag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1996. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic).

Hoare:1996:UTP

[Hoa96j] C. A. R. Hoare. Unifying theories: a personal statement. ACM Computing Surveys, 28(4es):46:1–46:??, December 1996. CODEN CMSVAN. ISSN 0360-0300 (print), 1557-7341 (elec-

tronic). URL http://www.acm.org/pubs/citations/journals/
surveys/1996-28-4es/a46-hoare/.

Hoare:1997:UTPa

[Hoa97] C. A. R. Hoare. Unified theories of programming. In Mathematical methods in program development (Marktoberdorf, 1996), volume 158 of NATO Adv. Sci. Inst. Ser. F: Comput. Systems Sci., pages 313–367. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1997.

Hoare:1999:TPT

[Hoa99] C. A. R. Hoare. Theories of programming: Top-down and bottomup and meeting in the middle. In International Symposium on Formal Methods–FM’99, volume 1708 of Lecture Notes in Computer Science, pages 1–27. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1999.

Hoare:2000:HAF

[Hoa00a] C. A. R. Hoare. A hard act to follow. Higher-Order and Symbolic Computation, 13(1–2):71–72, April 2000. CODEN LSCOEX. ISSN 1388-3690 (print), 2212-0793 (electronic). URL http://www.

springerlink.com/openurl.asp?genre=article&issn=1388-
3690&volume=13&issue=1&spage=71;   http://www.wkap.nl/
oasis.htm/258019.

Hoare:2000:LC

[Hoa00b] C. A. R. Hoare. Legacy code [invited talk]. In ICFEM 2000. Third IEEE International Conference on Formal Engineering Methods, page 75. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 2000. URL https://

ieeexplore.ieee.org/document/873807.

Hoare:2000:SLI

[Hoa00c] C. A. R. Hoare. Stories from a life in interesting times. In Kyoto Prizes and Inamori Grants 2000, pages 112–138. The Inamori Foundation, Kyoto, Japan, 2000. ISBN 4-900663-16-

6. URL https://www.kyotoprize.org/wp-content/uploads/

2019/07/2000_A.pdf. Japanese and English side-by-side.

Hoare:2000:A

[Hoa00d] Tony Hoare. Assertions. In Wolfgang Grieskamp, Thomas Santen, and Bill Stoddart, editors, Integrated Formal Methods: Second International Conference, IFM 2000, Dagstuhl Castle, Germany, November 1–3, 2000 Proceedings, volume 1945 of Lecture Notes in Computer Science, pages 1–2. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2000. ISBN 3-540-40911-4 (e-book), 3-540-41196-8 (Paper). LCCN QA76.9.F67 .G754 2000.

Hoare:2001:ABC

[Hoa01a] C. A. R. Hoare. An axiomatic basis for computer programming. In Broy and Denert [BD01], pages 419–438. ISBN 3-540-42290-0 (print), 3-642-48354-2 (e-book). LCCN QA76.758. URL http:

//link.springer.com/chapter/10.1007/978-3-642-48354-7_
17/.

Hoare:2001:PCD

[Hoa01b] C. A. R. Hoare. Proof of correctness of data representations. In Broy and Denert [BD01], pages 439–451. ISBN 3-540-42290-0 (print), 3-642-48354-2 (e-book). LCCN QA76.758. URL http:

//link.springer.com/chapter/10.1007/978-3-642-48354-7_
18/.

Hoare:2001:L

[Hoa01c] Tony Hoare. Legacy. Information Processing Letters, 77(2–4): 123–129, February 28, 2001. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic). URL http://www.elsevier.nl/

gej-ng/10/23/20/68/29/34/abstract.html;   http://www.
elsevier.nl/gej-ng/10/23/20/68/29/34/article.pdf.

Hoare:2002:APP

[Hoa02a] C. A. R. Hoare. Assertions: a personal perspective. In Broy and Denert [BD02], pages 356–366. ISBN 3-540-43081-4, 3-642-48354-2 (e-book), 3-642-59412-3 (e-book), 3-642-59413-1, 3-642-63970-4 (print). LCCN QA76.2.A2 S62 2002. URL

http://aleph.unisg.ch/hsgscan/hm00048094.pdf;   http:
//link.springer.com/10.1007/978-3-642-59412-0;   http:
//www.loc.gov/catdir/enhancements/fy0817/2002070484-d.
html;   http://www.springerlink.com/content/978-3-642-
48354-7;   z3950.loc.gov:7090/Voyager.

Hoare:2002:APV

[Hoa02b] C. A. R. Hoare. Assertions and program verification. In Broy and Denert [BD02], page ?? ISBN 3-540-43081-4, 3-642-48354-2 (e-book), 3-642-59412-3 (e-book), 3-642-59413-1, 3-642-63970-4 (print). LCCN QA76.2.A2 S62 2002. URL

http://aleph.unisg.ch/hsgscan/hm00048094.pdf;   http:
//link.springer.com/10.1007/978-3-642-59412-0;   http:
//www.loc.gov/catdir/enhancements/fy0817/2002070484-d.
html;   http://www.springerlink.com/content/978-3-642-
48354-7;   z3950.loc.gov:7090/Voyager.

Hoare:2002:ABC

[Hoa02c] C. A. R. Hoare. An axiomatic basis for computer programming. In Broy and Denert [BD02], pages 367–383. ISBN 3-540-43081-4, 3-642-48354-2 (e-book), 3-642-59412-3 (e-book), 3-642-59413-1, 3-642-63970-4 (print). LCCN QA76.2.A2 S62 2002. URL

http://aleph.unisg.ch/hsgscan/hm00048094.pdf;   http:
//link.springer.com/10.1007/978-3-642-59412-0;   http:
//www.loc.gov/catdir/enhancements/fy0817/2002070484-d.
html;   http://www.springerlink.com/content/978-3-642-
48354-7;   z3950.loc.gov:7090/Voyager.

Hoare:2002:CSP

[Hoa02d] C. A. R. Hoare. Communicating sequential processes. In Brinch Hansen [Bri02], pages 413–443. ISBN 0-387-95401-5, 1-4419-2986-X, 1-4757-3472-7, 1-4757-3472-7. LCCN QA76.642 .O75

2002. URL http://link.springer.com/10.1007/978-1-4757-
3472-0.

Hoare:2002:MOS

[Hoa02e] C. A. R. Hoare. Monitors: an operating system structuring concept. In Brinch Hansen [Bri02], pages 272–294. ISBN 0-387-95401-5, 1-4419-2986-X, 1-4757-3472-7, 1-4757-3472-7. LCCN QA76.642

.O75 2002. URL http://link.springer.com/10.1007/978-1-
4757-3472-0.

Hoare:2002:PCD

[Hoa02f] C. A. R. Hoare. Proof of correctness of data representations. In Broy and Denert [BD02], pages 385–396. ISBN 3-540-43081-4, 3-642-48354-2 (e-book), 3-642-59412-3 (e-book), 3-642-59413-1, 3-642-63970-4 (print). LCCN QA76.2.A2 S62 2002. URL

http://aleph.unisg.ch/hsgscan/hm00048094.pdf;   http:
//link.springer.com/10.1007/978-3-642-59412-0;   http:
//www.loc.gov/catdir/enhancements/fy0817/2002070484-d.
html;   http://www.springerlink.com/content/978-3-642-
48354-7;   z3950.loc.gov:7090/Voyager.

Hoare:2002:TTP

[Hoa02g] C. A. R. Hoare. Towards a theory of parallel programming. In Brinch Hansen [Bri02], pages 231–244. ISBN 0-387-95401-5, 1-4419-2986-X, 1-4757-3472-7, 1-4757-3472-7. LCCN QA76.642 .O75

2002. URL https://doi.org/10.1007/978-1-4757-3472-0_6.

Hoare:2002:LLU

[Hoa02h] Charles Antony Richard Hoare. Learning to love uncertainty. Times Higher Education Supplement, ??(1529):26, ???? ??, 2002. ISSN 0049-3929.

Hoare:2002:APS

[Hoa02i] Professor Sir Tony Hoare. Assertions in programming: From scientific theory to engineering practice. In D. Bustard, W. Liu, and R. Sterritt, editors, Soft-Ware 2002: Computing in an Imperfect World, volume 2311 of Lecture Notes in Computer Science, pages 350–351. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2002. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic). URL http:

//link.springer-ny.com/link/service/series/0558/bibs/
2311/23110350.htm;   http://link.springer-ny.com/link/
service/series/0558/papers/2311/23110350.pdf.

Hoare:2002:AMS

[Hoa02j] Tony Hoare. Assertions in modern software engineering practice. In IEEE [IEE02], page 459. ISBN 0-7695-1727-7 (paperback), 0-7695-1728-5 (case), 0-7695-1729-3 (microfiche). LCCN QA76.6

I615 2002. URL http://ieeexplore.ieee.org/servlet/opac?
punumber=8094.

Hoare:2003:A

[Hoa03a] C. A. R. Hoare. Assertions. In Broy and Pizka [BP03], pages 291–316. ISBN 1-58603-342-5, 4-274-90589-6 (Ohmsha). LCCN QA76.76.D47 N37 2002. URL http://books.google.

com/books?id=TK1QAAAAYAAJ;   http://books.google.com/
books?id=U6VQAAAAMAAJ;   http://catalog.hathitrust.org/
api/volumes/oclc/53998323.html.

Hoare:2003:APP

[Hoa03b] C. A. R. Hoare. Assertions: a personal perspective. IEEE Annals of the History of Computing, 25(2):14–25, April/ June 2003. CODEN IAHCEX. ISSN 1058-6180 (print),

1934-1547 (electronic). URL http://csdl.computer.org/dl/
mags/an/2003/02/a2014.htm;   http://csdl.computer.org/
dl/mags/an/2003/02/a2014.pdf;   http://csdl.computer.
org/dl/mags/an/2003/02/a2014abs.htm.

Hoare:2003:KTK

[Hoa03c] Charles Antony Richard Hoare. King toppled by knights in quest for computing holy grail. Times Higher Education Supplement, ?? (1575):26, ???? ??, 2003. ISSN 0049-3929.

Hoare:2003:EWD

[Hoa03d] Tony Hoare. Edsger Wybe Dijkstra. Physics Today, 56(3):96, 98, March 2003. CODEN PHTOAD. ISSN 0031-9228 (print), 1945-0699 (electronic).

Hoare:2003:TVC

[Hoa03e] Tony Hoare. Towards the verifying compiler. In Formal Methods at the Crossroads. From Panacea to Foundational Support, pages 151–160. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2003.

Hoare:2003:VC

[Hoa03f] Tony Hoare. The verifying compiler. Journal of the ACM, 50(1): 63–69, January 2003. CODEN JACOAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Hoare:2003:VCGa

[Hoa03g] Tony Hoare. The verifying compiler: a grand challenge for computing research. In Compiler Construction, volume 2622 of ser-LNCS, pages 262–272. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2003.

Hoare:2003:VCGb

[Hoa03h] Tony Hoare. The verifying compiler: a grand challenge for computing research. Journal of the ACM, 50(1):63–69, January 2003. CO-DEN JACOAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Hoare:2004:FSP

[Hoa04a] Charles Antony Richard Hoare. Fractional shifts produce sweet sound of spheres. Times Higher Education Supplement, ??(1640): 29, ???? ??, 2004. ISSN 0049-3929.

Hoare:2004:AA

[Hoa04b] Charles Antony Richard Hoare. From an amp to an atom. Times Higher Education Supplement, ??(1608):28, ???? ??, 2004. ISSN 0049-3929.

Hoare:2004:VIF

[Hoa04c] Charles Antony Richard Hoare. Visions of Iris flitting through the universe with a peeled grape. Times Higher Education Supplement, ??(1621):22, ???? ??, 2004. ISSN 0049-3929.

Hoare:2004:YWT

[Hoa04d] Charles Antony Richard Hoare. Yes we think, but not like a machine does. Times Higher Education Supplement, ??(1663):26, ???? ??, 2004. ISSN 0049-3929.

Hoare:2004:GCC

[Hoa04e] Tony Hoare. Grand challenges for computing research. In Herbert and Jones [HJ04], pages 117–123. ISBN 0-387-20170-X. LCCN QA76.9.S88 H45 2004.

Hoare:2004:TVC

[Hoa04f] Tony Hoare. Towards the verifying compiler. In Owe et al. [OKL04], pages 124–136. ISBN 3-540-21366-X, 3-540-39993-3 (e-

book). LCCN QA76.758. URL http://link.springer.com/10.
1007/b96089.

Hoare:2005:VCG

[Hoa05a] C. A. R. Hoare. The verifying compiler, a grand challenge for computing research. In Verification, model checking, and abstract interpretation, volume 3385 of Lecture Notes in Computer Science, page 78. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2005.

Hoare:2005:PAUa

[Hoa05b] Tony Hoare. Process algebra: a unifying approach. In Abdallah et al. [AJS05], pages 36–60. CODEN LNCSD9. ISBN 3-540-25813-2 (paperback), 3-540-32265-5 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.73.C75 S96 2004eb. URL

http://www.springerlink.com/content/978-3-540-25813-1;
 http://www.springerlink.com/openurl.asp?genre=issue&
issn=0302-9743&volume=3525;   http://www.springerlink.
com/openurl.asp?genre=volume&id=doi:10.1007/b136154.

Hoare:2005:PAUb

[Hoa05c] Tony Hoare. Process algebra: a unifying approach. In Broy et al. [BGHH05], pages 257–283. ISBN 1-4020-3530-6 (hardcover), 1-4020-3531-4 (paperback), 1-4020-3532-2 (e-book), 1-280-28396-3. LCCN QA76.758 .N385 2004. URL https://link.springer.

com/content/pdf/10.1007/1-4020-3532-2_9.pdf.

Hoare:2006:IVS

[Hoa06a] Tony Hoare. The ideal of verified software (invited talk). In Computer aided verification, volume 4144 of Lecture Notes in Computer Science, pages 5–16. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2006.

Hoare:2006:WEC

[Hoa06b] Tony Hoare. Why ever CSP? Electronic Notes in Theoretical Computer Science, 162:209–215, September 2006. ISSN 1571-0661.

Hoare:2007:CT

[Hoa07a] Tony Hoare. Compensable transactions. In Broy et al. [BGH07], pages 116–134. ISBN 1-4294-9223-6 (e-book), 1-4337-0874-4, 1-58603-731-5 (hardcover). ISSN 1574-5589 (print), 1879-8284 (electronic). LCCN QA76.76R44 S66. URL http://catdir.loc.gov/

catdir/toc/fy0802/2007922976.html.

Hoare:2007:IPC

[Hoa07b] Tony Hoare. The ideal of program correctness: Third Computer Journal Lecture. The Computer Journal, 50(3):254–260, May 2007. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-2067

(electronic). URL http://comjnl.oxfordjournals.org/cgi/
content/full/50/3/254;   http://comjnl.oxfordjournals.
org/cgi/reprint/50/3/254. See [Ano07a, Ano07b].

Hoare:2007:SEC

[Hoa07c] Tony Hoare. Science and engineering: a collusion of cultures. In 37th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN’07), pages 2–9. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, June 2007.

Hoare:2008:VFG

[Hoa08] Tony Hoare. Verification of fine-grain concurrent programs. Electronic Notes in Theoretical Computer Science, 209:165–171, 2008. ISSN 1571-0661.

Hoare:2009:VRA

[Hoa09] C. A. R. Hoare. Viewpoint: Retrospective: an axiomatic basis for computer programming. Communications of the ACM, 52(10): 30–32, October 2009. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Hoare:2010:MJD

[Hoa10a] C. A. R. Hoare. The Michael Jackson design technique: A study of the theory with applications. In B. Nuseibeh and P. Zave, editors, Software Requirements and Design: The Work of Michael Jackson, page ?? Good Friends Publishing Company,

2010. URL https://www.semanticscholar.org/paper/The-
Michael-Jackson-Design-Technique-%3A-A-study-of-Hoare/
eac2a5102a065f176d3b4dfbe5edc11299a5676d?p2df.

Hoare:2010:TPH

[Hoa10b] C. A. R. Hoare. Testing and proving, hand in hand. In Bottaci and Fraser [BF10], pages 5–6. ISBN 3-642-15584-7 (paperback), 3-642-15585-5 (e-book). LCCN QA76.76.T48 T47 2010. URL https://

dl.acm.org/doi/abs/10.5555/1885930.1885933.

Hoare:2010:CT

[Hoa10c] Tony Hoare. Compensable transactions. In Müller [Mül10], pages 21–40. ISBN 3-642-13009-7 (paperback), 3-642-13010-0. LCCN

QA76.758 .A38 2010. URL https://dl.acm.org/doi/abs/10.
5555/2167938.2167940.

Hoare:2010:FGCa

[Hoa10d] Tony Hoare. Fine-grain concurrency. In Müller [Mül10], pages 1–20. ISBN 3-642-13009-7 (paperback), 3-642-13010-0. LCCN

QA76.758 .A38 2010. URL https://dl.acm.org/doi/abs/10.
5555/2167938.2167940.

Hoare:2010:FGCb

[Hoa10e] Tony Hoare. Fine-grain concurrency. Concurrency and Computation: Practice and Experience, 22(8):912–934, June 10, 2010. CO-DEN CCPEBO. ISSN 1532-0626 (print), 1532-0634 (electronic).

Hoare:2011:RB

[Hoa11] Tony Hoare. Recovery blocks. In Jones and Lloyd [JL11], pages 261–266. ISBN 3-642-24540-4 (paperback), 3-642-24541-2

(e-book). LCCN QA76.17. URL http://link.springer.com/
chapter/10.1007/978-3-642-24541-1_19/.

Hoare:2012:MT

[Hoa12a] Tony Hoare. Message of thanks: On the receipt of the 2011 ACM SIGPLAN Distinguished Achievement Award. In John Field and Michael Hicks, editors, Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages — POPL ’12, Philadelphia, Pennsylvania, USA, January 22–28, 2012, pages 3–6. ACM Press, New York, NY 10036, USA, 2012.

Hoare:2012:MTR

[Hoa12b] Tony Hoare. Message of thanks: on the receipt of the 2011 ACM SIGPLAN distinguished achievement award. ACM SIGPLAN Notices, 47(1):3–6, January 2012. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Hoare:2012:NMC

[Hoa12c] Tony Hoare. Net models for concurrent object behaviour. In Haddad and Pomello [HP12], pages 1–2. CODEN LNCSD9. ISBN 3-642-31131-8. ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA75.5-76.95. URL http://link.springer.com/

accesspage/chapter/10.1007/978-3-642-31131-4_1.

Hoare:2013:GML

[Hoa13a] Tony Hoare. Generic models of the laws of programming. In Liu et al. [LWZ13], pages 213–226. ISBN 3-642-39697-6 (print), 3-642-39698-4 (e-book). ISSN 0302-9743. LCCN QA75.5-76.95.

Hoare:2013:LPC

[Hoa13b] Tony Hoare. Laws of programming with concurrency. In Jones and Ng [JN13], page 1. ISBN 3-939897-63-9. ISSN 2190-6807.

URL http://drops.dagstuhl.de/opus/volltexte/2013/4284/

. Invited talk.

Hoare:2013:USC

[Hoa13c] Tony Hoare. Unifying semantics for concurrent programming. In Computation, Logic, Games, and Quantum Foundations. The Many Facets of Samson Abramsky, volume 7860 of Lecture Notes in Computer Science, pages 139–149. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2013.

Hoare:2014:LCP

[Hoa14] Tony Hoare. Laws of concurrent programming. ACM SIGPLAN Notices, 49(6):168, June 2014. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Hoare:2021:CSP

[Hoa21a] C. A. R. Hoare. Communicating sequential processes. In Jones and Misra [JM21f], pages 157–186. ISBN 1-4503-8728-4. LCCN QA76.6.

Hoare:2021:ATA

[Hoa21b] Tony Hoare. The 1980 ACM Turing Award Lecture. In Jones and Misra [JM21f], pages 1–22. ISBN 1-4503-8728-4. LCCN QA76.6.

Hoare:2021:E

[Hoa21c] Tony Hoare. Envoi. In Jones and Misra [JM21f], pages 347–356. ISBN 1-4503-8728-4. LCCN QA76.6.

Hoare:2022:FYE

[Hoa22] Tony Hoare. Forty years with Edsger. In Apt and Hoare [AH22], chapter 25, pages 411–422. ISBN 1-4503-9771-9 (paperback), 1-4503-9772-7 (epub), 1-4503-9773-5 (hardcover), 1-4503-9774-3 (ebook). ISSN 2374-6777. LCCN DS119 .A685 2022.

Hoofman:1991:WEM

[Hoo91] R. Hoofman. Weakly expressive models for Hoare logic. Theoretical Computer Science, 82(2):409–418, May 31, 1991. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Hooman:1992:CVR

[Hoo92] J. Hooman. Compositional verification of real-time systems using extended Hoare triples. Lecture Notes in Computer Science, 600: 252–??, 1992. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic).

Hooman:1994:EHL

[Hoo94] Jozef Hooman. Extending Hoare logic to real-time. Formal Aspects of Computing, 6(1S):801–825, 1994. CODEN FACME5. ISSN 0934-5043 (print), 1433-299X (electronic). URL http://link.

springer.com/article/10.1007/BF01213604.

Horning:1989:BRE

[Hor89] J. J. Horning. Book review: Essays in computing science, by C. A. R. Hoare and C. B. Jones, ed., Prentice-Hall International, Hemel Hempstead, United Kingdom, 1989, Price £32.95 (hardback), ISBN 0-13-284027-8. Science of Computer Programming, 12(3):267–270, September 1989. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic). URL http://www.

sciencedirect.com/science/article/pii/0167642389900105.

Hoare:1972:OST

[HP72] C. A. R. Hoare and Ronald H. Perrott, editors. Operating Systems Techniques, Proceedings of a Seminar at Queen’s University, Belfast, Northern Ireland, August–September 1971, volume 9 of A.P.I.C. studies in data processing. Academic Press, New York, USA, 1972. ISBN 0-12-350650-6. LCCN QA76.6 .I57 1971; TA168.

URL http://brinch-hansen.net/papers/1971a.pdf.

Hoare:1994:HSCb

[HP94a] C. A. R. Hoare and I. Page. Hardware and software: The closing gap. Transputer Communications, 2(2):69–90, June 1994. CODEN TCOMET. ISSN 1070-454X.

Hoare:1994:HSCa

[HP94b] C. A. R. Hoare and Innes Page. Hardware and software: The closing gap. In Jürg Gutknecht, editor, Programming Languages and System Architectures: International Conference, Zurich, Switzerland, March 2–4, 1994. Proceedings, volume 782 of Lecture Notes in Computer Science, pages 49–68. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1994. CO-DEN LNCSD9. ISBN 3-540-57840-4 (paperback), 3-540-48356-X (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic).

Haddad:2012:ATP

[HP12] Serge Haddad and Lucia Pomello, editors. Application and Theory of Petri Nets: 33rd International Conference, PETRI NETS 2012, Hamburg, Germany, June 25–29, 2012. Proceedings, volume 7347 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2012. CODEN LNCSD9. ISBN 3-642-31131-8. ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA75.5-76.95. URL https:

//link.springer.com/book/10.1007/978-3-642-31131-4.

Hoare:1993:PPT

[HPGM93] C. A. R. Hoare, I. Page, M. Giles, and R. McLatchie. Parallel processing: Theoretical foundations. Oxford Innovation News, 8:

2–11, Winter 1993. URL http://www.cs.ox.ac.uk/files/6115/
H93%20-%20Parallel.pdf.

Hoare:1984:PEP

[HR84] C. A. R. Hoare and A. W. Roscoe. Programs as executable predicates. In ????, editor, Proceedings of the International Conference on Fifth Generation Computer Systems, November 6–9 1984, Tokyo, Japan, pages 220–228. Institute for New Generation Computer Technology, Tokyo, Japan, 1984.

Hoare:1985:MLP

[HS85] C. A. R. Hoare and J. C. Shepherdson, editors. Mathematical Logic and Programming Languages. Prentice-Hall International, Englewood Cliffs, NJ, USA, 1985. ISBN 0-13-561465-1. 184 pp. LCCN QA76.6 .M3646 1985. A Discussion Meeting of the Royal Society of London.

Hoare:1994:ACO

[HS94] C. A. R. Hoare and A. Sampaio. An algebraic characterisation of operational semantics. Technical Report ????, Oxford University Computing Laboratory, Oxford, UK, 1994.

Hoare:2010:UCT

[HS10] Tony Hoare and Natarajan Shankar. Unraveling a card trick. In Manna and Peled [MP10], pages 195–201. ISBN 3-642-15584-7 (paperback), 3-642-15585-5 (e-book). LCCN QA76.76.V47 T56 2010.

Hoare:2019:CSTa

[HSW19a] Tony Hoare, Georg Struth, and Jim Woodcock. A calculus of space, time, and causality: its algebra, geometry, logic. In Unifying theories of programming, volume 11885 of Lecture Notes in Computer Science, pages 3–21. Springer, Cham, 2019.

Hoare:2019:CST

[HSW19b] Tony Hoare, Georg Struth, and Jim Woodcock. A calculus of space, time, and causality: Its algebra, geometry, logic. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 3–21. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.6 .U86

2019. URL http://link.springer.com/.

Hartog:2002:VPP

[HV02] J. I. D. Hartog and E. P. D. Vink. Verifying probabilistic programs using a Hoare like logic. International Journal of Foundations of Computer Science (IJFCS), 13(3):315–??, 2002. CODEN IFCSEN. ISSN 0129-0541 (print), 1793-6373 (electronic).

Hoare:2012:PA

[HvS12a] Tony Hoare and Stephan van Staden. In praise of algebra. Formal Aspects of Computing, 24(4–6):423–431, July 2012. CO-DEN FACME5. ISSN 0934-5043 (print), 1433-299X (elec-

tronic). URL http://link.springer.com/article/10.1007/
s00165-012-0249-0.

Hoare:2012:LPU

[HvS12b] Tony Hoare and Stephan van Staden. The laws of programming unify process calculi. In Gibbons and Nogueira [GN12], pages 7–22. CODEN LNCSD9. ISBN 3-642-31112-1 (print), 3-642-31113-X (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.9.M65 M63 2012. URL http://link.springer.

com/chapter/10.1007/978-3-642-31113-0_2/.

Hoare:2014:LPU

[HvS14] Tony Hoare and Stephan van Staden. The laws of programming unify process calculi. Science of Computer Programming, 85((part B)):102–114, June 1, 2014. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic).

URL http://www.sciencedirect.com/science/article/pii/
S0167642313002207.

Hoare:2014:DCK

[HvSM^{+}14] Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, Jules Villard, Huibiao Zhu, and Peter O’Hearn. Developments in concurrent Kleene algebra. In Höfner et al. [HJKM14], pages 1–18. ISBN 3-319-06250-6 (paperback), 3-319-06251-4 (e-book). LCCN QA8.9-QA10.3; QA76.9.M35 R36 2014. URL https://doi.org/

10.1007/978-3-319-06251-8.

Hoare:2016:DCK

[HvSM^{+}16] Tony Hoare, Stephan van Staden, Bernhard Möller, Georg Struth, and Huibiao Zhu. Developments in concurrent Kleene algebra. J.

Log. Algebr. Methods Program., 85(4):617–636, 2016. ISSN 2352-2208.

Hoare:1966:PSA

[HW66] C. A. R. Hoare and N. Wirth. A proposal for a successor to AL-GOL 60. Communications of the ACM, 9(7):??, July 1966. URL

????.

Hoare:1972:ADP

[HW72] C. A. R. Hoare and Niklaus Wirth. An axiomatic definition of the programming language PASCAL. Report, ETH Zürich, Zürich, Switzerland, November 1972. v + 29 pp.

URL https://www.research-collection.ethz.ch/bitstream/
handle/20.500.11850/68663/eth-3028-01.pdf.

Hoare:1973:ADP

[HW73] C. A. R. Hoare and Niklaus Wirth. An axiomatic definition of the programming language Pascal. Acta Informatica, 2(4):335– 355, December 1973. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic). See addenda and corrigenda [HW74].

Hoare:1974:ACA

[HW74] C. A. R. Hoare and N. Wirth. Addenda and corrigenda to An Axiomatic Definition of the Programming Language Pascal. Acta Informatica, 3(3):296, July 22, 1974. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic). See [HW73].

Hoare:2004:RMN

[HW04] Tony Hoare and Maurice V. Wilkes. Roger Michael Needham CBE FREng. 9 February 1935–1 March 2003. Biographical Memoirs of Fellows of the Royal Society, 50:183–199, January 2004. CODEN BMFRA3. ISSN 0080-4606 (print), 1748-8494 (electronic).

Hoare:2011:UMD

[HW11] C. A. R. Hoare and J. Wickerson. Unifying models of data flow. In Broy et al. [BLH11], pages 211–230. ISBN 1-60750-710-2 (hardcover), 1-60750-711-0 (e-book). ISSN 1874-6268 (print), 1879-8292 (electronic). LCCN QA76.9.A25 S64 2011; QA76.76.P76 S64 2011.

URL http://www.gbv.de/dms/tib-ub-hannover/655827013.
pdf;   https://ebooks.iospress.nl/volume/software-and-
systems-safety.

Hoare:1981:PCC

[HZ81] C. A. R. Hoare and Chaochen Zhou. Partial correctness of communicating processes and protocols. Technical Report PRG 20, Programming Research Group, Oxford University Computing Laboratory, Oxford, UK, May 1981. ii + 23 pp. URL https://www.

cs.ox.ac.uk/files/3241/PRG20.pdf.

Hoare:1982:CCT

[HZ82] C. A. R. Hoare and C. C. Zhou. The consistency of the calculus of total correctness for communicating processes. Technical Monograph PRG-26, Oxford University Computing Laboratory, Programming Research Group, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, February 1982. URL http://www.cs.

ox.ac.uk/files/3292/PRG26.pdf.

Hoare:1990:MSS

[HZ90] C. A. R. Hoare and Chao Chen Zhou. A model for synchronous switching circuits and its theory of correctness. In ????, editor, Designing Correct Circuits, pages 196–211. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1990.

IEEE:1976:ASF

[IEE76] IEEE, editor. 17th annual Symposium on Foundations of Computer Science, October 25–27, 1976, Houston, Texas. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 1976. CODEN ASFPDV. ISBN ???? ISSN 0272-5428. LCCN QA75.5 .S97 1976.

URL https://ieeexplore.ieee.org/xpl/conhome/4567877/
proceeding?isnumber=4567878. IEEE catalog number CH1133-8

C.

IEEE:1988:ASL

[IEE88] IEEE, editor. 3rd Annual Symposium on Logic in Computer Science: proceedings, July 5–8, 1988, Edinburgh, Scotland. Computer Society Press, Washington, DC, USA, 1988. ISBN 0-8186-0853-6 (paperback); 0-8186-4853-8 (microfiche). LCCN QA76.9.M35 S94 1988. Computer Society order number 853. IEEE catalog number 88CH2608-8.

IEEE:2000:PSA

[IEE00] IEEE, editor. Proceedings Seventh Asia-Pacific Software Engeering Conference. APSEC 2000. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 2000.

ISBN 0-7695-0915-0, 0-7695-0916-9 (casebound), 0-7695-0917-7 (microfiche). ISSN 1530-1362. LCCN QA76.758 .A77 2000.

IEEE:2002:AIC

[IEE02] IEEE, editor. 26th Annual International Computer Software and Applications Conference: 26–29 August 2002, Oxford, England. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 2002. ISBN 0-7695-1727-7 (paperback), 0-7695-1728-5 (case), 0-7695-1729-3 (microfiche).

LCCN QA76.6 I615 2002. URL http://ieeexplore.ieee.org/
servlet/opac?punumber=8094.

Jacobs:2015:DHM

[Jac15] Bart Jacobs. Dijkstra and Hoare monads in monadic computation. Theoretical Computer Science, 604(??):30–45, November 2, 2015. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294

(electronic). URL http://www.sciencedirect.com/science/
article/pii/S0304397515002364.

JaJa:2000:PQ

[JaJ00] Joseph JaJa. A perspective on quicksort. Computing in Science and Engineering, 2(1):43–49, January/February 2000. CODEN CSENFA. ISSN 1521-9615 (print), 1558-366X (elec-

tronic). URL http://dlib.computer.org/cs/books/cs2000/
pdf/c1043.pdf;   http://www.computer.org/cse/cs1999/c1043abs.
htm.

Johnston:1975:MRE

[JH75] H. C. Johnston and C. A. R. Hoare. Matrix reduction — an efficient method (school timetables). Communications of the ACM, 18(3):141–150, March 1975. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Josephs:1989:TAP

[JHH89] M. B. Josephs, C. A. R. Hoare, and J. He. A theory of asynchronous processes. Technical Report TR-6-89, Oxford University Computing Laboratory, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, 1989.

Jones:2011:DHC

[JL11] Cliff B. Jones and John L. Lloyd, editors. Dependable and Historic Computing: Essays Dedicated to Brian Randell on the Occasion of His 75th Birthday, volume 6875 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2011. ISBN 3-642-24540-4 (paperback), 3-642-24541-2 (e-book). xii + 523 + 137 pp. LCCN QA76.17.

Jones:2021:FEA

[JM21a] Cliff Jones and Jayadev Misra. Finding effective abstractions. In Jones and Misra [JM21f], pages 23–40. ISBN 1-4503-8728-4. LCCN QA76.6.

Jones:2021:P

[JM21b] Cliff Jones and Jayadev Misra. Preface. In Jones and Misra [JM21f], pages xx + 430. ISBN 1-4503-8728-4. LCCN QA76.6.

Jones:2021:AI

[JM21c] Cliff B. Jones and Jayadev Misra. ACM interview. In Theories of Programming: The Life and Works of Tony Hoare [JM21f], pages 359–386. ISBN 1-4503-8728-4. LCCN QA76.6.

Jones:2021:ABI

[JM21d] Cliff B. Jones and Jayadev Misra. Authors’ biographies/index. In Theories of Programming: The Life and Works of Tony Hoare [JM21f], pages 413–420. ISBN 1-4503-8728-4. LCCN QA76.6.

Jones:2021:DS

[JM21e] Cliff B. Jones and Jayadev Misra. Doctoral students. In Theories of Programming: The Life and Works of Tony Hoare [JM21f], pages 393–394. ISBN 1-4503-8728-4. LCCN QA76.6.

Jones:2021:TPL

[JM21f] Cliff B. Jones and Jayadev Misra, editors. Theories of Programming: The Life and Works of Tony Hoare. ACM Press, New York, NY 10036, USA, 2021. ISBN 1-4503-8728-4. xx + 430 pp. LCCN QA76.6.

Joseph:1987:PRF

[JMS87] Mathai Joseph, Abha Moitra, and Neelam Soundararajan. Proof rules for fault tolerant distributed programs. Science of Computer Programming, 8(1):43–67, February 1987. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic).

Jones:2013:ICC

[JN13] Andrew V. Jones and Nicholas Ng, editors. 2013 Imperial College Computing Student Workshop: ICCSW’13 September 26–27, 2013, London, United Kingdom, volume 35 of Open Access Series in Informatics (OASIcs). Schloss Dagstuhl — Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 2013. ISBN 3-939897-63-9. ISSN 2190-6807. URL http://www.

dagstuhl.de/dagpub/978-3-939897-63-7;   https://drops.
dagstuhl.de/opus/volltexte/2013/4349;   https://drops.
dagstuhl.de/opus/volltexte/2013/4349/pdf/oasics_vol35_
iccsw2013_complete_volume.pdf.

Jones:2021:LTH

[Jon21] Cliff Jones. List of Tony Hoare’s publications. In Jones and Misra [JM21f], pages 395–410. ISBN 1-4503-8728-4. LCCN QA76.6.

Jones:1999:SIE

[JRH^{+}99] Simon Peyton Jones, Alastair Reid, Fergus Henderson, Tony Hoare, and Simon Marlow. A semantics for imprecise exceptions. ACM SIGPLAN Notices, 34(5):25–36, May 1999. CODEN SIN-ODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Jones:2010:RWC

[JRW10] Cliff B. Jones, A. W. Roscoe, and Kenneth R. Wood, editors. Reflections on the work of C. A. R. Hoare. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2010. ISBN 1-4471-6152-1, 1-84882-911-6 (hardcover), 1-84882-912-4 (e-book), 1-84882-917-5. xii + 430 pp. LCCN QA76 .R44 2010.

Jones:2001:PRR

[JTH01] S. P. Jones, A. Tolmach, and C. A. R. Hoare. Playing by the rules: Rewriting as a practical optimisation technique. In ????, editor, Haskell Workshop, pages 1–13. ACM Press, New York,

NY 10036, USA, 2001. URL http://citeseerx.ist.psu.edu/
viewdoc/summary?doi=10.1.1.22.1486.

Kapur:1992:ADC

[Kap92] Deepak Kapur, editor. Automated deduction, CADE-11: 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15–18, 1992: proceedings, volume 607 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1992. ISBN 3-540-55602-8. LCCN QA76.9.A96I57 1992.

Kernighan:1981:WPM

[Ker81] Brian W. Kernighan. Why Pascal is not my favorite programming language. Computer Science Report 100, AT&T Bell Laboratories, Murray Hill, NJ 07974, USA, July 1981. URL http://cm.bell-

labs.com/cm/cs/cstr/100.ps.gz. Published in [Ker84]. See also

[WSH77].

Kernighan:1984:WPM

[Ker84] Brian W. Kernighan. Why Pascal is not my favorite programming language. In Feuer and Gehani [FG84], pages 170–186. ISBN 0-13-154840-9 (paperback), 0-13-154857-3 (hardcover). LCCN QA76.73.A35 C66 1984. See also [WSH77, Ker81].

Kennaway:1980:TN

[KH80] J. R. Kennaway and C. A. R. Hoare. A theory of nondeterminism. In Automata, languages and programming (Proc. Seventh Internat. Colloq., Noordwijkerhout, 1980), volume 85 of Lecture Notes in Computer Science, pages 338–350. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1980.

Kaubisch:1982:DES

[KH82] W. H. Kaubisch and C. A. R. Hoareo. Discrete event simulation based on communicating sequential processes. In M. Broy and G. Schmidt, editors, Theoretical Foundations of Programming Methodology – Lecture Notes of an International Summer School, Germany, 1981, pages 625–642. D. Reidel, Dordrecht, The Netherlands; Boston, MA, USA; Lancaster, UK; Tokyo, Japan, 1982.

Khoar:1989:CVC

[Kho89] Ch. Khoar. Vzaimodeĭ stvuyushchie posledovatel′nye protsessy. “Mir”, Moscow, 1989. ISBN 5-03-001043-2. 264 pp. Translated from the English by A. A. Bul′onkova, Translation edited and with a foreword by A. P. Ershov.

Kojima:2017:HLG

[KI17] Kensuke Kojima and Atsushi Igarashi. A Hoare logic for GPU kernels. ACM Transactions on Computational Logic, 18(1):3:1– 3:??, April 2017. CODEN ???? ISSN 1529-3785 (print), 1557-945X (electronic).

Kirkerud:1982:CHC

[Kir82] Bjørn Kirkerud. Completeness of Hoare-calculi revisited. BIT, 22(4):401–418, December 1982. CODEN BITTEL, NBITAB. ISSN 0006-3835 (print), 1572-9125 (electronic). URL http:

//www.springerlink.com/openurl.asp?genre=article&issn=
0006-3835&volume=22&issue=4&spage=401.

Kleymann:1999:HLA

[Kle99] Thomas Kleymann. Hoare logic and auxiliary variables. Formal Aspects of Computing, 11(5):541–566, December 1999. CODEN FACME5. ISSN 0934-5043 (print), 1433-299X (electronic). URL

http://link.springer.com/article/10.1007/s001650050057.

Knijnenburg:1992:CIP

[KN92] P. M. W. Knijnenburg and F. Nordemann. A categorical interpretation of partial function logic and Hoare logic. Lecture Notes in Computer Science, 620:229–??, 1992. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic).

Kapur:1994:OTP

[KNM94] D. Kapur, X. Nie, and D. R. Musser. An overview of the Tecton proof system. Theoretical Computer Science, 133(2):307–340, October 24, 1994. CODEN TCSCDI. ISSN 0304-3975 (print),

1879-2294 (electronic). URL http://www.elsevier.com/cgi-
bin/cas/tree/store/tcs/cas_sub/browse/browse.cgi?year=
1994&volume=133&issue=2&aid=1712.

Kozen:2000:HLK

[Koz00] Dexter Kozen. On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic, 1(1):60–76, July 2000. CODEN ???? ISSN 1529-3785 (print), 1557-945X (elec-

tronic). URL http://www.acm.org/pubs/citations/journals/
tocl/2000-1-1/p60-kozen/.

Kirschenhofer:1998:CHF

[KP98] Peter Kirschenhofer and Helmut Prodinger. Comparisons in Hoare’s find algorithm. Combinatorics, Probability and Computing, 7(1):111–120, March 1998. CODEN CPCOFG. ISSN 0963-5483 (print), 1469-2163 (electronic). URL http://journals.

cambridge.org/action/displayIssue?jid=CPC&volumeId=7&
issueId=01.

Kaubisch:1976:QP

[KPH76] W. H. Kaubisch, R. H. Perrott, and C. A. R. Hoare. Quasiparallel programming. Software—Practice and Experience, 6(3):341–356, July/September 1976. CODEN SPEXBL. ISSN 0038-0644 (print), 1097-024X (electronic).

Kral:1966:NHP

[Krá66] Jaroslav Král. A note on Hoare proposal AB21.3. ALGOL Bulletin (Amsterdam: Mathematisch Centrum), (24):17–25, September 1966. CODEN ALGOBG. ISSN 0084-6198. See [?].

Lamport:1980:HLC

[Lam80] Leslie Lamport. The “Hoare logic” of concurrent programs. Acta Informatica, 14(1):21–37, June 1980. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic).

Lewis:1997:BCI

[Lew97] Ted Lewis. Binary critic: If Java is the answer, what was the question? Computer, 30(3):136, 133–135, March 1997. CODEN CPTRB4. ISSN 0018-9162 (print), 1558-0814 (electronic). See responses [GR97, Ols97, McR97, SL97, Wel97].

Lifschitz:1984:VPG

[Lif84] Vladimir Lifschitz. On verification of programs with GOTO statements. Information Processing Letters, 18(4):221–225, May 14, 1984. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Lenzerini:2008:PTS

[LL08] Maurizio Lenzerini and Domenico Lembo, editors. Proceedings of the Twenty-Seventh ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems: PODS’08, Vancouver, BC, Canada, June 9–11, 2008. ACM Press, New York, NY 10036, USA, 2008. ISBN 1-60560-932-3, 1-60558-108-9. LCCN QA76.9.D3.

Lloyd:1974:BRS

[Llo74] Cliff Lloyd. Book review: Structured programming, by O.-J. Dahl, E. W. Dijkstra and C. A. R. Hoare. The Computer Journal, 17(2):186, May 1974. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (electronic). URL http://www3.oup.co.uk/

computer_journal/hdb/Volume_17/Issue_02/tiff/186.tif.

Lamport:1984:HLC

[LS84] Leslie Lamport and Fred B. Schneider. The “Hoare logic” of CSP, and all that. ACM Transactions on Programming Languages and Systems, 6(2):281–296, April 1984. CODEN ATPSDT. ISSN 0164-0925 (print), 1558-4593 (electronic).

LeGuyadec:1996:SLP

[LV96] Y. Le Guyadec and B. Virot. Sequential-like proofs of data-parallel programs. Parallel Processing Letters, 6(3):415–426, September 1996. CODEN PPLTEE. ISSN 0129-6264.

Liu:2013:TPF

[LWZ13] Zhiming Liu, J. Woodcock, and Huibiao Zhu, editors. Theories of Programming and Formal Methods — Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2013. ISBN 3-642-39697-6 (print), 3-642-39698-4 (e-book). ISSN 0302-9743. LCCN QA75.5-76.95.

Mamouras:2016:HLD

[Mam16] Konstantinos Mamouras. The Hoare logic of deterministic and nondeterministic monadic recursion schemes. ACM Transactions on Computational Logic, 17(2):13:1–13:??, March 2016. CODEN ???? ISSN 1529-3785 (print), 1557-945X (electronic).

May:2021:COI

[May21] David May. CSP, occam, and Inmos. In Jones and Misra [JM21f], pages 271–284. ISBN 1-4503-8728-4. LCCN QA76.6.

McReynolds:1997:LBS

[McR97] David McReynolds. Letters: Brooks said it ten years ago. Computer, 30(5):9–10, May 1997. CODEN CPTRB4. ISSN 0018-9162 (print), 1558-0814 (electronic). Response to [Lew97].

Macnaghten:1977:FFT

[MH77] A. M. Macnaghten and C. A. R. Hoare. Fast Fourier transform free from tears. The Computer Journal, 20(1):78–83, February 1977. CODEN CMPJA6. ISSN 0010-4620 (print),

1460-2067 (electronic). URL http://comjnl.oxfordjournals.
org/content/20/1/78.full.pdf+html;   http://www3.oup.
co.uk/computer_journal/hdb/Volume_20/Issue_01/tiff/78.

tif;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
20/Issue_01/tiff/79.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_20/Issue_01/tiff/80.tif;   http://
www3.oup.co.uk/computer_journal/hdb/Volume_20/Issue_01/
tiff/81.tif;   http://www3.oup.co.uk/computer_journal/
hdb/Volume_20/Issue_01/tiff/82.tif;   http://www3.oup.
co.uk/computer_journal/hdb/Volume_20/Issue_01/tiff/83.
tif.

Morgan:1985:SSN

[MH85] C. C. Morgan and C. A. R. Hoare. Specification of a simplified network service in Z. In B. T. Denvir, W. T. Harwood, and M. I. Jackson, editors, he Analysis of Concurrent Systems, Cambridge, September 1983, Proceedings, volume 207 of Lecture Notes in Computer Science, pages 345–353. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1985.

Moller:2015:EIM

[MH15] Bernhard Möller and Tony Hoare. Exploring an interface model for CKA. In Mathematics of program construction, volume 9129 of Lecture Notes in Computer Science, pages 1–29. Springer, Cham, 2015.

Martin:1991:PAO

[MHH91] C. E. Martin, C. A. R. Hoare, and Jifeng He. Pre-adjunctions in order enriched categories. Mathematical Structures in Computer Science, 1(2):141–158, ???? 1991. ISSN 0960-1295.

Milner:1990:IOC

[Mil90] Robin Milner. Interpreting one concurrent calculus in another. Theoretical Computer Science, 75(1–2):3–13, September 25, 1990. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Misra:2021:C

[Mis21] Jayadev Misra. CV. In Jones and Misra [JM21f], pages 387–392. ISBN 1-4503-8728-4. LCCN QA76.6.

Mancini:1988:HLD

[MP88] Luigi Mancini and Giuseppe Pappalardo. Hoare logic of distributed redundant systems. Computer Systems Science and Engineering, 3(4):171–180, October 1988. CODEN CSSEEI. ISSN 0267-6192.

Manna:2010:TVE

[MP10] Zohar Manna and Doran A. Peled, editors. Time for Verification: Essays in Memory of Amir Pnueli, volume 6200 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2010. ISBN 3-642-15584-7 (paperback), 3-642-15585-5 (e-book). x + 399 pp. LCCN QA76.76.V47 T56 2010.

Makowsky:1989:WSO

[MS89] J. A. Makowsky and I. Sain. Weak second order characterizations of various program verification systems. Theoretical Computer Science, 66(3):299–321, August 26, 1989. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Mller:2021:FFY

[MS21] Peter Müller and Natarajan Shankar. The first fifteen years of the Verified Software Project. In Jones and Misra [JM21f], pages 93–124. ISBN 1-4503-8728-4. LCCN QA76.6.

Muller:2010:ALS

[Mül10] Peter Müller, editor. Advanced lectures on software engineering: LASER summer school 2007/2008. IOS Press, Amsterdam, The Netherlands, 2010. ISBN 3-642-13009-7 (paperback), 3-642-13010-0. LCCN QA76.758 .A38 2010. URL https://dl.acm.org/doi/

abs/10.5555/2167938.2167940.

Meyer:2008:VST

[MW08] Bertrand Meyer and Jim Woodcock, editors. Verified Software: Theories, Tools, Experiments: First IFIP TC 2/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10–13, 2005, Revised Selected Papers and Discussions, volume 4171 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2008. ISBN 3-540-69147-2 (paperback), 3-540-69149-9 (e-book). ISSN 0302-9743. LCCN QA76.76.V47 V78 2008eb. URL http:

//link.springer.com/openurl?genre=book\%26isbn=978-3-
540-69147-1;   http://VH7QX3XE2P.search.serialssolutions.
com/?V=1.0\%26L=VH7QX3XE2P\%26S=JCs\%26C=TC0000320630\
%26T=marc\%26tab=BOOKS.

Naumann:1995:PTH

[Nau95] David A. Naumann. Predicate transformers and higher-order programs. Theoretical Computer Science, 150(1):111–159, October 16, 1995. CODEN TCSCDI. ISSN 0304-3975 (print),

1879-2294 (electronic). URL http://www.elsevier.com/cgi-
bin/cas/tree/store/tcs/cas_sub/browse/browse.cgi?year=
1995&volume=150&issue=1&aid=1881.

Nguyen:1986:GOMa

[NH86] Van Nguyen and Brent Hailpern. A generalized object model. ACM SIGPLAN Notices, 21(10):78–87, October 1986. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Nielson:1987:HLP

[Nie87] Hanne Riis Nielson. A Hoare-like proof system for analysing the computation time of programs. Science of Computer Programming, 9(2):107–136, October 1987. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic).

Nipkow:2002:HLR

[Nip02] Tobias Nipkow. Hoare logics for recursive procedures and unbounded nondeterminism. Lecture Notes in Computer Science, 2471:103–119, 2002. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic). URL http://link.springer-ny.

com/link/service/series/0558/bibs/2471/24710103.htm;
http://link.springer-ny.com/link/service/series/0558/
papers/2471/24710103.pdf.

Nanevski:2006:PSH

[NMB06] Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Polymorphism and separation in Hoare type theory. ACM SIGPLAN Notices, 41(9):62–73, September 2006. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Nanevski:2008:HTT

[NMB08] Aleksandar Nanevski, Greg Morrisett, and Lars Birkedal. Hoare type theory, polymorphism and separation. Journal of Functional Programming, 18(5):865–911, September 2008. CO-DEN JFPRES. ISSN 0956-7968 (print), 1469-7653 (elec-

tronic). URL https://www.cambridge.org/core/product/
D6B10CE5025B4C895C2FC7438393195E.

Nanevski:2008:YDT

[NMS^{+}08] Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, and Lars Birkedal. Ynot: dependent types for imperative programs. ACM SIGPLAN Notices, 43(9):229–240, September 2008. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Naumann:2019:WSP

[NN19] David A. Naumann and Minh Ngo. Whither specifications as programs. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 39–61. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (ebook). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN

QA76.6 .U86 2019. URL http://link.springer.com/.

Neuhold:1977:UHM

[NS77] E. J. Neuhold and R. Studer. The use of Hoare’s method of program verification for the Quicksort algorithm. Computing, 18(4): 281–293, December 1977. CODEN CMPTA2. ISSN 0010-485X (print), 1436-5057 (electronic). See coments [Pri79].

Ni:2006:CAP

[NS06] Zhaozhong Ni and Zhong Shao. Certified assembly programming with embedded code pointers. ACM SIGPLAN Notices, 41(1):320– 333, January 2006. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

ODonnell:1982:CFH

[O’D82] M. J. O’Donnell. A critique of the foundations of Hoare style programming logics. Communications of the ACM, 25(12):927– 934, December 1982. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Olderog:1983:SOS

[OH83] Ernest-Rüdiger Olderog and C. A. R. Hoare. Specification-oriented semantics for communicating processes. In J. Diaz, editor, Automata, Languages and Programming — Proceedings of the 10th International Colloquium, Barcelona July 18–22, volume 154 of Lecture Notes in Computer Science, pages 561–572. Springer-Ver-lag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 1983.

Olderog:1986:SOS

[OH86] Ernst-Rüdiger R. Olderog and C. A. R. Hoare. Specificationoriented semantics for communicating processes. Acta Informatica, 23(1):9–66, March 1986. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic).

Owe:2004:OOF

[OKL04] Olaf Owe, Stein Krogdahl, and Tom Lyche, editors. From Object-Orientation to Formal Methods: Essays in Memory of Ole-Johan Dahl, volume 2635 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2004. ISBN 3-540-21366-X, 3-540-39993-3 (e-book).

LCCN QA76.758. URL http://link.springer.com/10.1007/
b96089.

Olderog:1981:SCH

[Old81] Ernst-Rüdiger Olderog. Sound and complete Hoare-like calculi based on copy rules. Acta Informatica, 16(2):161–197, October 1981. CODEN AINFA2. ISSN 0001-5903 (print), 1432-0525 (electronic).

Olderog:1983:NER

[Old83a] Ernest-Rüdiger Olderog. On the notion of expressiveness and the rule of adaptation. Theoretical Computer Science, 24(3):337–347, August 1983. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Olderog:1983:CHL

[Old83b] Ernst-Rüdiger Olderog. A characterization of Hoare’s logic for programs with Pascal-like procedures. In ACM [ACM83], pages 320–329. ISBN 0-89791-099-0. LCCN QA75.5.A14 1983. ACM order no. 508830.

Olderog:1984:CPP

[Old84] Ernest-Rüdiger Olderog. Correctness of programs with PASCALlike procedures without global variables. Theoretical Computer Science, 30(1):49–90, April 1984. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Olsen:1997:LWJ

[Ols97] Kurt Olsen. Letters: Why Java isn’t watered down C++. Computer, 30(5):9, May 1997. CODEN CPTRB4. ISSN 0018-9162 (print), 1558-0814 (electronic). Response to [Lew97]. See also [Wel97].

Pettersson:1991:LEC

[Pet91] Jimmi S. Pettersson. Letter to the editor: Comments on “Alwaystrue is not invariant”: Assertional reasoning about invariance [Inform. Process. Lett. 35(6), 15 September 1990, pp. 277–279]. Information Processing Letters, 40(5):231–233, December 13, 1991. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic). See [Ver87, VT90].

Page:1989:SME

[PJ89] I. P. Page and R. T. Jacob. The solution of mutual exclusion problems which can be described graphically. The Computer Journal, 32(1):45–54, February 1989. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (electronic). URL http:

//comjnl.oxfordjournals.org/content/32/1/45.full.pdf+
html;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
32/Issue_01/tiff/45.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_32/Issue_01/tiff/46.tif;   http://
www3.oup.co.uk/computer_journal/hdb/Volume_32/Issue_01/
tiff/47.tif;   http://www3.oup.co.uk/computer_journal/
hdb/Volume_32/Issue_01/tiff/48.tif;   http://www3.oup.
co.uk/computer_journal/hdb/Volume_32/Issue_01/tiff/49.
tif;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
32/Issue_01/tiff/50.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_32/Issue_01/tiff/51.tif;   http://
www3.oup.co.uk/computer_journal/hdb/Volume_32/Issue_01/
tiff/52.tif;   http://www3.oup.co.uk/computer_journal/
hdb/Volume_32/Issue_01/tiff/53.tif;   http://www3.oup.
co.uk/computer_journal/hdb/Volume_32/Issue_01/tiff/54.
tif.

Poskitt:2012:HSV

[PP12] Christopher M. Poskitt and Detlef Plump. Hoare-style verification of graph programs. Fundamenta Informaticae, 118(1–2):135–175, January 2012. CODEN FUMAAJ. ISSN 0169-2968 (print), 1875-8681 (electronic).

Pratt:1976:SCF

[Pra76] Vaughn R. Pratt. Semantical considerations on Floyd–Hoare logic. In IEEE [IEE76], pages 109–121. CODEN ASFPDV. ISBN ???? ISSN 0272-5428. LCCN QA75.5 .S97 1976.

URL https://ieeexplore.ieee.org/xpl/conhome/4567877/
proceeding?isnumber=4567878. IEEE catalog number CH1133-8

C.

PeytonJones:1999:SIE

[PRH^{+}99] Simon Peyton Jones, Alastair Reid, Tony Hoare, Simon Marlow, and Fergus Henderson. A semantics for imprecise exceptions. ACM SIGPLAN Notices, 34(5):25–36, May 1999. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160

(electronic). URL http://www.acm.org:80/pubs/citations/
proceedings/pldi/301122/p25-peyton_jones/.

Pritchard:1979:CPJ

[Pri79] P. Pritchard. Comments on a paper by E. J. Neuhold and R. Studer: “The use of Hoare’s method of program verification for the quick-sort algorithm” [Computing 18 (1977), no. 4, 281–293; MR 56 #13753]. Computing, 22(3):279–282, September 1979. CODEN CMPTA2. ISSN 0010-485X (print), 1436-5057 (electronic). See [NS77].

Prodinger:1995:MQH

[Pro95] Helmut Prodinger. Multiple Quickselect — Hoare’s Find algorithm for several elements. Information Processing Letters, 56(3): 123–129, November 10, 1995. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Qian:1990:ASD

[Qia90] Xiaolei Qian. An axiom system for database transactions. Information Processing Letters, 36(4):183–189, November 15, 1990. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Rehof:2010:ADS

[RAR^{+}10] Niels Jakob Rehof, Anthony D. Andrews, Sriram K. Rajamani, Charles Antony Richard Hoare, and Cédric Fournet. Analysis of distributed software systems via specification substitution. US Patent number 7,797,669., September 14, 2010. URL https://

patents.google.com/patent/US7797669. Patent filed 13 Febru-

ary 2004.

Roscoe:1986:LOP

[RH86] A. W. Roscoe and C. A. R. Hoare. Laws of occam programming. Technical Monograph PRG-53, Oxford University Computing Laboratory, Programming Research Group, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, February 1986.

Roscoe:1988:LOP

[RH88] A. W. Roscoe and C. A. R. Hoare. The laws of occam programming. Theoretical Computer Science, 60(2):177–229, September 1988. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Ridge:2009:VDS

[Rid09] Thomas Ridge. Verifying distributed systems: the operational approach. ACM SIGPLAN Notices, 44(1):429–440, January 2009. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Rishe:1990:PIC

[RNT90] Naphtali Rishe, Sham Navathe, and Doren Tal, editors. PARBASE-90: International conference on databases, parallel architectures, and their applications, March 7–9, 1990, Miami Beach, Florida: proceedings. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 1990. ISBN 0-8186-2035-8 (hardcover), 0-8186-6035-X (microfiche). LCCN QA76.9.D3 P3473 199.

RodriguezArtalejo:1985:SQA

[Rod85] M. Rodriguez Artalejo. Some questions about expressiveness and relative completeness in Hoare’s logic. Theoretical Computer Science, 39(2–3):189–206, August 1985. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Roscoe:1994:CME

[Ros94] A. W. Roscoe, editor. A Classical Mind, essays in honour of C. A. R. Hoare. Prentice-Hall, Upper Saddle River, NJ 07458, USA, 1994. ISBN 0-13-294844-3. xii + 451 pp. LCCN QA76.C484 1994.

Reus:2001:HCV

[RWH01] Bernhard Reus, Martin Wirsing, and Rolf Hennicker. A Hoare calculus for verifying Java realizations of OCL-constrained design models. Lecture Notes in Computer Science, 2029:300– ??, 2001. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-

3349 (electronic). URL http://link.springer-ny.com/link/
service/series/0558/bibs/2029/20290300.htm;   http://
link.springer-ny.com/link/service/series/0558/papers/
2029/20290300.pdf.

Ryder:1999:PAS

[Ryd99] Barbara G. Ryder, editor. Proceedings of the ACM SIGPLAN ’99 Conference on Programming Language Design and Implementation (PLDI ’99), Atlanta, Georgia, 2–4 May 1999, volume 34(5) of ACM SIGPLAN Notices. ACM Press, New York, NY 10036, USA, 1999. ISBN 1-58113-094-5 (paperback), 1-58113-094-5 (ebook). LCCN QA76.7 .A35 1999. URL https://dl.acm.org/

doi/proceedings/10.1145/301618.

Simauti:1967:CCD

[S^{+}67] T. Simauti et al. Comments on “A contribution to the development of ALGOL” (Wirth and Hoare). ALGOL Bulletin (Amsterdam: Mathematisch Centrum), (26):23–27, August 1967.

Santini:2005:WSI

[San05] Simone Santini. We are sorry to inform you . . .. Computer, 38(12): 128, 126–127, December 2005. CODEN CPTRB4. ISSN 0018-9162 (print), 1558-0814 (electronic).

Sousa:2016:CHL

[SD16] Marcelo Sousa and Isil Dillig. Cartesian Hoare logic for verifying k-safety properties. ACM SIGPLAN Notices, 51(6):57–69, June 2016. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Sridhar:1985:JEC

[SH85] K. T. Sridhar and C. A. R. Hoare. JSD expressed in CSP. Technical monograph PRG-51, Oxford University Computing Laboratory, Programming Research Group, Wolfson Building, Parks Road, Oxford, OX1 3QD, UK, 1985. 40 pp.

Shankar:1993:IAR

[Sha93] A. Udaya Shankar. An introduction to assertional reasoning for concurrent systems. ACM Computing Surveys, 25(3):225–262, September 1993. CODEN CMSVAN. ISSN 0360-0300 (print),

1557-7341 (electronic). URL http://www.acm.org/pubs/toc/
Abstracts/0360-0300/158441.html.

Shapiro:2006:PPC

[Sha06] Marc Shapiro. Practical proofs of concurrent programs. ACM SIG-PLAN Notices, 41(9):123, September 2006. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Shustek:2009:IIC

[Shu09] Len Shustek. Interview: an interview with C. A. R. Hoare. Communications of the ACM, 52(3):38–41, March 2009. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic).

Silberschatz:1981:PDC

[Sil81] A. Silberschatz. Port directed communication. The Computer Journal, 24(1):78–82, February 1981. CODEN CMPJA6. ISSN 0010-4620 (print), 1460-2067 (electronic). URL http:

//comjnl.oxfordjournals.org/content/24/1/78.full.pdf+
html;   http://www3.oup.co.uk/computer_journal/hdb/Volume_
24/Issue_01/tiff/78.tif;   http://www3.oup.co.uk/computer_
journal/hdb/Volume_24/Issue_01/tiff/79.tif;   http://
www3.oup.co.uk/computer_journal/hdb/Volume_24/Issue_01/
tiff/80.tif;   http://www3.oup.co.uk/computer_journal/
hdb/Volume_24/Issue_01/tiff/81.tif;   http://www3.oup.
co.uk/computer_journal/hdb/Volume_24/Issue_01/tiff/82.
tif.

Struble:1997:LDJ

[SL97] Craig A. Struble and Ted Lewis. Letters: Deadlocks, and Java. Computer, 30(5):10, May 1997. CODEN CPTRB4. ISSN 0018-9162 (print), 1558-0814 (electronic). Response to [Lew97].

Shaner:2007:MVH

[SLN07] Steve M. Shaner, Gary T. Leavens, and David A. Naumann. Modular verification of higher-order methods with mandatory calls specified by model programs. ACM SIGPLAN Notices, 42(10): 351–368, October 2007. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Sergey:2016:HSS

[SNBD16] Ilya Sergey, Aleksandar Nanevski, Anindya Banerjee, and Germán Andrés Delbianco. Hoare-style specifications as correctness conditions for non-linearizable concurrent objects. ACM SIG-PLAN Notices, 51(10):92–110, October 2016. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Sokolowski:1987:SHL

[Sok87] Stefan Sokołowski. Soundness of Hoare’s logic: an automated proof using LCF. ACM Transactions on Programming Languages and Systems, 9(1):100–120, January 1987. CODEN ATPSDT. ISSN 0164-0925 (print), 1558-4593 (electronic). URL http://www.acm.

org/pubs/toc/Abstracts/0164-0925/11326.html.

Spivey:1989:ZNR

[Spi89] J. M. Spivey. The Z notation: a reference manual. Prentice-Hall International series in computer science. Prentice-Hall, Upper Saddle River, NJ 07458, USA, 1989. ISBN 0-13-983768-X (paperback). xi + 155 pp. LCCN QA76.73.Z2 S66 1989. Based on work by Jean-Raymond Abrial.

Stoller:1995:VPU

[SS95] Scott D. Stoller and Fred B. Schneider. Verifying programs that use causally-ordered message-passing. Science of Computer Programming, 24(2):105–128, April 1995. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic).

Seres:1999:ALP

[SSH99] Silvija Seres, Michael Spivey, and Tony Hoare. Algebra of logic programming. In Proceedings of the 1999 international conference on Logic programming, November 1999 (Las Cruces, NM), MIT Press Ser. Logic Program., pages 184–199. MIT Press, Cam-

bridge, MA, USA, 1999. URL https://dl.acm.org/doi/10.
5555/341176.341200.

Stirling:1988:GOG

[Sti88] Colin Stirling. A generalization of Owicki–Gries’s Hoare logic for a concurrent while language. Theoretical Computer Science, 58 (1–3):347–359, June 1988. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Struth:2021:THA

[Str21] Georg Struth. Trimming the hedges: an algebra to tame concurrency. In Jones and Misra [JM21f], pages 317–346. ISBN 1-4503-8728-4. LCCN QA76.6.

Saabas:2007:CNS

[SU07] Ando Saabas and Tarmo Uustalu. A compositional natural semantics and Hoare logic for low-level languages. Theoretical Computer Science, 373(3):273–302, April 5, 2007. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Sufrin:2021:TBO

[Suf21] Bernard Sufrin. Teaching at Belfast and Oxford. In Jones and Misra [JM21f], pages 223–250. ISBN 1-4503-8728-4. LCCN QA76.6.

Sun:1996:TRH

[Sun96] Yong Sun. Term rewriting and Hoare logic — Coded rewriting. Information Processing Letters, 60(5):237–242, December 8, 1996. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Szczepanska:1991:HLV

[Szc91] D. Szczepanska. A Hoare-like verification system for a language with an exception handling mechanism. Theoretical Computer Science, 80(2):319–335, March 29, 1991. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Takaoka:1987:DRH

[Tak87] Tadao Takaoka. A decomposition rule for the Hoare logic. Information Processing Letters, 26(4):205–208, December 4, 1987. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Turon:2013:URH

[TDB13] Aaron Turon, Derek Dreyer, and Lars Birkedal. Unifying refinement and Hoare-style reasoning in a logic for higher-order concurrency. ACM SIGPLAN Notices, 48(9):377–390, September 2013. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Thielecke:2006:FRA

[Thi06] Hayo Thielecke. Frame rules from answer types for code pointers. ACM SIGPLAN Notices, 41(1):309–319, January 2006. CODEN SINODQ. ISSN 0362-1340 (print), 1523-2867 (print), 1558-1160 (electronic).

Tennent:1991:CPW

[TT91] R. D. Tennent and J. K. Tobin. Continuations in possible-world semantics. Theoretical Computer Science, 85(2):283–303, August 12, 1991. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

vanAmmers:1998:PCC

[vA98] Eric W. van Ammers. Program construction by context independent refinements. Science of Computer Programming, 30(3): 251–286, March 2, 1998. CODEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic). URL http://www.elsevier.com/

cas/tree/store/scico/sub/1998/30/3/527.pdf.

vanDiepen:1986:PDT

[vd86] N. W. P. van Diepen and W. P. de Roever. Program derivation through transformations: the evolution of list-copying algorithms. Science of Computer Programming, 6(3):213–272, May 1986. CO-DEN SCPGD4. ISSN 0167-6423 (print), 1872-7964 (electronic).

Verjus:1987:PDA

[Ver87] J. Pierre Verjus. On the proof of a distributed algorithm. Information Processing Letters, 25(3):145–147, May 29, 1987. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic). See comments [VT90, Pet91].

vonHenke:1985:RHS

[vH85] Friedrich W. von Henke. Reasoning with Hoare sentences. ACM SIGSOFT Software Engineering Notes, 10(4):84, August 1985. CODEN SFENDP. ISSN 0163-5948 (print), 1943-5843 (electronic).

Vafeiadis:2006:PCH

[VHHS06] Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro. Proving correctness of highly-concurrent linearisable objects. In Proceedings of the eleventh ACM SIGPLAN symposium on Principles and practice of parallel programming — PPoPP ’06, pages 129–136. ACM Press, New York, NY 10036, USA, 2006.

vonKarger:1995:SC

[vKH95] Burghard von Karger and C. A. R. Hoare. Sequential calculus. Information Processing Letters, 53(3):123–130, February 10, 1995. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

vonOheimb:2001:HLJ

[vO01] David von Oheimb. Hoare logic for Java in Isabelle/HOL. Concurrency and Computation: Practice and Experience, 13 (13):1173–1214, November 2001. CODEN CCPEBO. ISSN 1532-0626 (print), 1532-0634 (electronic). URL http://

www3.interscience.wiley.com/cgi-bin/abstract/88011338/
START;   http://www3.interscience.wiley.com/cgi-bin/fulltext?
ID=88011338&PLACEBO=IE.pdf.

vonOheimb:2002:HLN

[vON02] David von Oheimb and Tobias Nipkow. Hoare logic for NanoJava: Auxiliary variables, side effects, and virtual methods revisited.

Lecture Notes in Computer Science, 2391:89–??, 2002. CODEN LNCSD9. ISSN 0302-9743 (print), 1611-3349 (electronic). URL

http://link.springer-ny.com/link/service/series/0558/
bibs/2391/23910089.htm;   http://link.springer-ny.com/
link/service/series/0558/papers/2391/23910089.pdf.

vanStaden:2013:AUO

[vSH13] Stephan van Staden and Tony Hoare. Algebra unifies operational calculi. In Wolff et al. [WGF13], pages 88–104. ISBN 3-642-35704-0 (paperback), 3-642-35705-9 (e-book). LCCN QA76.6 .U87 2012.

VanGasteren:1990:CPD

[VT90] A. J. M. Van Gasteren and G. Tel. Comments on “On the proof of a distributed algorithm”: always-true is not invariant [Inform. Process. Lett. 25(3), 29 May 1987, pp. 145–147]. Information Processing Letters, 35(6):277–279, September 15, 1990. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic). See [Ver87, Pet91].

Wand:1976:NIR

[Wan76] Mitchell Wand. A new incompleteness result for Hoare’s system. In ACM [ACM76], pages 87–91. ISBN 1-4503-7414-X. LCCN QA 76.6

A12 1976. URL http://dl.acm.org/citation.cfm?id=800113.

Wand:1978:NIR

[Wan78] Mitchell Wand. A new incompleteness result for Hoare’s system. Journal of the ACM, 25(1):168–175, January 1978. CODEN JA-COAH. ISSN 0004-5411 (print), 1557-735X (electronic).

Woodcock:2021:VGC

[WBC^{+}21] Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, and Thomas Santen. Verification in the Grand Challenge. In Jones and Misra [JM21f], pages 125–156. ISBN 1-4503-8728-4. LCCN QA76.6.

Woodcock:2019:PSR

[WCF^{+}19] Jim Woodcock, Ana Cavalcanti, Simon Foster, Alexandre Mota, and Kangfeng Ye. Probabilistic semantics for RoboChart. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 80– 105. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.6

.U86 2019. URL http://link.springer.com/.

Weiss:1988:BOP

[Wei88] Eric A. Weiss. Biographies: Oh, pioneers! Annals of the History of Computing, 10(4):348–361, October/December 1988. CODEN

AHCOE5. ISSN 0164-1239. URL http://dlib.computer.org/
an/books/an1988/pdf/a4348.pdf;   http://www.computer.
org/annals/an1988/a4348abs.htm.

Welch:1997:LEI

[Wel97] Peter Welch. Letters to the editor: Ignore the monitor methods! Computer, 30(7):7, 9, July 1997. CODEN CPTRB4. ISSN 0018-9162 (print), 1558-0814 (electronic). Comments on [Lew97], and raises concerns about the inadequacy of the Java threads model,

and points to http://www.cs.bris.ac.uk/~alan/javappp.html

as a source for Java classes implementing C. A. R. Hoare’s Communicating Sequential Processes. See also [Ols97].

Wolff:2013:UTP

[WGF13] Burkhart Wolff, Marie-Claude Gaudel, and Abderrahmane Feliachi, editors. Unifying Theories of Programming: 4th International Symposium, UTP 2012, Paris, France, August 27–28, 2012, Revised Selected Papers, volume 7681 of Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany / Heidelberg, Germany / London, UK / etc., 2013. ISBN 3-642-35704-0 (paperback), 3-642-35705-9 (e-book). LCCN QA76.6 .U87 2012.

Wirth:1965:CDA

[WH65] Niklaus Wirth and C. A. R. Hoare. A contribution to the development of ALGOL. Report 35, Stanford University, Department of Computer Science, Stanford, CA, USA, December 1965. Revised February 1966. Published in [WH66a].

Wirth:1966:CDA

[WH66a] Niklaus Wirth and C. A. R. Hoare. A contribution to the development of ALGOL. Communications of the ACM, 9(6):413–432, June 1966. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). See errata [WH66b].

Wirth:1966:ECD

[WH66b] Niklaus Wirth and C. A. R. Hoare. Errata: “A Contribution to the Development of ALGOL”. Communications of the ACM, 9 (12):878, December 1966. CODEN CACMA2. ISSN 0001-0782 (print), 1557-7317 (electronic). See [WH66a].

Wehrman:2009:GMS

[WHO09] Ian Wehrman, C. A. R. Hoare, and Peter W. O’Hearn. Graphical models of separation logic. Information Processing Letters, 109 (17):1001–1004, August 16, 2009. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Winskel:1985:PM

[Win85] G. Winskel. On powerdomains and modality. Theoretical Computer Science, 36(1):127–137, March 1985. CODEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

Wing:1989:VAD

[Win89] Jeannette M. Wing. Verifying atomic data types. International Journal of Parallel Programming, 18(5):315–357, October 1989. CODEN IJPPE5. ISSN 0885-7458 (print), 1573-7640 (elec-

tronic). URL http://www.springerlink.com/openurl.asp?
genre=article&issn=0885-7458&volume=18&issue=5&spage=
315.

Woodcock:2021:HHU

[Woo21] Jim Woodcock. Hoare and He’s unifying theories of programming. In Jones and Misra [JM21f], pages 285–316. ISBN 1-4503-8728-4. LCCN QA76.6.

Welsh:1977:AIP

[WSH77] J. Welsh, W. J. Sneeringer, and C. A. R. Hoare. Ambiguities and insecurities in Pascal. Software—Practice and Experience, 7 (6):685–696, November/December 1977. CODEN SPEXBL. ISSN 0038-0644 (print), 1097-024X (electronic). See also [Ker81, Ker84].

Woodger:1969:MRA

[WTD^{+}69] Mike Woodger, Władisław Marek Turski, Edsger W. Dijkstra, C. A. R. Hoare, Brian Randell, Jan V. Garwick, Fraser G. Duncan, and Gerhard Seegmueller. Minority report on Algol 68. The draft and the final text. ALGOL Bulletin (Amsterdam: Mathematisch Centrum), ??(??):??, January 17, 1969. URL http://ershov.

iis.nsk.su/en/node/805785.

Wu:2019:USC

[WZX19] Xi Wu, Huibiao Zhu, and Wanling Xie. UTP semantics of a calculus for mobile ad hoc networks. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 198–216. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.6 .U86 2019. URL http://link.

springer.com/.

Xu:2016:CHL

[XSZ16] Zhaowei Xu, Yuefei Sui, and Wenhui Zhang. Completeness of Hoare logic with inputs over the standard model. Theoretical Computer Science, 612(??):23–28, January 25, 2016. CO-DEN TCSCDI. ISSN 0304-3975 (print), 1879-2294 (electronic).

URL http://www.sciencedirect.com/science/article/pii/
S0304397515007239.

Ying:2011:FHL

[Yin11] Mingsheng Ying. Floyd–Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems, 33(6): 19:1–19:49, December 2011. CODEN ATPSDT. ISSN 0164-0925 (print), 1558-4593 (electronic).

Zhou:1981:PCC

[ZH81] Chaochen Zhou and C. A. R. Hoare. Partial correctness of communicating sequential processes. In ????, editor, Proceedings of 2nd International Conference on Distributed Computing Systems, pages 1–12. IEEE Computer Society Press, 1109 Spring Street, Suite 300, Silver Spring, MD 20910, USA, 1981.

Zhou:1992:MSS

[ZH92] Chaochen Zhou and C. A. R. Hoare. A model for synchronous switching circuits and its theory of correctness. Formal Methods in System Design, 1(1):7–28, July 1992. CODEN FMSDE6. ISSN 0925-9856 (print), 1572-8102 (electronic).

Zhou:1991:CD

[ZHR91] Chaochen Zhou, C. A. R. Hoare, and Anders P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, December 13, 1991. CODEN IFPLAT. ISSN 0020-0190 (print), 1872-6119 (electronic).

Zhan:2019:UGC

[ZLW^{+}19] Haolan Zhan, Qianqian Lin, Shuling Wang, Jean-Pierre Talpin, Xiong Xu, and Naijun Zhan. Unified graphical co-modelling of cyber-physical systems using AADL and Simulink/Stateflow. In de Oliveira Salazar) Ribeiro and Sampaio [dOSRS19], pages 109– 129. ISBN 3-030-31037-X (paperback), 3-030-31038-8 (e-book). ISSN 0302-9743 (print), 1611-3349 (electronic). LCCN QA76.6

.U86 2019. URL http://link.springer.com/.