%%======================================================================
%% WARNING: Do NOT edit this file.  It was produced automatically
%% with the UNIX pipeline
%%
%%       biblex xxx.bib | \
%%         gawk -f keywords.awk | \
%%         egrep 'entrytype$' | \
%%         gawk -f fmtwords.awk >xxx.xwx
%%
%% by beebe@gamma.math.utah.edu on Tue Oct  1 09:46:54 MDT 2024
%%======================================================================

\ifx \NAMECITE \undefined % User can override this definition 
    \def \NAMECITE #1#2{{\bf #1} \cite{#2}}
\fi



\NAMECITE{\#13753}{%
		Pritchard:1979:CPJ%
		}.


\NAMECITE{$^*$}{%
		Damm:1983:SRH%
		}.
\NAMECITE{$i$}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA%
		}.
\NAMECITE{$k$}{%
		Sousa:2016:CHL%
		}.
\NAMECITE{$n$}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA%
		}.


\NAMECITE{-safety}{%
		Sousa:2016:CHL%
		}.
\NAMECITE{-th}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA%
		}.


\NAMECITE{{0}}{%
		Horning:1989:BRE%
		}.
\NAMECITE{{0-13-284027-8}}{%
		Horning:1989:BRE%
		}.


\NAMECITE{{10}}{%
		Hoare:1971:CSI%
		}.
\NAMECITE{11th}{%
		Kapur:1992:ADC,%
		Berghammer:2009:RKA,%
		Gibbons:2012:MPC%
		}.
\NAMECITE{{14th}}{%
		Hofner:2014:RAM%
		}.
\NAMECITE{16th}{%
		Abadi:2005:CCT%
		}.
\NAMECITE{17th}{%
		IEEE:1976:ASF,%
		Hoare:1986:MPI%
		}.
\NAMECITE{{18}}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{{1971}}{%
		Hoare:1971:CSI,%
		Hoare:1972:OST%
		}.
\NAMECITE{{1980}}{%
		Hoare:2016:PST,%
		Hoare:2021:ATA%
		}.
\NAMECITE{{1983}}{%
		ACM:1983:PFA%
		}.
\NAMECITE{{1985}}{%
		Hoare:1986:MPI%
		}.
\NAMECITE{{1991}}{%
		Gordon:1992:MRH%
		}.
\NAMECITE{{1994}}{%
		Broy:1996:DPD%
		}.
\NAMECITE{{1999}}{%
		Ryder:1999:PAS%
		}.


\NAMECITE{{2.1}}{%
		Hoare:1966:LWM%
		}.
\NAMECITE{{2.15s}}{%
		Hoare:1970:BRC%
		}.
\NAMECITE{2/WG}{%
		Meyer:2008:VST%
		}.
\NAMECITE{{2000}}{%
		Hoare:2001:ETS,%
		IEEE:2000:PSA%
		}.
\NAMECITE{{2003}}{%
		Hoare:2004:RMN%
		}.
\NAMECITE{{2007}}{%
		Muller:2010:ALS%
		}.
\NAMECITE{{2007/2008}}{%
		Muller:2010:ALS%
		}.
\NAMECITE{{2008}}{%
		Lenzerini:2008:PTS,%
		Muller:2010:ALS%
		}.
\NAMECITE{{2011}}{%
		Hoare:2012:MT,%
		Hoare:2012:MTR%
		}.
\NAMECITE{{2013}}{%
		Jones:2013:ICC%
		}.
\NAMECITE{{20th}}{%
		Cipra:2000:BCE%
		}.
\NAMECITE{{25}}{%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{{26th}}{%
		IEEE:2002:AIC%
		}.
\NAMECITE{28/29}{%
		Broy:2001:PTC%
		}.


\NAMECITE{{30}}{%
		Hoare:1987:CLP%
		}.
\NAMECITE{33rd}{%
		Haddad:2012:ATP%
		}.
\NAMECITE{{35}}{%
		Pettersson:1991:LEC%
		}.
\NAMECITE{{3rd}}{%
		IEEE:1988:ASL%
		}.


\NAMECITE{{4.20}}{%
		Barron:1975:BRS%
		}.
\NAMECITE{{489}}{%
		Floyd:1975:AAA%
		}.
\NAMECITE{{4th}}{%
		Wolff:2013:UTP%
		}.


\NAMECITE{{56}}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{5th}{%
		Bottaci:2010:TAI%
		}.


\NAMECITE{{60}}{%
		Hoare:1966:PSA%
		}.
\NAMECITE{{63}}{%
		Hoare:1961:AP%
		}.
\NAMECITE{{64}}{%
		Hoare:1961:AQ%
		}.
\NAMECITE{{65}}{%
		Hoare:1961:AF%
		}.
\NAMECITE{{68}}{%
		Hoare:1968:CA,%
		Hoare:1968:RDR,%
		Woodger:1969:MRA%
		}.
\NAMECITE{6th}{%
		Berghammer:2009:RKA%
		}.


\NAMECITE{70th}{%
		Liu:2013:TPF%
		}.
\NAMECITE{75th}{%
		Jones:2011:DHC%
		}.
\NAMECITE{'76}{%
		ACM:1976:SPE%
		}.
\NAMECITE{7th}{%
		Ribeiro:2019:UTP%
		}.


\NAMECITE{{8}}{%
		Horning:1989:BRE%
		}.
\NAMECITE{85th}{%
		Ribeiro:2019:UTP%
		}.


\NAMECITE{'90}{%
		Bjorner:1990:VVZ,%
		Baeten:1990:CTC,%
		Rishe:1990:PIC%
		}.
\NAMECITE{'99}{%
		Ryder:1999:PAS%
		}.


\NAMECITE{{A.}}{%
		Hoare:1968:LVW%
		}.
\NAMECITE{{AADL}}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{{AB21.3}}{%
		Kral:1966:NHP%
		}.
\NAMECITE{Abrupt}{%
		Huisman:2000:JPV%
		}.
\NAMECITE{Abstraction}{%
		Banerjee:2022:RPL%
		}.
\NAMECITE{Abstractions}{%
		Jones:2021:FEA%
		}.
\NAMECITE{Academic}{%
		Barron:1975:BRS,%
		Bottaci:2010:TAI%
		}.
\NAMECITE{Acceptance}{%
		Enslow:1975:ILRa%
		}.
\NAMECITE{Achievement}{%
		Hoare:2012:MT,%
		Black:2012:PSD,%
		Hoare:2012:MTR%
		}.
\NAMECITE{ACM}{%
		ACM:1983:PFA,%
		Hoare:1987:CLP,%
		Hoare:2012:MT,%
		Hoare:2012:MTR,%
		Hoare:2016:PST,%
		Hoare:2021:ATA,%
		Lenzerini:2008:PTS,%
		Ryder:1999:PAS,%
		Ashenhurst:1987:ATA,%
		Floyd:1975:AAA,%
		Jones:2021:AI%
		}.
\NAMECITE{Act}{%
		Hoare:2000:HAF%
		}.
\NAMECITE{Ad}{%
		Wu:2019:USC%
		}.
\NAMECITE{{Ada}}{%
		Feuer:1984:CAP%
		}.
\NAMECITE{adaptation}{%
		Olderog:1983:NER%
		}.
\NAMECITE{add}{%
		Hoare:1986:MAS%
		}.
\NAMECITE{Addenda}{%
		Hoare:1974:ACA%
		}.
\NAMECITE{Address}{%
		Hoare:1990:RAPb,%
		Hoare:1991:TCC,%
		Hoare:1978:SEK,%
		Hoare:1990:LMM,%
		Hoare:1997:UTC%
		}.
\NAMECITE{addressing}{%
		Hoare:1965:NIA%
		}.
\NAMECITE{adjunctions}{%
		Martin:1991:PAO%
		}.
\NAMECITE{Advanced}{%
		Broy:1996:DPD,%
		Muller:2010:ALS%
		}.
\NAMECITE{Afternoon}{%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{Ago}{%
		McReynolds:1997:LBS%
		}.
\NAMECITE{Aided}{%
		Barthe:2012:PRH%
		}.
\NAMECITE{AKA}{%
		Berghammer:2009:RKA%
		}.
\NAMECITE{Algebra}{%
		Brookes:2021:CPP,%
		Hayes:2019:DAR,%
		Hoare:1992:AM,%
		Hoare:1993:AMa,%
		Hoare:1993:AMb,%
		Hoare:1995:AM,%
		Hoare:1996:AM,%
		Hoare:2005:PAUa,%
		Hoare:2005:PAUb,%
		Hoare:2019:CST,%
		Seres:1999:ALP,%
		Struth:2021:THA,%
		vanStaden:2013:AUO,%
		Berghammer:2009:RKA,%
		Groote:1994:PAG,%
		He:1993:AOS,%
		Hoare:1990:RAPa,%
		Hoare:1990:RAPb,%
		Hoare:1992:RAP,%
		Hoare:2009:CKA,%
		Hoare:2009:FCK,%
		Hoare:2011:CKA,%
		Hoare:2012:PA,%
		Hoare:2014:DCK,%
		Hoare:2016:DCK,%
		Hoare:2019:CSTa,%
		Kozen:2000:HLK%
		}.
\NAMECITE{Algebraic}{%
		Aichernig:2019:TPA,%
		Gardiner:1995:APC,%
		He:1987:ASP,%
		Hoare:1986:ASP,%
		Hoare:1987:ASP,%
		Hoare:1991:ASP,%
		Hoare:1994:ACO,%
		Hoare:1997:ADO,%
		Hoare:2000:ADO,%
		Hofner:2014:RAM,%
		Delbianco:2013:HSR,%
		Gritzner:1996:RAM,%
		Hoare:1990:AAV%
		}.
\NAMECITE{Algebras}{%
		Broy:2003:MAL,%
		Butterfield:2019:IOA%
		}.
\NAMECITE{ALGOL}{%
		Wirth:1966:ECD,%
		Hoare:1962:REA,%
		Hoare:1963:EAI,%
		Hoare:1964:EAP,%
		Hoare:1966:PSA,%
		Hoare:1968:CA,%
		Hoare:1968:RDR,%
		Simauti:1967:CCD,%
		Wirth:1965:CDA,%
		Wirth:1966:CDA,%
		Woodger:1969:MRA,%
		Hoare:1964:BRA%
		}.
\NAMECITE{Algorithm}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA,%
		Grubel:1996:ADT,%
		Grubel:1998:HSA,%
		Kirschenhofer:1998:CHF,%
		He:1987:ASP,%
		Neuhold:1977:UHM,%
		Pritchard:1979:CPJ,%
		Prodinger:1995:MQH,%
		VanGasteren:1990:CPD,%
		Verjus:1987:PDA,%
		Brown:1976:RAA,%
		Hoare:1961:AF,%
		Hoare:1961:AP,%
		Hoare:1961:AQ%
		}.
\NAMECITE{Algorithms}{%
		Cipra:2000:BCE,%
		vanDiepen:1986:PDT,%
		denHartog:2008:TMC%
		}.
\NAMECITE{Always}{%
		Pettersson:1991:LEC,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{Always-true}{%
		Pettersson:1991:LEC,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{Ambiguities}{%
		Welsh:1977:AIP%
		}.
\NAMECITE{{Amir}}{%
		Manna:2010:TVE%
		}.
\NAMECITE{amp}{%
		Hoare:2004:AA%
		}.
\NAMECITE{analysing}{%
		Nielson:1987:HLP%
		}.
\NAMECITE{Analysis}{%
		Fouz:2012:SAQ,%
		Hoare:1961:MSS,%
		Rehof:2010:ADS%
		}.
\NAMECITE{Annual}{%
		IEEE:1988:ASL,%
		IEEE:2002:AIC,%
		ACM:1976:SPE,%
		ACM:1983:PFA,%
		IEEE:1976:ASF%
		}.
\NAMECITE{Answer}{%
		Lewis:1997:BCI,%
		Thielecke:2006:FRA%
		}.
\NAMECITE{Antony}{%
		Black:2012:PSD,%
		Davies:2000:MPC,%
		Dijkstra:1999:FWT,%
		Frana:2002:ICA%
		}.
\NAMECITE{application}{%
		Hoare:1976:CST,%
		Haddad:2012:ATP%
		}.
\NAMECITE{Applications}{%
		Berghammer:2009:RKA,%
		Elliott:1989:SAM,%
		Herbert:2004:CST,%
		IEEE:2002:AIC,%
		Hoare:2010:MJD,%
		Rishe:1990:PIC%
		}.
\NAMECITE{applied}{%
		Hoare:1988:PCC%
		}.
\NAMECITE{Approach}{%
		Grubel:1998:HSA,%
		Hoare:1989:NAC,%
		Hoare:1993:NFA,%
		Hoare:2005:PAUa,%
		Hoare:2005:PAUb,%
		Hoare:1971:PPA,%
		Hoare:1975:PPA,%
		Hoare:1976:PPA,%
		Hoare:1990:AAV,%
		Hortala-Gonzalez:1989:HLN,%
		Ridge:2009:VDS%
		}.
\NAMECITE{approaches}{%
		Bruni:2005:CTA%
		}.
\NAMECITE{April}{%
		ACM:1983:PFA,%
		Bjorner:1990:VVZ,%
		Hofner:2014:RAM%
		}.
\NAMECITE{APSEC}{%
		IEEE:2000:PSA%
		}.
\NAMECITE{architectures}{%
		Rishe:1990:PIC%
		}.
\NAMECITE{arithmetic}{%
		Bergstra:1983:HLP%
		}.
\NAMECITE{Art}{%
		Bates:1976:SPI%
		}.
\NAMECITE{Asia}{%
		IEEE:2000:PSA%
		}.
\NAMECITE{Asia-Pacific}{%
		IEEE:2000:PSA%
		}.
\NAMECITE{assembly}{%
		Ni:2006:CAP%
		}.
\NAMECITE{assertion}{%
		Chisholm:1989:ARP%
		}.
\NAMECITE{Assertional}{%
		Pettersson:1991:LEC,%
		Shankar:1993:IAR%
		}.
\NAMECITE{Assertions}{%
		Hoare:2000:A,%
		Hoare:2002:AMS,%
		Hoare:2002:APP,%
		Hoare:2002:APS,%
		Hoare:2002:APV,%
		Hoare:2003:A,%
		Hoare:2003:APP%
		}.
\NAMECITE{Assessing}{%
		Apt:2021:ASI,%
		Feuer:1984:CAP%
		}.
\NAMECITE{associated}{%
		Chisholm:1989:ARP%
		}.
\NAMECITE{Asymptotic}{%
		Grubel:1996:ADT%
		}.
\NAMECITE{asynchronous}{%
		Josephs:1989:TAP%
		}.
\NAMECITE{asynchronously}{%
		deBoer:2002:HLD%
		}.
\NAMECITE{asynchrony}{%
		He:1990:TSA%
		}.
\NAMECITE{Atlanta}{%
		Ryder:1999:PAS%
		}.
\NAMECITE{atom}{%
		Hoare:2004:AA%
		}.
\NAMECITE{atomic}{%
		Wing:1989:VAD%
		}.
\NAMECITE{Aug}{%
		Ershov:1974:IST%
		}.
\NAMECITE{August}{%
		Abadi:2005:CCT,%
		Bauer:1976:LHI,%
		Broy:1996:DPD,%
		Hoare:1972:OST,%
		Hoare:2001:ETS,%
		IEEE:2002:AIC,%
		Wolff:2013:UTP,%
		Dijkstra:1970:LPC%
		}.
\NAMECITE{Author}{%
		Jones:2021:ABI%
		}.
\NAMECITE{authorization}{%
		Becker:2010:LSM%
		}.
\NAMECITE{Automated}{%
		Boyer:1992:ACP,%
		Boyer:1996:APO,%
		Kapur:1992:ADC,%
		Sokolowski:1987:SHL,%
		Chisholm:1989:ARP,%
		Kapur:1992:ADC%
		}.
\NAMECITE{automorphisms}{%
		Hoare:1979:CGW%
		}.
\NAMECITE{Auxiliary}{%
		Kleymann:1999:HLA,%
		vonOheimb:2002:HLN%
		}.
\NAMECITE{Award}{%
		Ashenhurst:1987:ATA,%
		Hoare:2016:PST,%
		Hoare:2021:ATA,%
		Black:2012:PSD,%
		Hoare:2012:MTR,%
		Hoare:2012:MT%
		}.
\NAMECITE{Axiom}{%
		Clarke:1979:PLC,%
		Qian:1990:ASD%
		}.
\NAMECITE{Axiomatic}{%
		Bergstra:1984:ASP,%
		Hoare:1969:ABC,%
		Hoare:1972:ADP,%
		Hoare:1973:ADP,%
		Hoare:1974:ACA,%
		Hoare:1983:ABC,%
		Hoare:2001:ABC,%
		Hoare:2002:ABC,%
		Hoare:1971:PPA,%
		Hoare:1974:ADP,%
		Hoare:1975:PPA,%
		Hoare:1976:PPA,%
		Hoare:1996:PAB,%
		Hoare:1996:PPA,%
		Hoare:2009:VRA%
		}.
\NAMECITE{Axiomatics}{%
		Cherniavsky:1979:CCH%
		}.
\NAMECITE{{Axiomatization}}{%
		denHartog:2008:TMC%
		}.
\NAMECITE{Axiomatizations}{%
		Clarke:1983:EAH%
		}.


\NAMECITE{B}{%
		Horning:1989:BRE%
		}.
\NAMECITE{Based}{%
		Bergstra:1984:ASP,%
		Kaubisch:1982:DES,%
		Olderog:1981:SCH,%
		Barthe:2009:FCC%
		}.
\NAMECITE{basic}{%
		Bowen:1996:PIP%
		}.
\NAMECITE{Basis}{%
		Hoare:1961:MSS,%
		Hoare:1969:ABC,%
		Hoare:1983:ABC,%
		Hoare:2001:ABC,%
		Hoare:2002:ABC,%
		Hoare:1981:TMB,%
		Hoare:1996:PAB,%
		Hoare:2009:VRA%
		}.
\NAMECITE{Bazilevskii}{%
		Baer:1965:RPP%
		}.
\NAMECITE{BC}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{be}{%
		Page:1989:SME%
		}.
\NAMECITE{Beach}{%
		Rishe:1990:PIC%
		}.
\NAMECITE{Beauty}{%
		Feijen:1990:BOB%
		}.
\NAMECITE{bedrock}{%
		Chlipala:2013:BSP%
		}.
\NAMECITE{before}{%
		Hoare:1971:CSI,%
		Hoare:1986:MPI%
		}.
\NAMECITE{Behaviour}{%
		Hoare:2012:NMC%
		}.
\NAMECITE{behind}{%
		Hoare:1973:HLP%
		}.
\NAMECITE{being}{%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{Belfast}{%
		Hoare:1972:OST,%
		Hoare:1971:CSI,%
		Sufrin:2021:TBO%
		}.
\NAMECITE{Best}{%
		Cipra:2000:BCE%
		}.
\NAMECITE{better}{%
		Hoare:1972:PBP%
		}.
\NAMECITE{Binary}{%
		Lewis:1997:BCI%
		}.
\NAMECITE{Biographies}{%
		Jones:2021:ABI,%
		Weiss:1988:BOP%
		}.
\NAMECITE{Biographies/Index}{%
		Jones:2021:ABI%
		}.
\NAMECITE{Birthday}{%
		Feijen:1990:BOB,%
		Jones:2011:DHC,%
		Liu:2013:TPF,%
		Ribeiro:2019:UTP%
		}.
\NAMECITE{Blocks}{%
		Hoare:2011:RB%
		}.
\NAMECITE{Bonn}{%
		Broy:2001:PTC%
		}.
\NAMECITE{Book}{%
		Anonymous:1987:BRC,%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Hoare:1963:BR,%
		Hoare:1964:BRA,%
		Hoare:1970:BR,%
		Hoare:1970:BRC,%
		Hoare:1977:BR,%
		Horning:1989:BRE,%
		Lloyd:1974:BRS,%
		Brockhaus:1973:BRC%
		}.
\NAMECITE{Boston}{%
		ACM:1983:PFA%
		}.
\NAMECITE{Bottom}{%
		Hoare:1999:TPT%
		}.
\NAMECITE{Bottom-Up}{%
		Hoare:1999:TPT%
		}.
\NAMECITE{{Brian}}{%
		Jones:2011:DHC%
		}.
\NAMECITE{Broadcasting}{%
		Broy:1988:BBC%
		}.
\NAMECITE{{Brooks}}{%
		McReynolds:1997:LBS%
		}.
\NAMECITE{Buffering}{%
		Broy:1988:BBC%
		}.
\NAMECITE{Business}{%
		Feijen:1990:BOB%
		}.
\NAMECITE{Butterworths}{%
		Hoare:1970:BRC%
		}.


\NAMECITE{C}{%
		Anonymous:1987:BRC,%
		Baer:1965:RPP,%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Brockhaus:1973:BRC,%
		Hoare:1970:BRC,%
		Horning:1989:BRE,%
		Lloyd:1974:BRS,%
		Roscoe:1994:CME,%
		Feuer:1984:CAP,%
		Hoare:1988:PCC,%
		Hoare:1990:TDC,%
		Hoare:1991:TDCa,%
		Hoare:1991:TDCb,%
		Olsen:1997:LWJ%
		}.
\NAMECITE{{C-MOS}}{%
		Hoare:1988:PCC,%
		Hoare:1990:TDC,%
		Hoare:1991:TDCa,%
		Hoare:1991:TDCb%
		}.
\NAMECITE{{C.}}{%
		Ashcroft:1976:RPP,%
		Dijkstra:1970:LPC,%
		Dijkstra:1974:LCR,%
		Dijkstra:1975:VTO,%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa,%
		Dijkstra:1982:PTP,%
		Dijkstra:1982:VTO,%
		Dijkstra:20xx:ERC,%
		Hoare:1982:VTO,%
		Jones:2010:RWC,%
		Shustek:2009:IIC%
		}.
\NAMECITE{CA}{%
		Abadi:2005:CCT%
		}.
\NAMECITE{CADE}{%
		Kapur:1992:ADC%
		}.
\NAMECITE{CADE-11}{%
		Kapur:1992:ADC%
		}.
\NAMECITE{Calculi}{%
		Hoare:2012:LPU,%
		Olderog:1981:SCH,%
		vanStaden:2013:AUO,%
		Hoare:2014:LPU,%
		Kirkerud:1982:CHC%
		}.
\NAMECITE{Calculus}{%
		Hoare:1981:CTCb,%
		Hoare:2019:CST,%
		Reus:2001:HCV,%
		Wu:2019:USC,%
		Hoare:1981:CTCa,%
		Hoare:1982:CCT,%
		Hoare:1985:CNP,%
		Hoare:2019:CSTa,%
		Milner:1990:IOC,%
		Zhou:1991:CD,%
		vonKarger:1995:SC%
		}.
\NAMECITE{Call}{%
		deBoer:2021:CCR%
		}.
\NAMECITE{Call-by-Value}{%
		deBoer:2021:CCR%
		}.
\NAMECITE{Calls}{%
		BrinchHansen:2002:OCP,%
		Shaner:2007:MVH%
		}.
\NAMECITE{can}{%
		Page:1989:SME%
		}.
\NAMECITE{Canada}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{Card}{%
		Hoare:2010:UCT%
		}.
\NAMECITE{{Cartesian}}{%
		Sousa:2016:CHL%
		}.
\NAMECITE{Case}{%
		Hoare:1964:CE%
		}.
\NAMECITE{Categorical}{%
		He:1990:CSP,%
		Hoare:1990:CSP,%
		Knijnenburg:1992:CIP,%
		He:1990:DRC,%
		Hoare:1990:DRC%
		}.
\NAMECITE{categories}{%
		Martin:1991:PAO%
		}.
\NAMECITE{Category}{%
		Hoare:1989:NAC%
		}.
\NAMECITE{Causality}{%
		Hoare:2019:CST,%
		Hoare:2019:CSTa%
		}.
\NAMECITE{causally}{%
		Stoller:1995:VPU%
		}.
\NAMECITE{causally-ordered}{%
		Stoller:1995:VPU%
		}.
\NAMECITE{CBE}{%
		Hoare:2004:RMN%
		}.
\NAMECITE{{CCS}}{%
		He:2010:CRC%
		}.
\NAMECITE{{CE}}{%
		Gozum:1997:LWC%
		}.
\NAMECITE{{Century}}{%
		Cipra:2000:BCE%
		}.
\NAMECITE{certification}{%
		Barthe:2009:FCC%
		}.
\NAMECITE{Certified}{%
		Cai:2007:CSM,%
		Ni:2006:CAP%
		}.
\NAMECITE{Certifying}{%
		Chajed:2017:CFS%
		}.
\NAMECITE{Chain}{%
		Grubel:1998:HSA%
		}.
\NAMECITE{Challenge}{%
		Hoare:1996:UTC,%
		Hoare:2003:VCGa,%
		Hoare:2008:VST,%
		Hoare:2003:VCGb,%
		Hoare:2005:VCG,%
		Woodcock:2021:VGC%
		}.
\NAMECITE{Challenges}{%
		Hayes:2019:DAR,%
		Hoare:2004:GCC,%
		Hoare:2005:GCC%
		}.
\NAMECITE{Characterisation}{%
		Hoare:1994:ACO%
		}.
\NAMECITE{characterization}{%
		Olderog:1983:CHL%
		}.
\NAMECITE{characterizations}{%
		Makowsky:1989:WSO%
		}.
\NAMECITE{Charles}{%
		Black:2012:PSD,%
		Dijkstra:1999:FWT,%
		Frana:2002:ICA%
		}.
\NAMECITE{chief}{%
		Hoare:1970:BRC%
		}.
\NAMECITE{circuit}{%
		Hoare:1990:TDC,%
		Hoare:1991:TDCa,%
		Hoare:1991:TDCb%
		}.
\NAMECITE{circuits}{%
		Hoare:1988:PCC,%
		Hoare:1990:MSS,%
		Zhou:1992:MSS%
		}.
\NAMECITE{{CKA}}{%
		Moller:2015:EIM%
		}.
\NAMECITE{claims}{%
		Chisholm:1989:ARP%
		}.
\NAMECITE{class}{%
		Dijkstra:20xx:ERC%
		}.
\NAMECITE{Classic}{%
		Lewis:2021:ICF%
		}.
\NAMECITE{Classical}{%
		Feng:2021:QHL,%
		Roscoe:1994:CME%
		}.
\NAMECITE{{Clint}}{%
		Ashcroft:1976:RPP%
		}.
\NAMECITE{Closing}{%
		Hoare:1994:HSCa,%
		Hoare:1994:HSCb%
		}.
\NAMECITE{Clothes}{%
		Hoare:1981:EOC,%
		Hoare:1987:EOC%
		}.
\NAMECITE{{Club}}{%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{Co}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{Co-modelling}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{code}{%
		Barthe:2009:FCC,%
		Boyer:1992:ACP,%
		Boyer:1996:APO,%
		Cai:2007:CSM,%
		Hoare:2000:LC,%
		Ni:2006:CAP,%
		Thielecke:2006:FRA%
		}.
\NAMECITE{code-based}{%
		Barthe:2009:FCC%
		}.
\NAMECITE{{Coded}}{%
		Sun:1996:TRH%
		}.
\NAMECITE{Coinitial}{%
		Hoare:1979:CGW%
		}.
\NAMECITE{collection}{%
		Hoare:1974:OSS%
		}.
\NAMECITE{College}{%
		Jones:2013:ICC%
		}.
\NAMECITE{Collusion}{%
		Hoare:2007:SEC%
		}.
\NAMECITE{combinational}{%
		Hoare:1991:TDCa,%
		Hoare:1991:TDCb%
		}.
\NAMECITE{Combining}{%
		Groote:1994:PAG,%
		Chlipala:2013:BSP%
		}.
\NAMECITE{Comm}{%
		Hoare:1987:CLP%
		}.
\NAMECITE{Command}{%
		Enslow:1975:ILRc,%
		Hoare:1975:HDP,%
		Hoare:1976:HDP%
		}.
\NAMECITE{Comments}{%
		Enslow:1975:ILRb,%
		Enslow:1975:ILRc,%
		Pettersson:1991:LEC,%
		Pritchard:1979:CPJ,%
		Simauti:1967:CCD,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{commercial}{%
		Boyer:1992:ACP%
		}.
\NAMECITE{Communicating}{%
		Brookes:1984:TCS,%
		Hoare:1978:CCS,%
		Hoare:1978:CSPa,%
		Hoare:1978:CSPb,%
		Hoare:1981:CTCb,%
		Hoare:1981:PCC,%
		Hoare:1985:CSP,%
		Hoare:1986:NCS,%
		Hoare:1987:ASP,%
		Hoare:2002:CSP,%
		Hoare:2008:SLS,%
		Hoare:2021:CSP,%
		Kaubisch:1982:DES,%
		Olderog:1986:SOS,%
		Enikeev:1987:MTC,%
		Hehner:1983:MCM,%
		Hoare:1980:MCSa,%
		Hoare:1980:MCSb,%
		Hoare:1981:CTCa,%
		Hoare:1981:MCS,%
		Hoare:1982:CCT,%
		Hoare:1983:NCS,%
		Hoare:1985:NCS,%
		Hoare:1991:ASP,%
		Olderog:1983:SOS,%
		Zhou:1981:PCC,%
		deBoer:2002:HLD,%
		Abdallah:2005:CSP,%
		Hoare:1983:CSP,%
		Anonymous:1987:BRC%
		}.
\NAMECITE{Communication}{%
		Broy:1988:BBC,%
		Hoare:1991:DCC,%
		Silberschatz:1981:PDC,%
		Francez:1978:SNC,%
		Francez:1979:SNC%
		}.
\NAMECITE{communications}{%
		Hoare:1993:WSE%
		}.
\NAMECITE{commute}{%
		Flannery:1990:HSP%
		}.
\NAMECITE{Comparing}{%
		Bruni:2005:CTA,%
		Feuer:1984:CAP%
		}.
\NAMECITE{Comparisons}{%
		Kirschenhofer:1998:CHF%
		}.
\NAMECITE{Compensable}{%
		Hoare:2007:CT,%
		Hoare:2010:CT,%
		Bruni:2005:CTA%
		}.
\NAMECITE{compilation}{%
		Hoare:1966:SPC,%
		Hoare:1992:RAP%
		}.
\NAMECITE{Compiler}{%
		Hoare:1993:NFA,%
		Hoare:2003:TVC,%
		Hoare:2003:VCGa,%
		Hoare:2004:TVC,%
		Bicarregui:2006:VSR,%
		Hoare:2003:VC,%
		Hoare:2003:VCGb,%
		Hoare:2005:VCG%
		}.
\NAMECITE{compiling}{%
		Hoare:1990:AAV,%
		Hoare:1990:RAPa,%
		Hoare:1990:RAPb%
		}.
\NAMECITE{Complementary}{%
		Hoare:1974:CCF%
		}.
\NAMECITE{Complete}{%
		Cherniavsky:1979:CCH,%
		Damm:1983:SRH,%
		Olderog:1981:SCH,%
		Arthan:2009:GFS,%
		Hehner:1983:MCM%
		}.
\NAMECITE{Completeness}{%
		Bergstra:1982:TTA,%
		Kirkerud:1982:CHC,%
		Xu:2016:CHL,%
		deBoer:2021:CCR,%
		Bergstra:1982:ECH,%
		Gardiner:1995:APC,%
		RodriguezArtalejo:1985:SQA%
		}.
\NAMECITE{Complexity}{%
		Hoare:1993:MPM,%
		deBoer:2021:CCR,%
		Cohen:2000:NCP%
		}.
\NAMECITE{composition}{%
		Bruni:2005:CTA,%
		Flannery:1990:HSP%
		}.
\NAMECITE{Compositional}{%
		Hooman:1992:CVR,%
		DeBoer:1997:HSC,%
		Saabas:2007:CNS%
		}.
\NAMECITE{computable}{%
		Blass:2001:ICL%
		}.
\NAMECITE{computation}{%
		Jacobs:2015:DHM,%
		Nielson:1987:HLP%
		}.
\NAMECITE{Computations}{%
		Guttmann:2019:CFC%
		}.
\NAMECITE{Computer}{%
		Barthe:2012:PRH,%
		Herbert:2004:CST,%
		Hoare:1969:ABC,%
		Hoare:1971:CSI,%
		Hoare:1973:CPE,%
		Hoare:1976:CST,%
		Hoare:1983:ABC,%
		Hoare:1989:NAC,%
		Hoare:2001:ABC,%
		Hoare:2001:ETS,%
		Hoare:2002:ABC,%
		Hofner:2014:RAM,%
		IEEE:1976:ASF,%
		IEEE:1988:ASL,%
		IEEE:2002:AIC,%
		Lewis:2021:ICF,%
		Berghammer:2009:RKA,%
		Davies:2000:MPC,%
		Hoare:1981:TMB,%
		Hoare:1986:MAS,%
		Hoare:1989:FMC,%
		Hoare:1996:PAB,%
		Hoare:2009:VRA,%
		Hoare:2007:IPC,%
		Hoare:1970:BRC%
		}.
\NAMECITE{Computer-Aided}{%
		Barthe:2012:PRH%
		}.
\NAMECITE{Computing}{%
		ACM:1983:PFA,%
		Dijkstra:1982:SWC,%
		Hoare:1989:ECS,%
		Hoare:1996:UTC,%
		Hoare:2003:VCGa,%
		Hoare:2004:GCC,%
		Hoare:2005:GCC,%
		Jones:2011:DHC,%
		Jones:2013:ICC,%
		Pritchard:1979:CPJ,%
		Anonymous:1976:SSE,%
		Hoare:1996:MMC,%
		Hoare:1998:SCE,%
		Hoare:2003:KTK,%
		Hoare:2003:VCGb,%
		Hoare:2005:VCG,%
		Horning:1989:BRE,%
		ACM:1976:SPE%
		}.
\NAMECITE{Concept}{%
		Hoare:1974:MOS,%
		Hoare:2002:MOS%
		}.
\NAMECITE{CONCUR}{%
		Abadi:2005:CCT,%
		Abadi:2005:CCT,%
		Baeten:1990:CTC%
		}.
\NAMECITE{Concurrency}{%
		Baeten:1990:CTC,%
		Butterfield:2019:IOA,%
		Hayes:2019:DAR,%
		Hoare:1991:DCC,%
		Hoare:2010:FGCa,%
		Struth:2021:THA,%
		Abadi:2005:CCT,%
		Cleaveland:1996:SDC,%
		DeBoer:1997:HSC,%
		Francez:1978:SNC,%
		Francez:1979:SNC,%
		He:2005:LTC,%
		Hoare:1990:TCC,%
		Hoare:1991:TCC,%
		Hoare:1997:UTC,%
		Hoare:2010:FGCb,%
		Hoare:2013:LPC,%
		Turon:2013:URH%
		}.
\NAMECITE{Concurrent}{%
		BrinchHansen:2002:OCP,%
		Hoare:2009:CKA,%
		Hoare:2011:CKA,%
		Hoare:2012:NMC,%
		Lamport:1980:HLC,%
		Shankar:1993:IAR,%
		Hoare:2008:VFG,%
		Hoare:2009:FCK,%
		Hoare:2011:LEL,%
		Hoare:2013:USC,%
		Hoare:2014:DCK,%
		Hoare:2014:LCP,%
		Hoare:2016:DCK,%
		Milner:1990:IOC,%
		Sergey:2016:HSS,%
		Shapiro:2006:PPC,%
		Stirling:1988:GOG,%
		Vafeiadis:2006:PCH%
		}.
\NAMECITE{condition}{%
		He:2000:UTH,%
		Homeier:1995:MVV%
		}.
\NAMECITE{conditions}{%
		Sergey:2016:HSS%
		}.
\NAMECITE{Conference}{%
		Abadi:2005:CCT,%
		Berghammer:2009:RKA,%
		Bottaci:2010:TAI,%
		Broy:2001:PTC,%
		Gibbons:2012:MPC,%
		Haddad:2012:ATP,%
		Hofner:2014:RAM,%
		IEEE:2000:PSA,%
		IEEE:2002:AIC,%
		Kapur:1992:ADC,%
		Meyer:2008:VST,%
		Ryder:1999:PAS,%
		Anonymous:1976:SSE,%
		Rishe:1990:PIC%
		}.
\NAMECITE{conformance}{%
		Fournet:2004:SFC%
		}.
\NAMECITE{conjunction}{%
		Hoare:1990:TCC,%
		Hoare:1991:TCC%
		}.
\NAMECITE{Connecting}{%
		Guttmann:2019:CFC%
		}.
\NAMECITE{conservation}{%
		Hoare:1973:GCL%
		}.
\NAMECITE{considerations}{%
		Pratt:1976:SCF%
		}.
\NAMECITE{consistency}{%
		Gardiner:1995:APC,%
		Hoare:1982:CCT%
		}.
\NAMECITE{Consistent}{%
		Cherniavsky:1979:CCH,%
		Hoare:1974:CCF%
		}.
\NAMECITE{Constrained}{%
		Reus:2001:HCV%
		}.
\NAMECITE{Construction}{%
		Hoare:2001:ETS,%
		Gibbons:2012:MPC,%
		vanAmmers:1998:PCC%
		}.
\NAMECITE{constructors}{%
		Flannery:1990:HSP%
		}.
\NAMECITE{Constructs}{%
		Clarke:1979:PLC%
		}.
\NAMECITE{context}{%
		vanAmmers:1998:PCC%
		}.
\NAMECITE{Continuations}{%
		Tennent:1991:CPW,%
		Delbianco:2013:HSR%
		}.
\NAMECITE{Contradiction}{%
		Hoare:1978:ESS%
		}.
\NAMECITE{Contribution}{%
		Wirth:1965:CDA,%
		Wirth:1966:CDA,%
		Wirth:1966:ECD,%
		Simauti:1967:CCD%
		}.
\NAMECITE{Contributions}{%
		Broy:2001:PTC,%
		Broy:2002:SPC,%
		Broy:2001:PTC%
		}.
\NAMECITE{Control}{%
		Enslow:1975:ILRc,%
		Hoare:1993:MPM,%
		Hoare:1975:HDP,%
		Hoare:1976:HDP%
		}.
\NAMECITE{conversation}{%
		Dale:1994:CST%
		}.
\NAMECITE{Copy}{%
		Olderog:1981:SCH%
		}.
\NAMECITE{Copying}{%
		vanDiepen:1986:PDT%
		}.
\NAMECITE{Correct}{%
		He:1994:PCS%
		}.
\NAMECITE{Correctness}{%
		Anonymous:2007:DIPa,%
		Anonymous:2007:DIPb,%
		Hoare:1981:CTCb,%
		Hoare:1981:PCC,%
		Hoare:2001:PCD,%
		Hoare:2002:PCD,%
		Hoare:2007:IPC,%
		Olderog:1984:CPP,%
		Boyer:1992:ACP,%
		Chajed:2017:CFS,%
		Fokkinga:1987:CPS,%
		Gritzner:1996:RAM,%
		Hoare:1972:PCD,%
		Hoare:1975:PCP,%
		Hoare:1976:PCD,%
		Hoare:1981:CTCa,%
		Hoare:1982:CCT,%
		Hoare:1988:PCC,%
		Hoare:1990:MSS,%
		Hoare:1990:RAPa,%
		Hoare:1990:RAPb,%
		Hoare:1992:RAP,%
		Hoare:1996:PPC,%
		Sergey:2016:HSS,%
		Vafeiadis:2006:PCH,%
		Zhou:1981:PCC,%
		Zhou:1992:MSS,%
		denHartog:2008:TMC%
		}.
\NAMECITE{Corrigenda}{%
		Hoare:1974:ACA,%
		Hoare:1987:CLP%
		}.
\NAMECITE{Corrigendum}{%
		Hoare:1978:CCS%
		}.
\NAMECITE{cost}{%
		Hoare:1976:HCP%
		}.
\NAMECITE{couple}{%
		Hoare:1985:CNP%
		}.
\NAMECITE{courses}{%
		Hoare:1976:SPI%
		}.
\NAMECITE{{Crash}}{%
		Chajed:2017:CFS%
		}.
\NAMECITE{crashes}{%
		Chajed:2017:CFS%
		}.
\NAMECITE{Created}{%
		Lewis:2021:ICF%
		}.
\NAMECITE{Critic}{%
		Lewis:1997:BCI%
		}.
\NAMECITE{Critique}{%
		Greif:1981:SSW,%
		Hoare:1968:CA,%
		ODonnell:1982:CFH%
		}.
\NAMECITE{cryptographic}{%
		Barthe:2009:FCC,%
		denHartog:2008:TMC%
		}.
\NAMECITE{CSP}{%
		Abdallah:2005:CSP,%
		Brookes:2021:CPP,%
		He:2010:CRC,%
		Hoare:1985:SSN,%
		Hoare:2006:WEC,%
		Lamport:1984:HLC,%
		May:2021:COI,%
		Sridhar:1985:JEC%
		}.
\NAMECITE{Cultures}{%
		Hoare:2007:SEC%
		}.
\NAMECITE{{CV}}{%
		Misra:2021:C%
		}.
\NAMECITE{Cyber}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{Cyber-Physical}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{Cyclic}{%
		Brotherston:2008:CPP%
		}.


\NAMECITE{{D.}}{%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa%
		}.
\NAMECITE{Dahl}{%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Lloyd:1974:BRS,%
		Owe:2004:OOF%
		}.
\NAMECITE{Data}{%
		Banerjee:2022:RPL,%
		He:1986:DRR,%
		He:1990:DRC,%
		Hoare:1968:DST,%
		Hoare:1975:DR,%
		Hoare:1990:DRC,%
		Hoare:2001:PCD,%
		Hoare:2002:PCD,%
		Bergstra:1984:HLP,%
		Hoare:1972:NDS,%
		Hoare:1972:PCD,%
		Hoare:1975:RDS,%
		Hoare:1976:PCD,%
		Hoare:1987:PDR,%
		Hoare:1996:PPC,%
		Hoare:2011:UMD,%
		LeGuyadec:1996:SLP,%
		Wing:1989:VAD%
		}.
\NAMECITE{data-parallel}{%
		LeGuyadec:1996:SLP%
		}.
\NAMECITE{Database}{%
		Lenzerini:2008:PTS,%
		Qian:1990:ASD%
		}.
\NAMECITE{databases}{%
		Rishe:1990:PIC%
		}.
\NAMECITE{Dawn}{%
		Daylight:2012:DSE%
		}.
\NAMECITE{Deadlocks}{%
		Struble:1997:LDJ%
		}.
\NAMECITE{decidable}{%
		Bergstra:1982:SNS%
		}.
\NAMECITE{Decisions}{%
		Hayes:2019:DAR%
		}.
\NAMECITE{decomposition}{%
		Takaoka:1987:DRH%
		}.
\NAMECITE{Dedicated}{%
		Jones:2011:DHC,%
		Liu:2013:TPF,%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa,%
		Dijkstra:1999:FWT,%
		Ribeiro:2019:UTP,%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{deduction}{%
		Kapur:1992:ADC%
		}.
\NAMECITE{Deductive}{%
		Broy:1996:DPD%
		}.
\NAMECITE{Definition}{%
		Hoare:1972:ADP,%
		Hoare:1973:ADP,%
		Hoare:1974:ACA,%
		Hoare:1974:ADP,%
		Hoare:1996:PPA%
		}.
\NAMECITE{delivered}{%
		Hoare:1971:CSI,%
		Hoare:1986:MPI%
		}.
\NAMECITE{Denotational}{%
		Aichernig:2019:TPA%
		}.
\NAMECITE{Dependable}{%
		Jones:2011:DHC%
		}.
\NAMECITE{dependent}{%
		Nanevski:2008:YDT%
		}.
\NAMECITE{Derivation}{%
		vanDiepen:1986:PDT,%
		Hoare:1990:TDC,%
		Hoare:1991:TDCa,%
		Hoare:1991:TDCb,%
		Hoare:1997:ADO,%
		Hoare:2000:ADO%
		}.
\NAMECITE{described}{%
		Page:1989:SME%
		}.
\NAMECITE{Design}{%
		Enslow:1975:ILRb,%
		Hayes:2019:DAR,%
		Hoare:1973:HPLa,%
		Hoare:1973:HPLb,%
		Hoare:1973:HPLc,%
		Hoare:1987:DPM,%
		Hoare:1987:OSF,%
		Hoare:1991:DPM,%
		Hoare:1993:NFA,%
		Reus:2001:HCV,%
		Ryder:1999:PAS,%
		Broy:1996:DPD,%
		Gordon:1992:MRH,%
		Hoare:1974:HPL,%
		Hoare:1974:SDP,%
		Hoare:1975:HDP,%
		Hoare:1976:HDP,%
		Hoare:1989:FMC,%
		Hoare:1996:LED,%
		Hoare:2010:MJD%
		}.
\NAMECITE{designs}{%
		Hoare:1990:TDC,%
		Hoare:1991:TDCa,%
		Hoare:1991:TDCb%
		}.
\NAMECITE{determinism}{%
		Hoare:1980:TND%
		}.
\NAMECITE{Deterministic}{%
		Mamouras:2016:HLD,%
		deBoer:2002:HLD%
		}.
\NAMECITE{Developing}{%
		Hayes:2019:DAR%
		}.
\NAMECITE{Development}{%
		Wirth:1965:CDA,%
		Wirth:1966:CDA,%
		Wirth:1966:ECD,%
		Bjorner:1990:VVZ,%
		Simauti:1967:CCD%
		}.
\NAMECITE{Developments}{%
		Hoare:1991:DCC,%
		Hoare:2014:DCK,%
		Hoare:2016:DCK%
		}.
\NAMECITE{dialog}{%
		Enikeev:1987:MTC%
		}.
\NAMECITE{did}{%
		Hoare:1996:HDS%
		}.
\NAMECITE{Dijkstra}{%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Lloyd:1974:BRS,%
		Apt:2022:EWD,%
		Boyer:2002:MEW,%
		Daylight:2012:DSE,%
		Feijen:1990:BOB,%
		Hoare:2003:EWD,%
		Jacobs:2015:DHM%
		}.
\NAMECITE{Directed}{%
		Silberschatz:1981:PDC%
		}.
\NAMECITE{directions}{%
		Cleaveland:1996:SDC%
		}.
\NAMECITE{discipline}{%
		Dijkstra:1976:DP,%
		Hoare:1973:CPE%
		}.
\NAMECITE{disciplines}{%
		Hoare:1973:GCL%
		}.
\NAMECITE{Discrete}{%
		Kaubisch:1982:DES%
		}.
\NAMECITE{Discussion}{%
		Anonymous:2007:DIPa,%
		Anonymous:2007:DIPb,%
		Gordon:1992:MRH%
		}.
\NAMECITE{{Discussions}}{%
		Meyer:2008:VST%
		}.
\NAMECITE{Distinguished}{%
		Hoare:2012:MT,%
		Black:2012:PSD,%
		Hoare:2012:MTR%
		}.
\NAMECITE{Distributed}{%
		Joseph:1987:PRF,%
		He:1987:ASP,%
		Mancini:1988:HLD,%
		Rehof:2010:ADS,%
		Ridge:2009:VDS,%
		VanGasteren:1990:CPD,%
		Verjus:1987:PDA%
		}.
\NAMECITE{Distribution}{%
		Grubel:1996:ADT%
		}.
\NAMECITE{Doctoral}{%
		Jones:2021:DS%
		}.
\NAMECITE{does}{%
		Hoare:2004:YWT%
		}.
\NAMECITE{Doha}{%
		Berghammer:2009:RKA%
		}.
\NAMECITE{{DOM}}{%
		Gardner:2008:LHR%
		}.
\NAMECITE{domain}{%
		Flannery:1990:HSP%
		}.
\NAMECITE{Down}{%
		Hoare:1999:TPT,%
		Olsen:1997:LWJ%
		}.
\NAMECITE{Draft}{%
		Hoare:1968:RDR,%
		Woodger:1969:MRA%
		}.
\NAMECITE{{DSE}}{%
		Hoare:2004:EHDa,%
		Hoare:2004:EHDb%
		}.
\NAMECITE{durations}{%
		Zhou:1991:CD%
		}.
\NAMECITE{Dynamic}{%
		Banerjee:2022:RPL,%
		deBoer:2002:HLD%
		}.


\NAMECITE{{E.}}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{ed}{%
		Horning:1989:BRE%
		}.
\NAMECITE{Edinburgh}{%
		IEEE:1988:ASL%
		}.
\NAMECITE{Editor}{%
		Pettersson:1991:LEC,%
		Welch:1997:LEI%
		}.
\NAMECITE{Editorial}{%
		Hoare:1972:GEQ,%
		Hoare:1994:GE%
		}.
\NAMECITE{Editors}{%
		Cipra:2000:BCE%
		}.
\NAMECITE{{Edsger}}{%
		Apt:2022:EWD,%
		Boyer:2002:MEW,%
		Feijen:1990:BOB,%
		Hoare:2003:EWD,%
		Hoare:2022:FYE%
		}.
\NAMECITE{Effective}{%
		Clarke:1983:EAH,%
		Jones:2021:FEA%
		}.
\NAMECITE{Effects}{%
		vonOheimb:2002:HLN%
		}.
\NAMECITE{Efficient}{%
		Johnston:1975:MRE%
		}.
\NAMECITE{eighth}{%
		ACM:1976:SPE%
		}.
\NAMECITE{elected}{%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{Elements}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA,%
		Prodinger:1995:MQH%
		}.
\NAMECITE{{Elliott}}{%
		Hoare:1962:REA,%
		Hoare:1963:EAI,%
		Hoare:1964:EAP%
		}.
\NAMECITE{embedded}{%
		Ni:2006:CAP%
		}.
\NAMECITE{Emeritus}{%
		Anonymous:20xx:THE%
		}.
\NAMECITE{emperor}{%
		Hoare:1987:EOC,%
		Hoare:1981:EOC%
		}.
\NAMECITE{Engeering}{%
		IEEE:2000:PSA%
		}.
\NAMECITE{Engineering}{%
		Beckert:2006:ISF,%
		Broy:2001:PTC,%
		Broy:2002:SPC,%
		Broy:2003:MAL,%
		Broy:2005:ETS,%
		Daylight:2012:DSE,%
		Hoare:1978:ESS,%
		Hoare:2001:ETS,%
		Hoare:2002:APS,%
		Hoare:2007:SEC,%
		Anonymous:1976:SSE,%
		Hoare:1973:CPE,%
		Hoare:1975:SE,%
		Hoare:1978:SEK,%
		Hoare:1983:PEP,%
		Hoare:1993:WSE,%
		Hoare:1996:LED,%
		Hoare:1998:SCE,%
		Hoare:2002:AMS,%
		Muller:2010:ALS%
		}.
\NAMECITE{{England}}{%
		IEEE:2002:AIC%
		}.
\NAMECITE{enriched}{%
		Martin:1991:PAO%
		}.
\NAMECITE{Envoi}{%
		Hoare:2021:E%
		}.
\NAMECITE{{Eratosthenes}}{%
		Hoare:1972:PSP%
		}.
\NAMECITE{Errata}{%
		Wirth:1966:ECD%
		}.
\NAMECITE{{Esprit}}{%
		Bowen:1996:PIP%
		}.
\NAMECITE{Essays}{%
		Hoare:1989:ECS,%
		Jones:2011:DHC,%
		Liu:2013:TPF,%
		Manna:2010:TVE,%
		Owe:2004:OOF,%
		Roscoe:1994:CME,%
		Horning:1989:BRE%
		}.
\NAMECITE{EUROCOMP}{%
		Anonymous:1976:SSE%
		}.
\NAMECITE{Europe}{%
		Bjorner:1990:VVZ%
		}.
\NAMECITE{European}{%
		Anonymous:1976:SSE%
		}.
\NAMECITE{Event}{%
		Kaubisch:1982:DES%
		}.
\NAMECITE{ever}{%
		Hoare:2006:WEC%
		}.
\NAMECITE{Evolution}{%
		vanDiepen:1986:PDT%
		}.
\NAMECITE{exception}{%
		Cocco:1982:MEH,%
		Szczepanska:1991:HLV%
		}.
\NAMECITE{Exceptions}{%
		PeytonJones:1999:SIE,%
		Jones:1999:SIE%
		}.
\NAMECITE{exchange}{%
		Hoare:2011:LEL%
		}.
\NAMECITE{exclusion}{%
		Page:1989:SME%
		}.
\NAMECITE{executable}{%
		Hoare:1984:PEP%
		}.
\NAMECITE{exercise}{%
		Dijkstra:1989:ETH,%
		Hoare:1988:PCC%
		}.
\NAMECITE{Experiment}{%
		Dijkstra:20xx:ERC%
		}.
\NAMECITE{Experiments}{%
		Hoare:2008:VST,%
		Meyer:2008:VST%
		}.
\NAMECITE{Exploring}{%
		Moller:2015:EIM%
		}.
\NAMECITE{expressed}{%
		Sridhar:1985:JEC%
		}.
\NAMECITE{expressions}{%
		Hoare:1964:CE%
		}.
\NAMECITE{expressive}{%
		Hoofman:1991:WEM%
		}.
\NAMECITE{Expressiveness}{%
		Bergstra:1982:ECH,%
		Olderog:1983:NER,%
		RodriguezArtalejo:1985:SQA%
		}.
\NAMECITE{Extended}{%
		Hooman:1992:CVR%
		}.
\NAMECITE{Extending}{%
		Hoare:2004:EHDa,%
		Hoare:2004:EHDb,%
		Hooman:1994:EHL%
		}.
\NAMECITE{extensible}{%
		Chlipala:2013:BSP%
		}.
\NAMECITE{Extension}{%
		Baeten:1990:CTC%
		}.


\NAMECITE{F}{%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa%
		}.
\NAMECITE{fail}{%
		Bergstra:1982:SNS%
		}.
\NAMECITE{Fast}{%
		Macnaghten:1977:FFT%
		}.
\NAMECITE{Fault}{%
		Joseph:1987:PRF%
		}.
\NAMECITE{Favorite}{%
		Kernighan:1984:WPM,%
		Kernighan:1981:WPM%
		}.
\NAMECITE{{FBCS}}{%
		Black:2012:PSD%
		}.
\NAMECITE{February}{%
		Hoare:1971:CSI,%
		Hoare:2004:RMN%
		}.
\NAMECITE{{Fellow}}{%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{Fifteen}{%
		Mller:2021:FFY%
		}.
\NAMECITE{fifteenth}{%
		ACM:1983:PFA%
		}.
\NAMECITE{Fifty}{%
		Apt:2019:FYH%
		}.
\NAMECITE{file}{%
		Chajed:2017:CFS%
		}.
\NAMECITE{final}{%
		Bowen:1996:PIP,%
		Woodger:1969:MRA%
		}.
\NAMECITE{{FIND}}{%
		Hoare:1971:PPF,%
		Fouz:2012:SAQ,%
		Hoare:1961:AF,%
		Prodinger:1995:MQH,%
		Kirschenhofer:1998:CHF%
		}.
\NAMECITE{Finding}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA,%
		Jones:2021:FEA%
		}.
\NAMECITE{Fine}{%
		Dijkstra:1982:MSMa,%
		Hoare:2010:FGCa,%
		Hoare:2010:FGCb,%
		Dijkstra:1977:MSM,%
		Hoare:2008:VFG%
		}.
\NAMECITE{Fine-Grain}{%
		Hoare:2010:FGCa,%
		Hoare:2010:FGCb,%
		Hoare:2008:VFG%
		}.
\NAMECITE{Fine-Grained}{%
		Dijkstra:1982:MSMa,%
		Dijkstra:1977:MSM%
		}.
\NAMECITE{First}{%
		Meyer:2008:VST,%
		Mller:2021:FFY,%
		Abdallah:2005:CSP,%
		Ashenhurst:1987:ATA%
		}.
\NAMECITE{Fixed}{%
		Hoare:1990:FPI%
		}.
\NAMECITE{Fixpoints}{%
		Guttmann:2019:CFC%
		}.
\NAMECITE{flitting}{%
		Hoare:2004:VIF%
		}.
\NAMECITE{Florida}{%
		Rishe:1990:PIC%
		}.
\NAMECITE{flow}{%
		Bruni:2005:CTA,%
		Hoare:2011:UMD%
		}.
\NAMECITE{{Floyd}}{%
		Arthan:2009:GFS,%
		Bloom:1991:FHL,%
		Chisholm:1989:ARP,%
		Pratt:1976:SCF,%
		Ying:2011:FHL%
		}.
\NAMECITE{{Floyd-Hoare}}{%
		Arthan:2009:GFS%
		}.
\NAMECITE{Follow}{%
		Hoare:2000:HAF%
		}.
\NAMECITE{forecast}{%
		Hoare:1983:TF%
		}.
\NAMECITE{Foreword}{%
		Hoare:1976:F,%
		Hoare:1994:F%
		}.
\NAMECITE{Form}{%
		Hoare:1993:NFA%
		}.
\NAMECITE{Formal}{%
		Barthe:2009:FCC,%
		Beckert:2006:ISF,%
		Hoare:1974:CCF,%
		Hoare:1987:OSF,%
		Hoare:1989:FMC,%
		Liu:2013:TPF,%
		Owe:2004:OOF,%
		Bjorner:1990:VVZ,%
		Fokkinga:1987:CPS%
		}.
\NAMECITE{formula}{%
		Dijkstra:1999:FWT%
		}.
\NAMECITE{Forty}{%
		Hoare:2022:FYE%
		}.
\NAMECITE{Foundations}{%
		Hoare:2009:FCK,%
		IEEE:1976:ASF,%
		ODonnell:1982:CFH,%
		Hoare:1993:PPT,%
		Hoare:2011:CKA%
		}.
\NAMECITE{{Fourier}}{%
		Macnaghten:1977:FFT%
		}.
\NAMECITE{Fractional}{%
		Hoare:2004:FSP%
		}.
\NAMECITE{Frame}{%
		Thielecke:2006:FRA%
		}.
\NAMECITE{framework}{%
		Arthan:2009:GFS%
		}.
\NAMECITE{Framing}{%
		Banerjee:2022:RPL%
		}.
\NAMECITE{France}{%
		Wolff:2013:UTP%
		}.
\NAMECITE{Francisco}{%
		Abadi:2005:CCT%
		}.
\NAMECITE{Free}{%
		Macnaghten:1977:FFT,%
		Fournet:2004:SFC%
		}.
\NAMECITE{FREng}{%
		Black:2012:PSD,%
		Hoare:2004:RMN%
		}.
\NAMECITE{FRG}{%
		Bjorner:1990:VVZ%
		}.
\NAMECITE{FRS}{%
		Black:2012:PSD%
		}.
\NAMECITE{Function}{%
		Knijnenburg:1992:CIP%
		}.
\NAMECITE{Functions}{%
		Clint:1972:PPJ,%
		Hoare:1972:OSTb,%
		Hoare:1990:FPI,%
		Ashcroft:1976:RPP%
		}.
\NAMECITE{Future}{%
		Lewis:2021:ICF%
		}.


\NAMECITE{Gap}{%
		Hoare:1994:HSCa,%
		Hoare:1994:HSCb%
		}.
\NAMECITE{garbage}{%
		Hoare:1974:OSS%
		}.
\NAMECITE{GC6}{%
		Hoare:2004:EHDa%
		}.
\NAMECITE{General}{%
		Enslow:1975:ILRb,%
		Arthan:2009:GFS,%
		Csirmaz:1981:PPV,%
		Hoare:1973:GCL%
		}.
\NAMECITE{generalization}{%
		Stirling:1988:GOG%
		}.
\NAMECITE{generalized}{%
		Nguyen:1986:GOMa%
		}.
\NAMECITE{generative}{%
		Chlipala:2013:BSP%
		}.
\NAMECITE{generator}{%
		Homeier:1995:MVV%
		}.
\NAMECITE{Generic}{%
		Hoare:2013:GML%
		}.
\NAMECITE{genetically}{%
		Bernot:2019:GMH%
		}.
\NAMECITE{Geometry}{%
		Hoare:2019:CST,%
		Hoare:2019:CSTa%
		}.
\NAMECITE{Georgia}{%
		Ryder:1999:PAS%
		}.
\NAMECITE{Germany}{%
		Broy:1996:DPD,%
		Haddad:2012:ATP,%
		Hofner:2014:RAM%
		}.
\NAMECITE{get}{%
		Hoare:1996:HDS%
		}.
\NAMECITE{global}{%
		Olderog:1984:CPP%
		}.
\NAMECITE{Good}{%
		Clarke:1979:PLC%
		}.
\NAMECITE{{GOTO}}{%
		Lifschitz:1984:VPG%
		}.
\NAMECITE{{GPU}}{%
		Kojima:2017:HLG%
		}.
\NAMECITE{grail}{%
		Hoare:2003:KTK%
		}.
\NAMECITE{Grain}{%
		Hoare:2010:FGCa,%
		Hoare:2008:VFG,%
		Hoare:2010:FGCb%
		}.
\NAMECITE{Grained}{%
		Dijkstra:1982:MSMa,%
		Dijkstra:1977:MSM%
		}.
\NAMECITE{Grand}{%
		Hoare:2003:VCGa,%
		Hoare:2004:GCC,%
		Hoare:2005:GCC,%
		Hoare:2008:VST,%
		Hoare:2003:VCGb,%
		Hoare:2005:VCG,%
		Woodcock:2021:VGC%
		}.
\NAMECITE{grape}{%
		Hoare:2004:VIF%
		}.
\NAMECITE{Graph}{%
		Poskitt:2012:HSV%
		}.
\NAMECITE{Graphical}{%
		Wehrman:2009:GMS,%
		Zhan:2019:UGC%
		}.
\NAMECITE{graphically}{%
		Page:1989:SME%
		}.
\NAMECITE{graphs}{%
		Hoare:1979:CGW%
		}.
\NAMECITE{gratitude}{%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa%
		}.
\NAMECITE{{Gries}}{%
		Stirling:1988:GOG%
		}.
\NAMECITE{Guarantee}{%
		Hayes:2019:DAR%
		}.
\NAMECITE{guards}{%
		Groote:1994:PAG%
		}.
\NAMECITE{Guest}{%
		Hoare:1972:GEQ,%
		Hoare:1994:GE%
		}.
\NAMECITE{guide}{%
		Hoare:1970:BRC%
		}.


\NAMECITE{H}{%
		Brockhaus:1973:BRC%
		}.
\NAMECITE{Hall}{%
		Anonymous:1987:BRC,%
		Horning:1989:BRE%
		}.
\NAMECITE{Hamburg}{%
		Haddad:2012:ATP%
		}.
\NAMECITE{hand}{%
		Hoare:2010:TPH%
		}.
\NAMECITE{handling}{%
		Cocco:1982:MEH,%
		Hoare:1965:RH,%
		Hoare:1968:RH,%
		Szczepanska:1991:HLV%
		}.
\NAMECITE{Hard}{%
		Hoare:2000:HAF%
		}.
\NAMECITE{hardback}{%
		Horning:1989:BRE%
		}.
\NAMECITE{Hardware}{%
		Hoare:1994:HSCa,%
		Hoare:1994:HSCb,%
		Gordon:1992:MRH%
		}.
\NAMECITE{healthiness}{%
		He:2000:UTH%
		}.
\NAMECITE{Hedges}{%
		Struth:2021:THA%
		}.
\NAMECITE{held}{%
		Bauer:1976:LHI,%
		Broy:1996:DPD,%
		Ershov:1974:IST,%
		Gordon:1992:MRH%
		}.
\NAMECITE{Help}{%
		Hoare:1993:MPM%
		}.
\NAMECITE{Hemel}{%
		Horning:1989:BRE%
		}.
\NAMECITE{Hempstead}{%
		Horning:1989:BRE%
		}.
\NAMECITE{Hierarchical}{%
		Dahl:1972:HPS,%
		Dijkstra:1971:HOS%
		}.
\NAMECITE{hierarchies}{%
		Bauer:1976:LHI%
		}.
\NAMECITE{High}{%
		Hoare:1973:HLP,%
		Hoare:1976:HCP%
		}.
\NAMECITE{Higher}{%
		Damm:1983:SRH,%
		Naumann:1995:PTH,%
		Shaner:2007:MVH,%
		Turon:2013:URH%
		}.
\NAMECITE{higher-order}{%
		Naumann:1995:PTH,%
		Shaner:2007:MVH,%
		Turon:2013:URH%
		}.
\NAMECITE{highly}{%
		Vafeiadis:2006:PCH%
		}.
\NAMECITE{highly-concurrent}{%
		Vafeiadis:2006:PCH%
		}.
\NAMECITE{Hints}{%
		Hoare:1973:HPLa,%
		Hoare:1973:HPLb,%
		Hoare:1973:HPLc,%
		Hoare:1974:HPL,%
		Hoare:1975:HDP,%
		Hoare:1976:HDP%
		}.
\NAMECITE{Historic}{%
		Broy:2001:PTC,%
		Jones:2011:DHC%
		}.
\NAMECITE{histories}{%
		Borgstrom:2011:RSH%
		}.
\NAMECITE{Hoare}{%
		Anonymous:1987:BRC,%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Black:2012:PSD,%
		Brockhaus:1973:BRC,%
		Horning:1989:BRE,%
		Pritchard:1979:CPJ,%
		Ribeiro:2019:UTP,%
		Anonymous:2007:DIPa,%
		Anonymous:2007:DIPb,%
		Anonymous:20xx:THE,%
		Apt:1981:TYH,%
		Apt:2019:FYH,%
		Apt:2021:ASI,%
		Arthan:2009:GFS,%
		Arthan:2013:HLL,%
		Ashcroft:1976:RPP,%
		Baer:1965:RPP,%
		Barthe:2012:PRH,%
		Bergstra:1982:ECH,%
		Bergstra:1982:SNS,%
		Bergstra:1982:TTA,%
		Bergstra:1983:HLP,%
		Bergstra:1984:ASP,%
		Bergstra:1984:HLP,%
		Bergstra:1984:PPI,%
		Bernot:2019:GMH,%
		Bloom:1991:FHL,%
		Borgstrom:2011:RSH,%
		Chajed:2017:CFS,%
		Cherniavsky:1979:CCH,%
		Chisholm:1989:ARP,%
		Chlipala:2013:BSP,%
		Clarke:1979:PLC,%
		Clarke:1983:EAH,%
		Coenen:1995:HLV,%
		Cohen:2000:NCP,%
		Dale:1994:CST,%
		Damm:1983:SRH,%
		Dasgupta:1984:UHL,%
		Davies:2000:MPC,%
		Daylight:2012:THM,%
		DeBoer:1997:HSC,%
		Delbianco:2013:HSR,%
		Dijkstra:1970:LPC,%
		Dijkstra:1974:LCR,%
		Dijkstra:1975:VTO,%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa,%
		Dijkstra:1982:PTP,%
		Dijkstra:1982:VTO,%
		Dijkstra:1989:ETH,%
		Dijkstra:1999:FWT,%
		Dijkstra:20xx:ERC,%
		Engelhardt:1996:SSS,%
		Feng:2021:QHL,%
		Flannery:1990:HSP,%
		Fouz:2012:SAQ,%
		Frana:2002:ICA,%
		Gardner:2008:LHR,%
		Greif:1981:SSW,%
		Groote:1994:PAG,%
		Grubel:1996:ADT,%
		Grubel:1998:HSA,%
		Hartog:2002:VPP,%
		Hoare:1980:HP,%
		Hoare:1982:VTO,%
		Hoofman:1991:WEM,%
		Hooman:1992:CVR,%
		Hooman:1994:EHL,%
		Hortala-Gonzalez:1989:HLN,%
		Huisman:2000:JPV,%
		Jacobs:2015:DHM,%
		Jones:2010:RWC,%
		Jones:2021:LTH,%
		Jones:2021:TPL,%
		Kirkerud:1982:CHC,%
		Kirschenhofer:1998:CHF,%
		Kleymann:1999:HLA,%
		Knijnenburg:1992:CIP,%
		Kojima:2017:HLG,%
		Kozen:2000:HLK,%
		Kral:1966:NHP,%
		Lamport:1980:HLC,%
		Lamport:1984:HLC,%
		Lloyd:1974:BRS,%
		Mamouras:2016:HLD,%
		Mancini:1988:HLD,%
		Nanevski:2006:PSH,%
		Nanevski:2008:HTT,%
		Neuhold:1977:UHM,%
		Nielson:1987:HLP,%
		Nipkow:2002:HLR,%
		ODonnell:1982:CFH,%
		Olderog:1981:SCH,%
		Olderog:1983:CHL%
		}.
\NAMECITE{{Hoare}}{%
		Poskitt:2012:HSV,%
		Pratt:1976:SCF,%
		Prodinger:1995:MQH,%
		Reus:2001:HCV,%
		RodriguezArtalejo:1985:SQA,%
		Roscoe:1994:CME,%
		Saabas:2007:CNS,%
		Sergey:2016:HSS,%
		Shustek:2009:IIC,%
		Simauti:1967:CCD,%
		Sokolowski:1987:SHL,%
		Sousa:2016:CHL,%
		Stirling:1988:GOG,%
		Sun:1996:TRH,%
		Szczepanska:1991:HLV,%
		Takaoka:1987:DRH,%
		Turon:2013:URH,%
		Wand:1976:NIR,%
		Wand:1978:NIR,%
		Woodcock:2021:HHU,%
		Xu:2016:CHL,%
		Ying:2011:FHL,%
		deBoer:2002:HLD,%
		deBoer:2021:CCR,%
		denHartog:2008:TMC,%
		vonHenke:1985:RHS,%
		vonOheimb:2001:HLJ,%
		vonOheimb:2002:HLN%
		}.
\NAMECITE{{Hoare}-calculi}{%
		Kirkerud:1982:CHC%
		}.
\NAMECITE{{Hoare}-like}{%
		Bergstra:1982:SNS,%
		Nielson:1987:HLP,%
		Olderog:1981:SCH,%
		Szczepanska:1991:HLV%
		}.
\NAMECITE{{Hoare}-Logic}{%
		Damm:1983:SRH%
		}.
\NAMECITE{{Hoare}-Style}{%
		Poskitt:2012:HSV,%
		DeBoer:1997:HSC,%
		Delbianco:2013:HSR,%
		Sergey:2016:HSS,%
		Turon:2013:URH%
		}.
\NAMECITE{Hoares}{%
		Apt:1984:TYH%
		}.
\NAMECITE{Hoc}{%
		Wu:2019:USC%
		}.
\NAMECITE{{HOL}}{%
		vonOheimb:2001:HLJ%
		}.
\NAMECITE{holy}{%
		Hoare:2003:KTK%
		}.
\NAMECITE{honour}{%
		Davies:2000:MPC,%
		Roscoe:1994:CME%
		}.
\NAMECITE{horizons}{%
		Hoare:2004:EHDa,%
		Hoare:2004:EHDb%
		}.
\NAMECITE{horizontal}{%
		Dasgupta:1984:UHL%
		}.
\NAMECITE{Houston}{%
		IEEE:1976:ASF%
		}.
\NAMECITE{Hrsg}{%
		Brockhaus:1973:BRC%
		}.
\NAMECITE{Hybrid}{%
		Foster:2019:HRI%
		}.


\NAMECITE{ICCSW'13}{%
		Jones:2013:ICC%
		}.
\NAMECITE{idea}{%
		Fetzer:1988:PVV%
		}.
\NAMECITE{Ideal}{%
		Anonymous:2007:DIPa,%
		Anonymous:2007:DIPb,%
		Hoare:2007:IPC,%
		Hoare:2006:IVS%
		}.
\NAMECITE{Ideas}{%
		Lewis:2021:ICF%
		}.
\NAMECITE{If}{%
		Lewis:1997:BCI%
		}.
\NAMECITE{{IFIP}}{%
		Meyer:2008:VST%
		}.
\NAMECITE{Ignore}{%
		Welch:1997:LEI%
		}.
\NAMECITE{{II}}{%
		Apt:1984:TYH,%
		Bowen:1996:PIP,%
		Enslow:1975:ILRb,%
		Hoare:1986:WPb%
		}.
\NAMECITE{III}{%
		Hoare:2001:ETS,%
		Enslow:1975:ILRc%
		}.
\NAMECITE{Impact}{%
		Apt:2021:ASI%
		}.
\NAMECITE{imperative}{%
		Nanevski:2008:YDT%
		}.
\NAMECITE{Imperial}{%
		Jones:2013:ICC%
		}.
\NAMECITE{Implementation}{%
		Enslow:1975:ILRa,%
		Enslow:1975:ILRb,%
		Enslow:1975:ILRc,%
		Ryder:1999:PAS%
		}.
\NAMECITE{implementations}{%
		Hoare:1982:SPI%
		}.
\NAMECITE{Impossible}{%
		Clarke:1979:PLC%
		}.
\NAMECITE{Imprecise}{%
		PeytonJones:1999:SIE,%
		Jones:1999:SIE%
		}.
\NAMECITE{Inadequacy}{%
		Blass:2001:ICL%
		}.
\NAMECITE{inaugural}{%
		Hoare:1971:CSI,%
		Hoare:1986:MPI%
		}.
\NAMECITE{inclusion}{%
		Bergstra:1984:PPI%
		}.
\NAMECITE{Incompleteness}{%
		Wand:1978:NIR,%
		Wand:1976:NIR%
		}.
\NAMECITE{Incomputability}{%
		Hoare:1972:I%
		}.
\NAMECITE{increasing}{%
		Hoare:1990:FPI%
		}.
\NAMECITE{independent}{%
		vanAmmers:1998:PCC%
		}.
\NAMECITE{Index}{%
		Jones:2021:ABI%
		}.
\NAMECITE{indirect}{%
		Hoare:1965:NIA%
		}.
\NAMECITE{inductive}{%
		Chisholm:1989:ARP%
		}.
\NAMECITE{Industrial}{%
		Bottaci:2010:TAI%
		}.
\NAMECITE{Inform}{%
		Pettersson:1991:LEC,%
		Santini:2005:WSI,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{{Infotech}}{%
		Bates:1976:SPI%
		}.
\NAMECITE{initiative}{%
		Hoare:2009:VSI,%
		Hoare:2021:VSI%
		}.
\NAMECITE{{Inmos}}{%
		May:2021:COI%
		}.
\NAMECITE{Inner}{%
		Butterfield:2019:IOA%
		}.
\NAMECITE{input}{%
		Hoare:1963:EAI%
		}.
\NAMECITE{input/output}{%
		Hoare:1963:EAI%
		}.
\NAMECITE{inputs}{%
		Xu:2016:CHL%
		}.
\NAMECITE{Insecurities}{%
		Welsh:1977:AIP%
		}.
\NAMECITE{Institute}{%
		Broy:1996:DPD%
		}.
\NAMECITE{Intelligent}{%
		Beckert:2006:ISF%
		}.
\NAMECITE{Intensive}{%
		Broy:2005:ETS%
		}.
\NAMECITE{interesting}{%
		Hoare:2000:SLI%
		}.
\NAMECITE{interface}{%
		Moller:2015:EIM%
		}.
\NAMECITE{interfaces}{%
		Bauer:1976:LHI%
		}.
\NAMECITE{International}{%
		Abadi:2005:CCT,%
		Anonymous:1987:BRC,%
		Berghammer:2009:RKA,%
		Bjorner:1990:VVZ,%
		Bottaci:2010:TAI,%
		Gibbons:2012:MPC,%
		Haddad:2012:ATP,%
		Hofner:2014:RAM,%
		Horning:1989:BRE,%
		IEEE:2002:AIC,%
		Kapur:1992:ADC,%
		Ribeiro:2019:UTP,%
		Rishe:1990:PIC,%
		Wolff:2013:UTP,%
		Bauer:1976:LHI,%
		Ershov:1974:IST%
		}.
\NAMECITE{Interpretation}{%
		Knijnenburg:1992:CIP%
		}.
\NAMECITE{Interpreting}{%
		Milner:1990:IOC%
		}.
\NAMECITE{Interview}{%
		Frana:2002:ICA,%
		Jones:2021:AI,%
		Shustek:2009:IIC,%
		Black:2012:PSD%
		}.
\NAMECITE{Introduction}{%
		Hoare:1977:I,%
		Shankar:1993:IAR%
		}.
\NAMECITE{introductory}{%
		Hoare:1976:SPI%
		}.
\NAMECITE{invariance}{%
		Pettersson:1991:LEC%
		}.
\NAMECITE{invariant}{%
		Pettersson:1991:LEC,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{invariants}{%
		Blass:2001:ICL%
		}.
\NAMECITE{Invention}{%
		Priestley:2010:SOM%
		}.
\NAMECITE{invited}{%
		Abdallah:2005:CSP,%
		Hoare:2000:LC,%
		Hoare:2006:IVS%
		}.
\NAMECITE{Ireland}{%
		Hoare:1972:OST%
		}.
\NAMECITE{{Iris}}{%
		Hoare:2004:VIF%
		}.
\NAMECITE{Isabelle}{%
		Foster:2019:HRI,%
		vonOheimb:2001:HLJ%
		}.
\NAMECITE{{Isabelle/HOL}}{%
		vonOheimb:2001:HLJ%
		}.
\NAMECITE{Isabelle/{UTP}}{%
		Foster:2019:HRI%
		}.
\NAMECITE{ISBN}{%
		Horning:1989:BRE%
		}.
\NAMECITE{Isn't}{%
		Olsen:1997:LWJ%
		}.
\NAMECITE{Issue}{%
		Hoare:2021:PSI,%
		Hoare:2009:PSI%
		}.
\NAMECITE{Item}{%
		Dijkstra:1970:NIM%
		}.
\NAMECITE{Iteration}{%
		Bloom:1991:FHL%
		}.


\NAMECITE{J}{%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Lloyd:1974:BRS,%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{{J.}}{%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa%
		}.
\NAMECITE{{Jackson}}{%
		Hoare:2010:MJD%
		}.
\NAMECITE{{Java}}{%
		Huisman:2000:JPV,%
		Lewis:1997:BCI,%
		Olsen:1997:LWJ,%
		Reus:2001:HCV,%
		Struble:1997:LDJ,%
		vonOheimb:2001:HLJ%
		}.
\NAMECITE{{Jifeng}}{%
		Liu:2013:TPF%
		}.
\NAMECITE{{Johan}}{%
		Owe:2004:OOF%
		}.
\NAMECITE{Jones}{%
		Horning:1989:BRE%
		}.
\NAMECITE{{Journal}}{%
		Hoare:2007:IPC%
		}.
\NAMECITE{{JSD}}{%
		Sridhar:1985:JEC%
		}.
\NAMECITE{July}{%
		Abdallah:2005:CSP,%
		Bauer:1976:LHI,%
		Broy:1996:DPD,%
		Hoare:2001:ETS,%
		IEEE:1988:ASL,%
		Dijkstra:1974:LCR%
		}.
\NAMECITE{Jumps}{%
		Ashcroft:1976:RPP,%
		Clint:1972:PPJ%
		}.
\NAMECITE{June}{%
		Broy:2001:PTC,%
		Gibbons:2012:MPC,%
		Haddad:2012:ATP,%
		Kapur:1992:ADC,%
		Lenzerini:2008:PTS%
		}.


\NAMECITE{{{{KDF9}}}}{%
		Hoare:1964:BRA%
		}.
\NAMECITE{Kernels}{%
		Kojima:2017:HLG%
		}.
\NAMECITE{Key}{%
		Hoare:1997:UTC%
		}.
\NAMECITE{Keynote}{%
		Hoare:1990:LMM,%
		Hoare:1990:RAPb,%
		Hoare:1991:TCC,%
		Hoare:1978:SEK%
		}.
\NAMECITE{Kiel}{%
		Bjorner:1990:VVZ%
		}.
\NAMECITE{King}{%
		Hoare:2003:KTK%
		}.
\NAMECITE{Kingdom}{%
		Horning:1989:BRE,%
		Jones:2013:ICC%
		}.
\NAMECITE{Kleene}{%
		Berghammer:2009:RKA,%
		Berghammer:2009:RKA,%
		Hoare:2009:CKA,%
		Hoare:2009:FCK,%
		Hoare:2011:CKA,%
		Hoare:2014:DCK,%
		Hoare:2016:DCK,%
		Kozen:2000:HLK%
		}.
\NAMECITE{knights}{%
		Hoare:2003:KTK%
		}.
\NAMECITE{{Knuth}}{%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa%
		}.


\NAMECITE{Language}{%
		Cherniavsky:1979:CCH,%
		Clarke:1979:PLC,%
		Damm:1983:SRH,%
		Enslow:1975:ILRb,%
		Hoare:1972:ADP,%
		Hoare:1973:ADP,%
		Hoare:1973:HPLa,%
		Hoare:1973:HPLb,%
		Hoare:1973:HPLc,%
		Hoare:1974:ACA,%
		Hoare:2005:TSO,%
		Kernighan:1984:WPM,%
		Ryder:1999:PAS,%
		Hoare:1972:PBP,%
		Hoare:1974:ADP,%
		Hoare:1974:HPL,%
		Hoare:1975:HDP,%
		Hoare:1976:HDP,%
		Hoare:1989:VPL,%
		Hoare:1990:AAV,%
		Kernighan:1981:WPM,%
		Stirling:1988:GOG,%
		Szczepanska:1991:HLV,%
		Bauer:1976:LHI,%
		Hoare:1996:PPA%
		}.
\NAMECITE{Languages}{%
		Enslow:1975:ILRa,%
		Enslow:1975:ILRb,%
		Enslow:1975:ILRc,%
		Feuer:1984:CAP,%
		Hoare:1974:CCF,%
		Hoare:1985:MLP,%
		Bergstra:1984:HLP,%
		He:1990:CSP,%
		Hoare:1968:LL,%
		Hoare:1970:BRC,%
		Hoare:1973:HLP,%
		Hoare:1976:HCP,%
		Hoare:1990:CSP,%
		Saabas:2007:CNS,%
		Hoare:1970:BRC%
		}.
\NAMECITE{{LASER}}{%
		Muller:2010:ALS%
		}.
\NAMECITE{{Lauer}}{%
		Greif:1981:SSW%
		}.
\NAMECITE{law}{%
		Hoare:1973:GCL,%
		Hoare:2011:LEL%
		}.
\NAMECITE{Laws}{%
		Hoare:1987:CLP,%
		Hoare:1987:LP,%
		Hoare:1992:LP,%
		Hoare:1993:MPM,%
		Hoare:2012:LPU,%
		Hoare:2013:GML,%
		Hoare:2013:LPC,%
		Hoare:2014:LCP,%
		Roscoe:1986:LOP,%
		Hoare:2014:LPU,%
		Roscoe:1988:LOP%
		}.
\NAMECITE{{LCF}}{%
		Sokolowski:1987:SHL%
		}.
\NAMECITE{Learning}{%
		Hoare:2002:LLU%
		}.
\NAMECITE{lecture}{%
		Hoare:1971:CSI,%
		Hoare:1986:MPI,%
		Hoare:2007:IPC,%
		Hoare:2021:ATA%
		}.
\NAMECITE{lectures}{%
		Muller:2010:ALS,%
		Ashenhurst:1987:ATA%
		}.
\NAMECITE{Legacy}{%
		Apt:2022:EWD,%
		Hoare:2000:LC,%
		Hoare:2001:L%
		}.
\NAMECITE{Let}{%
		Hoare:1990:LMM%
		}.
\NAMECITE{Lett}{%
		Pettersson:1991:LEC,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{Letter}{%
		Dijkstra:1970:LPC,%
		Hoare:1966:LWM,%
		Hoare:1968:LVW,%
		Hoare:1982:VTO,%
		Pettersson:1991:LEC,%
		Dijkstra:1974:LCR,%
		Dijkstra:1975:VTO,%
		Dijkstra:1982:VTO%
		}.
\NAMECITE{Letters}{%
		Gozum:1997:LWC,%
		McReynolds:1997:LBS,%
		Olsen:1997:LWJ,%
		Struble:1997:LDJ,%
		Welch:1997:LEI%
		}.
\NAMECITE{level}{%
		Hoare:1968:DST,%
		Hoare:1973:HLP,%
		Hoare:1990:AAV,%
		Saabas:2007:CNS%
		}.
\NAMECITE{Life}{%
		Apt:2022:EWD,%
		Jones:2021:TPL,%
		Hoare:2000:SLI%
		}.
\NAMECITE{Like}{%
		Hartog:2002:VPP,%
		Bergstra:1982:SNS,%
		Hoare:2004:YWT,%
		LeGuyadec:1996:SLP,%
		Nielson:1987:HLP,%
		Olderog:1981:SCH,%
		Olderog:1984:CPP,%
		Szczepanska:1991:HLV,%
		Olderog:1983:CHL%
		}.
\NAMECITE{Limitations}{%
		Hoare:1968:LL%
		}.
\NAMECITE{linear}{%
		Arthan:2013:HLL%
		}.
\NAMECITE{linearisable}{%
		Vafeiadis:2006:PCH%
		}.
\NAMECITE{linearizable}{%
		Sergey:2016:HSS%
		}.
\NAMECITE{Linking}{%
		He:1997:LTP,%
		He:1999:LTP,%
		He:2005:LTC%
		}.
\NAMECITE{List}{%
		Jones:2021:LTH,%
		vanDiepen:1986:PDT%
		}.
\NAMECITE{List-Copying}{%
		vanDiepen:1986:PDT%
		}.
\NAMECITE{Local}{%
		Gardner:2008:LHR%
		}.
\NAMECITE{locality}{%
		Hoare:2011:LEL%
		}.
\NAMECITE{Logic}{%
		Apt:1981:TYH,%
		Apt:2021:ASI,%
		Banerjee:2022:RPL,%
		Bergstra:1982:TTA,%
		Bergstra:1984:ASP,%
		Bloom:1991:FHL,%
		Broy:2003:MAL,%
		Damm:1983:SRH,%
		Feng:2021:QHL,%
		Hartog:2002:VPP,%
		Hoare:1985:MLP,%
		Hoare:2008:SLS,%
		Hoare:2019:CST,%
		Huisman:2000:JPV,%
		IEEE:1988:ASL,%
		Kleymann:1999:HLA,%
		Knijnenburg:1992:CIP,%
		Kojima:2017:HLG,%
		Lamport:1980:HLC,%
		Lamport:1984:HLC,%
		Mamouras:2016:HLD,%
		Priestley:2010:SOM,%
		Sokolowski:1987:SHL,%
		deBoer:2021:CCR,%
		vonOheimb:2002:HLN,%
		Apt:1984:TYH,%
		Apt:2019:FYH,%
		Arthan:2013:HLL,%
		Becker:2010:LSM,%
		Bergstra:1982:ECH,%
		Bergstra:1982:SNS,%
		Bergstra:1983:HLP,%
		Bergstra:1984:HLP,%
		Bergstra:1984:PPI,%
		Bernot:2019:GMH,%
		Brotherston:2008:CPP,%
		Chajed:2017:CFS,%
		Chlipala:2013:BSP,%
		Coenen:1995:HLV,%
		Cohen:2000:NCP,%
		Dasgupta:1984:UHL,%
		Daylight:2012:THM,%
		Engelhardt:1996:SSS,%
		Groote:1994:PAG,%
		Hoare:1988:PCC,%
		Hoare:1996:LED,%
		Hoare:2001:UTL,%
		Hoare:2019:CSTa,%
		Hoofman:1991:WEM,%
		Hooman:1994:EHL,%
		Hortala-Gonzalez:1989:HLN,%
		Kozen:2000:HLK,%
		Mancini:1988:HLD,%
		Olderog:1983:CHL,%
		Pratt:1976:SCF,%
		RodriguezArtalejo:1985:SQA,%
		Saabas:2007:CNS,%
		Seres:1999:ALP,%
		Sousa:2016:CHL,%
		Stirling:1988:GOG,%
		Sun:1996:TRH,%
		Takaoka:1987:DRH,%
		Turon:2013:URH,%
		Wehrman:2009:GMS,%
		Xu:2016:CHL,%
		Ying:2011:FHL,%
		deBoer:2002:HLD,%
		denHartog:2008:TMC,%
		vonOheimb:2001:HLJ%
		}.
\NAMECITE{Logics}{%
		Barthe:2012:PRH,%
		Clarke:1983:EAH,%
		Nipkow:2002:HLR,%
		ODonnell:1982:CFH,%
		Arthan:2009:GFS%
		}.
\NAMECITE{London}{%
		Abdallah:2005:CSP,%
		Anonymous:1976:SSE,%
		Anonymous:1987:BRC,%
		Barron:1975:BRS,%
		Jones:2013:ICC%
		}.
\NAMECITE{Long}{%
		Butler:2005:TSL%
		}.
\NAMECITE{Long-Running}{%
		Butler:2005:TSL%
		}.
\NAMECITE{loop}{%
		Blass:2001:ICL%
		}.
\NAMECITE{love}{%
		Hoare:2002:LLU%
		}.
\NAMECITE{low}{%
		Saabas:2007:CNS%
		}.
\NAMECITE{low-level}{%
		Saabas:2007:CNS%
		}.


\NAMECITE{M}{%
		Hoare:1970:BRC%
		}.
\NAMECITE{{M.}}{%
		Ashcroft:1976:RPP%
		}.
\NAMECITE{M1}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA%
		}.
\NAMECITE{Machine}{%
		Hoare:1961:MSS,%
		Boyer:1992:ACP,%
		Hoare:2004:YWT%
		}.
\NAMECITE{Machines}{%
		Bazilevskii:1963:TMM,%
		Priestley:2010:SOM,%
		Baer:1965:RPP%
		}.
\NAMECITE{Madrid}{%
		Gibbons:2012:MPC%
		}.
\NAMECITE{mail}{%
		Hoare:1986:ASP,%
		Hoare:1987:DPM,%
		Hoare:1991:DPM%
		}.
\NAMECITE{make}{%
		Hoare:1990:LMM%
		}.
\NAMECITE{Making}{%
		Dijkstra:1982:MSMa,%
		Dijkstra:1977:MSM%
		}.
\NAMECITE{management}{%
		Hoare:1972:SSMa,%
		Hoare:1972:SSMb%
		}.
\NAMECITE{mandatory}{%
		Shaner:2007:MVH%
		}.
\NAMECITE{Manifesto}{%
		Hoare:2021:VSI,%
		Hoare:2009:VSI%
		}.
\NAMECITE{manipulation}{%
		Hoare:1968:SM%
		}.
\NAMECITE{manual}{%
		Spivey:1989:ZNR%
		}.
\NAMECITE{March}{%
		Hoare:2004:RMN,%
		Rishe:1990:PIC%
		}.
\NAMECITE{Marienstatt}{%
		Hofner:2014:RAM%
		}.
\NAMECITE{{Markov}}{%
		Grubel:1998:HSA%
		}.
\NAMECITE{Marktoberdorf}{%
		Bauer:1976:LHI,%
		Broy:1996:DPD,%
		Hoare:2001:ETS%
		}.
\NAMECITE{Massachusetts}{%
		ACM:1983:PFA%
		}.
\NAMECITE{Mathematical}{%
		Baer:1965:RPP,%
		Bazilevskii:1963:TMM,%
		Hoare:1985:MLP,%
		Hoare:1993:MPM,%
		Hoare:1996:MMC,%
		Daylight:2012:THM,%
		Hoare:1981:TMB%
		}.
\NAMECITE{Mathematics}{%
		Gibbons:2012:MPC,%
		Hoare:1986:MP,%
		Hoare:1993:MPM,%
		Hoare:1985:MP,%
		Hoare:1986:MPI%
		}.
\NAMECITE{Maths}{%
		Hoare:1986:MAS%
		}.
\NAMECITE{Matrix}{%
		Johnston:1975:MRE%
		}.
\NAMECITE{May}{%
		Hofner:2014:RAM,%
		Ryder:1999:PAS,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{means}{%
		Fokkinga:1987:CPS%
		}.
\NAMECITE{mechanically}{%
		Homeier:1995:MVV%
		}.
\NAMECITE{mechanism}{%
		Cocco:1982:MEH,%
		Szczepanska:1991:HLV%
		}.
\NAMECITE{Mechanized}{%
		Gordon:1992:MRH,%
		denHartog:2008:TMC%
		}.
\NAMECITE{Meeting}{%
		Hoare:1999:TPT,%
		Gordon:1992:MRH,%
		Hoare:1993:WSE%
		}.
\NAMECITE{members}{%
		Hoare:1966:LWM%
		}.
\NAMECITE{memoriam}{%
		Boyer:2002:MEW%
		}.
\NAMECITE{Memory}{%
		Manna:2010:TVE,%
		Owe:2004:OOF%
		}.
\NAMECITE{men}{%
		Hoare:1973:TMR%
		}.
\NAMECITE{menu}{%
		Enikeev:1987:MTC%
		}.
\NAMECITE{menu-dialog}{%
		Enikeev:1987:MTC%
		}.
\NAMECITE{Message}{%
		Hoare:2012:MT,%
		Hoare:2012:MTR,%
		Stoller:1995:VPU%
		}.
\NAMECITE{message-passing}{%
		Stoller:1995:VPU%
		}.
\NAMECITE{metaprogramming}{%
		Chlipala:2013:BSP%
		}.
\NAMECITE{Method}{%
		Hoare:1961:MSS,%
		Johnston:1975:MRE,%
		Neuhold:1977:UHM,%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{Methods}{%
		Beckert:2006:ISF,%
		Berghammer:2009:RKA,%
		Hoare:1987:OSF,%
		Hofner:2014:RAM,%
		Liu:2013:TPF,%
		Owe:2004:OOF,%
		Welch:1997:LEI,%
		vonOheimb:2002:HLN,%
		Bjorner:1990:VVZ,%
		Chisholm:1989:ARP,%
		Hoare:1989:FMC,%
		Shaner:2007:MVH%
		}.
\NAMECITE{Miami}{%
		Rishe:1990:PIC%
		}.
\NAMECITE{Michael}{%
		Hoare:2004:RMN,%
		Hoare:2010:MJD%
		}.
\NAMECITE{Microcomputer}{%
		Ekanadham:1981:MN%
		}.
\NAMECITE{microprocessor}{%
		Boyer:1992:ACP,%
		Boyer:1996:APO%
		}.
\NAMECITE{microprograms}{%
		Dasgupta:1984:UHL%
		}.
\NAMECITE{Microsoft}{%
		Davies:2000:MPC%
		}.
\NAMECITE{Middle}{%
		Hoare:1999:TPT%
		}.
\NAMECITE{{Millennial}}{%
		Davies:2000:MPC%
		}.
\NAMECITE{{Mind}}{%
		Roscoe:1994:CME%
		}.
\NAMECITE{Minority}{%
		Dijkstra:1970:NIM,%
		Woodger:1969:MRA%
		}.
\NAMECITE{Mobile}{%
		Wu:2019:USC%
		}.
\NAMECITE{modality}{%
		Winskel:1985:PM%
		}.
\NAMECITE{Model}{%
		Enikeev:1987:MTC,%
		Hoare:1999:TMPb,%
		Gritzner:1996:RAM,%
		Hehner:1983:MCM,%
		Hoare:1980:MCSa,%
		Hoare:1980:MCSb,%
		Hoare:1981:MCS,%
		Hoare:1990:MSS,%
		Hoare:1999:TMPa,%
		Moller:2015:EIM,%
		Nguyen:1986:GOMa,%
		Shaner:2007:MVH,%
		Xu:2016:CHL,%
		Zhou:1992:MSS%
		}.
\NAMECITE{modelling}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{Models}{%
		Broy:2003:MAL,%
		Hoare:1993:AMb,%
		Hoare:2012:NMC,%
		Hoare:2013:GML,%
		Reus:2001:HCV,%
		Hoare:1990:LMM,%
		Hoare:1992:AM,%
		Hoare:1993:AMa,%
		Hoare:1995:AM,%
		Hoare:1996:AM,%
		Hoare:1996:MMC,%
		Hoare:2011:UMD,%
		Hoofman:1991:WEM,%
		Wehrman:2009:GMS%
		}.
\NAMECITE{modern}{%
		Hoare:2002:AMS%
		}.
\NAMECITE{modified}{%
		Bernot:2019:GMH%
		}.
\NAMECITE{modifying}{%
		Becker:2010:LSM,%
		Cai:2007:CSM%
		}.
\NAMECITE{Modular}{%
		Shaner:2007:MVH%
		}.
\NAMECITE{Monadic}{%
		Mamouras:2016:HLD,%
		Jacobs:2015:DHM%
		}.
\NAMECITE{monads}{%
		Jacobs:2015:DHM%
		}.
\NAMECITE{Monitor}{%
		Welch:1997:LEI%
		}.
\NAMECITE{Monitors}{%
		Hoare:1974:MOS,%
		Hoare:2002:MOS%
		}.
\NAMECITE{{MOS}}{%
		Hoare:1988:PCC,%
		Hoare:1990:TDC,%
		Hoare:1991:TDCa,%
		Hoare:1991:TDCb%
		}.
\NAMECITE{MPC}{%
		Gibbons:2012:MPC%
		}.
\NAMECITE{MR}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{{Multiple}}{%
		Prodinger:1995:MQH%
		}.
\NAMECITE{Multiprocessors}{%
		Elliott:1989:SAM%
		}.
\NAMECITE{mutual}{%
		Page:1989:SME%
		}.
\NAMECITE{My}{%
		Kernighan:1984:WPM,%
		Kernighan:1981:WPM%
		}.


\NAMECITE{Name}{%
		Cipra:2000:BCE%
		}.
\NAMECITE{{NanoJava}}{%
		vonOheimb:2002:HLN%
		}.
\NAMECITE{{NATO}}{%
		Broy:1996:DPD,%
		Hoare:2001:ETS%
		}.
\NAMECITE{natural}{%
		Bergstra:1982:SNS,%
		Saabas:2007:CNS%
		}.
\NAMECITE{Needham}{%
		Hoare:2004:RMN,%
		Herbert:2004:CST%
		}.
\NAMECITE{Net}{%
		Hoare:2012:NMC%
		}.
\NAMECITE{Nets}{%
		Haddad:2012:ATP%
		}.
\NAMECITE{network}{%
		Hoare:1985:SSN,%
		Morgan:1985:SSN%
		}.
\NAMECITE{Networks}{%
		Ekanadham:1981:MN,%
		Wu:2019:USC,%
		deBoer:2002:HLD%
		}.
\NAMECITE{{Neuhold}}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{Newnes}{%
		Hoare:1970:BRC%
		}.
\NAMECITE{Newnes-Butterworths}{%
		Hoare:1970:BRC%
		}.
\NAMECITE{News}{%
		Dijkstra:1970:NIM%
		}.
\NAMECITE{No}{%
		Barron:1975:BRS,%
		Hoare:1987:CLP,%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{non}{%
		Hoare:1980:TND,%
		Sergey:2016:HSS%
		}.
\NAMECITE{non-determinism}{%
		Hoare:1980:TND%
		}.
\NAMECITE{non-linearizable}{%
		Sergey:2016:HSS%
		}.
\NAMECITE{Nondeterminism}{%
		Apt:1984:TYH,%
		Nipkow:2002:HLR,%
		Francez:1978:SNC,%
		Francez:1979:SNC,%
		Kennaway:1980:TN%
		}.
\NAMECITE{Nondeterministic}{%
		Mamouras:2016:HLD,%
		Hortala-Gonzalez:1989:HLN%
		}.
\NAMECITE{nonstandard}{%
		Hortala-Gonzalez:1989:HLN%
		}.
\NAMECITE{Normal}{%
		Hoare:1993:NFA%
		}.
\NAMECITE{Northern}{%
		Hoare:1972:OST%
		}.
\NAMECITE{notation}{%
		Spivey:1989:ZNR%
		}.
\NAMECITE{Note}{%
		Hoare:1972:NS,%
		Kral:1966:NHP,%
		Cohen:2000:NCP,%
		Hoare:1965:NIA%
		}.
\NAMECITE{Notes}{%
		Dijkstra:1972:NSP,%
		Hoare:1972:NDS,%
		Hoare:1983:NCS,%
		Hoare:1985:NCS,%
		Hoare:1986:NCS,%
		Hoare:1989:NAC%
		}.
\NAMECITE{notion}{%
		Olderog:1983:NER%
		}.
\NAMECITE{novelties}{%
		Hoare:1985:CNP%
		}.
\NAMECITE{November}{%
		Berghammer:2009:RKA%
		}.
\NAMECITE{Novosibirsk}{%
		Ershov:1974:IST%
		}.
\NAMECITE{NY}{%
		Kapur:1992:ADC%
		}.
\NAMECITE{nye}{%
		Khoar:1989:CVC%
		}.


\NAMECITE{O}{%
		Barron:1975:BRS,%
		Lloyd:1974:BRS%
		}.
\NAMECITE{{O.}}{%
		Barth:1974:BRJ%
		}.
\NAMECITE{O.-J}{%
		Barron:1975:BRS,%
		Lloyd:1974:BRS%
		}.
\NAMECITE{Object}{%
		Hoare:2012:NMC,%
		Owe:2004:OOF,%
		Boyer:1996:APO,%
		Nguyen:1986:GOMa%
		}.
\NAMECITE{Object-Orientation}{%
		Owe:2004:OOF%
		}.
\NAMECITE{objectives}{%
		Hoare:1972:OSTb%
		}.
\NAMECITE{Objects}{%
		Hoare:1999:TMPb,%
		Hoare:1999:TMPa,%
		Sergey:2016:HSS,%
		Vafeiadis:2006:PCH%
		}.
\NAMECITE{Obtain}{%
		Clarke:1979:PLC%
		}.
\NAMECITE{occam}{%
		Hoare:1991:TOP,%
		May:2021:COI,%
		Roscoe:1986:LOP,%
		Roscoe:1988:LOP%
		}.
\NAMECITE{Occasion}{%
		Jones:2011:DHC,%
		Liu:2013:TPF,%
		Abdallah:2005:CSP,%
		Dijkstra:1982:PTP,%
		Ribeiro:2019:UTP%
		}.
\NAMECITE{{OCL}}{%
		Reus:2001:HCV%
		}.
\NAMECITE{{OCL}-Constrained}{%
		Reus:2001:HCV%
		}.
\NAMECITE{October}{%
		Gordon:1992:MRH,%
		Hoare:1986:MPI,%
		IEEE:1976:ASF,%
		Meyer:2008:VST,%
		Ribeiro:2019:UTP%
		}.
\NAMECITE{Oh}{%
		Weiss:1988:BOP%
		}.
\NAMECITE{Old}{%
		Hoare:1981:EOC,%
		Hoare:1987:EOC%
		}.
\NAMECITE{{Ole}}{%
		Owe:2004:OOF%
		}.
\NAMECITE{{Ole-Johan}}{%
		Owe:2004:OOF%
		}.
\NAMECITE{one}{%
		Milner:1990:IOC%
		}.
\NAMECITE{Online}{%
		Gray:2021:OR%
		}.
\NAMECITE{Open}{%
		Hoare:1982:VTO,%
		Dijkstra:1975:VTO,%
		Dijkstra:1982:VTO%
		}.
\NAMECITE{Operating}{%
		Brockhaus:1973:BRC,%
		Hoare:1972:OSTb,%
		Hoare:1974:MOS,%
		Hoare:1982:SOS,%
		Hoare:2002:MOS,%
		Hoare:1976:SOS,%
		Hoare:1972:OST%
		}.
\NAMECITE{Operational}{%
		Aichernig:2019:TPA,%
		Hoare:1994:ACO,%
		vanStaden:2013:AUO,%
		He:1993:AOS,%
		Hoare:1997:ADO,%
		Hoare:2000:ADO,%
		Ridge:2009:VDS%
		}.
\NAMECITE{Operations}{%
		Priestley:2010:SOM%
		}.
\NAMECITE{optimisation}{%
		Jones:2001:PRR%
		}.
\NAMECITE{Optimization}{%
		Hoare:1974:OSS%
		}.
\NAMECITE{Orchestration}{%
		Hoare:2005:TSO%
		}.
\NAMECITE{order}{%
		Makowsky:1989:WSO,%
		Martin:1991:PAO,%
		Naumann:1995:PTH,%
		Shaner:2007:MVH,%
		Turon:2013:URH%
		}.
\NAMECITE{ordered}{%
		Stoller:1995:VPU%
		}.
\NAMECITE{Ordering}{%
		Dijkstra:1971:HOS%
		}.
\NAMECITE{Orientation}{%
		Owe:2004:OOF%
		}.
\NAMECITE{Oriented}{%
		Olderog:1986:SOS,%
		Olderog:1983:SOS%
		}.
\NAMECITE{Origin}{%
		BrinchHansen:2002:OCP%
		}.
\NAMECITE{Original}{%
		Broy:2001:PTC%
		}.
\NAMECITE{our}{%
		Feijen:1990:BOB%
		}.
\NAMECITE{Outer}{%
		Butterfield:2019:IOA%
		}.
\NAMECITE{output}{%
		Hoare:1963:EAI%
		}.
\NAMECITE{Overview}{%
		Hoare:1987:OSF,%
		Kapur:1994:OTP%
		}.
\NAMECITE{{Owicki}}{%
		Stirling:1988:GOG%
		}.
\NAMECITE{Oxford}{%
		Davies:2000:MPC,%
		IEEE:2002:AIC,%
		Hoare:1986:MPI,%
		Sufrin:2021:TBO%
		}.


\NAMECITE{Pacific}{%
		IEEE:2000:PSA%
		}.
\NAMECITE{pages}{%
		Barron:1975:BRS,%
		Anonymous:1987:BRC%
		}.
\NAMECITE{paging}{%
		Hoare:1973:SPS%
		}.
\NAMECITE{Paper}{%
		Greif:1981:SSW,%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{Papers}{%
		Lewis:2021:ICF,%
		Meyer:2008:VST,%
		Anonymous:1976:SSE,%
		Wolff:2013:UTP,%
		Abdallah:2005:CSP%
		}.
\NAMECITE{parable}{%
		Hoare:1974:SDP%
		}.
\NAMECITE{Parallel}{%
		Hoare:1972:TTP,%
		Hoare:1975:PPA,%
		Hoare:1976:PPA,%
		Hoare:1993:PPT,%
		Hoare:1997:UTPb,%
		Hoare:2002:TTP,%
		Hoare:1980:SPP,%
		LeGuyadec:1996:SLP,%
		Rishe:1990:PIC%
		}.
\NAMECITE{parameters}{%
		Hoare:1971:PPA%
		}.
\NAMECITE{{PARBASE}}{%
		Rishe:1990:PIC%
		}.
\NAMECITE{{PARBASE-90}}{%
		Rishe:1990:PIC%
		}.
\NAMECITE{Paris}{%
		Wolff:2013:UTP%
		}.
\NAMECITE{PART}{%
		Bottaci:2010:TAI,%
		Hoare:1972:SSMa,%
		Hoare:1972:SSMb,%
		Anonymous:1976:SSE,%
		Apt:1981:TYH%
		}.
\NAMECITE{Partial}{%
		Hoare:1981:PCC,%
		Hoare:1988:PCC,%
		Knijnenburg:1992:CIP,%
		Zhou:1981:PCC%
		}.
\NAMECITE{{Partition}}{%
		Hoare:1961:AP%
		}.
\NAMECITE{{PASCAL}}{%
		Hoare:1972:ADP,%
		Hoare:1974:ADP,%
		Olderog:1984:CPP,%
		Feuer:1984:CAP,%
		Hoare:1973:ADP,%
		Kernighan:1981:WPM,%
		Kernighan:1984:WPM,%
		Olderog:1983:CHL,%
		Welsh:1977:AIP,%
		Hoare:1974:ACA%
		}.
\NAMECITE{{PASCAL}-like}{%
		Olderog:1984:CPP,%
		Olderog:1983:CHL%
		}.
\NAMECITE{pass}{%
		Hoare:1966:SPC%
		}.
\NAMECITE{passing}{%
		Stoller:1995:VPU%
		}.
\NAMECITE{{Peano}}{%
		Bergstra:1983:HLP%
		}.
\NAMECITE{peeled}{%
		Hoare:2004:VIF%
		}.
\NAMECITE{Perrot}{%
		Brockhaus:1973:BRC%
		}.
\NAMECITE{Personal}{%
		Dijkstra:1982:SWC,%
		Hoare:1991:TOP,%
		Hoare:2002:APP,%
		Hoare:2003:APP,%
		Hoare:1996:UTP%
		}.
\NAMECITE{Perspective}{%
		Aichernig:2019:TPA,%
		Dijkstra:1982:SWC,%
		Hoare:2002:APP,%
		Hoare:2003:APP,%
		JaJa:2000:PQ%
		}.
\NAMECITE{perspectives}{%
		Davies:2000:MPC%
		}.
\NAMECITE{Peter}{%
		Hoare:1970:BRC%
		}.
\NAMECITE{Petri}{%
		Haddad:2012:ATP%
		}.
\NAMECITE{Physical}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{pictures}{%
		Dijkstra:1999:FWT%
		}.
\NAMECITE{Pioneers}{%
		Broy:2001:PTC,%
		Broy:2002:SPC,%
		Weiss:1988:BOP,%
		Broy:2001:PTC%
		}.
\NAMECITE{{PL}}{%
		Hoare:1966:P%
		}.
\NAMECITE{{PL/I}}{%
		Hoare:1966:P%
		}.
\NAMECITE{Playing}{%
		Jones:2001:PRR%
		}.
\NAMECITE{PLDI}{%
		Ryder:1999:PAS%
		}.
\NAMECITE{{Pnueli}}{%
		Manna:2010:TVE%
		}.
\NAMECITE{PODS'08}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{Pointers}{%
		Hoare:1999:TMPb,%
		Hoare:1999:TMPa,%
		Ni:2006:CAP,%
		Thielecke:2006:FRA%
		}.
\NAMECITE{points}{%
		Hoare:1990:FPI%
		}.
\NAMECITE{policies}{%
		Becker:2010:LSM%
		}.
\NAMECITE{Polymorphism}{%
		Nanevski:2006:PSH,%
		Nanevski:2008:HTT%
		}.
\NAMECITE{Port}{%
		Silberschatz:1981:PDC%
		}.
\NAMECITE{Porto}{%
		Ribeiro:2019:UTP%
		}.
\NAMECITE{Portugal}{%
		Ribeiro:2019:UTP%
		}.
\NAMECITE{posledovatel\cprime}{%
		Khoar:1989:CVC%
		}.
\NAMECITE{possess}{%
		Bergstra:1982:SNS%
		}.
\NAMECITE{possible}{%
		Tennent:1991:CPW%
		}.
\NAMECITE{possible-world}{%
		Tennent:1991:CPW%
		}.
\NAMECITE{power}{%
		Flannery:1990:HSP%
		}.
\NAMECITE{powerdomains}{%
		Winskel:1985:PM%
		}.
\NAMECITE{pp}{%
		Pettersson:1991:LEC,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{Practical}{%
		Brookes:2021:CPP,%
		Shapiro:2006:PPC,%
		Hoare:1970:BRC,%
		Jones:2001:PRR%
		}.
\NAMECITE{Practice}{%
		Bottaci:2010:TAI,%
		Hoare:2002:APS,%
		Hoare:2002:AMS%
		}.
\NAMECITE{praise}{%
		Hoare:2012:PA%
		}.
\NAMECITE{Pre}{%
		Martin:1991:PAO%
		}.
\NAMECITE{Pre-adjunctions}{%
		Martin:1991:PAO%
		}.
\NAMECITE{Predicate}{%
		Hoare:1978:SPP,%
		Naumann:1995:PTH,%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{predicates}{%
		Dijkstra:1982:PTP,%
		Hoare:1984:PEP,%
		Hoare:1984:PP,%
		Hoare:1985:PP,%
		Hoare:1993:PP%
		}.
\NAMECITE{Preface}{%
		Hoare:1986:P,%
		Hoare:1996:PAB,%
		Hoare:1996:PPA,%
		Hoare:1996:PPC,%
		Hoare:1996:PQ,%
		Hoare:2009:PSI,%
		Hoare:2021:PSI,%
		Jones:2021:P,%
		Hoare:1996:PPA%
		}.
\NAMECITE{Prentice}{%
		Anonymous:1987:BRC,%
		Horning:1989:BRE%
		}.
\NAMECITE{Prentice-Hall}{%
		Anonymous:1987:BRC,%
		Horning:1989:BRE%
		}.
\NAMECITE{presence}{%
		Chajed:2017:CFS%
		}.
\NAMECITE{Presentation}{%
		Black:2012:PSD%
		}.
\NAMECITE{Presentations}{%
		Baer:1965:RPP%
		}.
\NAMECITE{presented}{%
		Anonymous:1976:SSE%
		}.
\NAMECITE{Prespecification}{%
		Hoare:1985:WP,%
		Hoare:1987:PDR,%
		Hoare:1986:WPa,%
		Hoare:1986:WPb,%
		Hoare:1987:WP%
		}.
\NAMECITE{Press}{%
		Barron:1975:BRS%
		}.
\NAMECITE{Price}{%
		Barron:1975:BRS,%
		Horning:1989:BRE%
		}.
\NAMECITE{Principles}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{Probabilistic}{%
		Barthe:2012:PRH,%
		Hartog:2002:VPP,%
		Woodcock:2019:PSR,%
		He:1997:LTP,%
		He:1999:LTP,%
		denHartog:2008:TMC%
		}.
\NAMECITE{problem}{%
		Chisholm:1989:ARP%
		}.
\NAMECITE{problems}{%
		Page:1989:SME%
		}.
\NAMECITE{Procedure}{%
		BrinchHansen:2002:OCP%
		}.
\NAMECITE{Procedures}{%
		Damm:1983:SRH,%
		Hoare:1971:PPA,%
		Nipkow:2002:HLR,%
		Fokkinga:1987:CPS,%
		Olderog:1983:CHL,%
		Olderog:1984:CPP%
		}.
\NAMECITE{Proceedings}{%
		ACM:1976:SPE,%
		Hoare:1972:OST,%
		Hoare:2001:ETS,%
		Broy:1996:DPD,%
		Davies:2000:MPC,%
		IEEE:1988:ASL,%
		ACM:1983:PFA,%
		Abadi:2005:CCT,%
		Berghammer:2009:RKA,%
		Bottaci:2010:TAI,%
		Gibbons:2012:MPC,%
		Haddad:2012:ATP,%
		Hofner:2014:RAM,%
		IEEE:2000:PSA,%
		Lenzerini:2008:PTS,%
		Ryder:1999:PAS,%
		Bjorner:1990:VVZ,%
		Kapur:1992:ADC,%
		Ribeiro:2019:UTP,%
		Rishe:1990:PIC%
		}.
\NAMECITE{Process}{%
		Brookes:2021:CPP,%
		Groote:1994:PAG,%
		Hoare:2005:PAUa,%
		Hoare:2005:PAUb,%
		Hoare:2012:LPU,%
		Pettersson:1991:LEC,%
		VanGasteren:1990:CPD,%
		Hoare:2014:LPU%
		}.
\NAMECITE{Processes}{%
		Brookes:1984:TCS,%
		Dijkstra:1971:HOS,%
		Hoare:1978:CCS,%
		Hoare:1978:CSPb,%
		Hoare:1981:CTCb,%
		Hoare:1981:PCC,%
		Hoare:1985:CSP,%
		Hoare:1987:ASP,%
		Hoare:2002:CSP,%
		Hoare:2008:SLS,%
		Hoare:2021:CSP,%
		Kaubisch:1982:DES,%
		Olderog:1986:SOS,%
		Abdallah:2005:CSP,%
		Enikeev:1987:MTC,%
		Hehner:1983:MCM,%
		Hoare:1978:CSPa,%
		Hoare:1980:MCSa,%
		Hoare:1980:MCSb,%
		Hoare:1980:SPP,%
		Hoare:1981:CTCa,%
		Hoare:1981:MCS,%
		Hoare:1982:CCT,%
		Hoare:1983:NCS,%
		Hoare:1991:ASP,%
		Hoare:2011:LEL,%
		Josephs:1989:TAP,%
		Olderog:1983:SOS,%
		Zhou:1981:PCC,%
		deBoer:2002:HLD,%
		Hoare:1983:CSP,%
		Anonymous:1987:BRC%
		}.
\NAMECITE{processing}{%
		Hoare:1993:PPT%
		}.
\NAMECITE{{ProCoS}}{%
		Hoare:1990:AAV,%
		Bowen:1996:PIP%
		}.
\NAMECITE{produce}{%
		Hoare:2004:FSP%
		}.
\NAMECITE{profession}{%
		Hoare:1983:PEP%
		}.
\NAMECITE{Professionalism}{%
		Hoare:1981:P%
		}.
\NAMECITE{Professor}{%
		Davies:2000:MPC,%
		Dijkstra:1970:LPC,%
		Hoare:2016:PST%
		}.
\NAMECITE{Program}{%
		Anonymous:2007:DIPa,%
		Anonymous:2007:DIPb,%
		Ashcroft:1976:RPP,%
		Banerjee:2022:RPL,%
		Clint:1972:PPJ,%
		Fetzer:1988:PVV,%
		Hoare:1971:PPF,%
		Hoare:1975:PCP,%
		Hoare:1987:OSF,%
		Hoare:2007:IPC,%
		Huisman:2000:JPV,%
		vanAmmers:1998:PCC,%
		vanDiepen:1986:PDT,%
		Bergstra:1984:PPI,%
		Brotherston:2008:CPP,%
		Broy:1996:DPD,%
		Chlipala:2013:BSP,%
		Csirmaz:1981:PPV,%
		Dahl:1972:HPS,%
		Foley:1971:PRP,%
		Gibbons:2012:MPC,%
		Hoare:1971:PP,%
		Hoare:1972:PSP,%
		Hoare:2002:APV,%
		Makowsky:1989:WSO,%
		Neuhold:1977:UHM,%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{Programmers}{%
		Hoare:1993:MPM%
		}.
\NAMECITE{Programming}{%
		Bates:1976:SPI,%
		BrinchHansen:2002:OCP,%
		Cherniavsky:1979:CCH,%
		Clarke:1979:PLC,%
		Dahl:1972:SP,%
		Ershov:1974:IST,%
		Feuer:1984:CAP,%
		Hoare:1969:ABC,%
		Hoare:1972:ADP,%
		Hoare:1972:TTP,%
		Hoare:1973:ADP,%
		Hoare:1973:HPLa,%
		Hoare:1973:HPLb,%
		Hoare:1973:HPLc,%
		Hoare:1974:ACA,%
		Hoare:1974:CCF,%
		Hoare:1983:ABC,%
		Hoare:1983:PEP,%
		Hoare:1984:PSS,%
		Hoare:1985:MLP,%
		Hoare:1986:MP,%
		Hoare:1992:LP,%
		Hoare:1993:MPM,%
		Hoare:1994:UTP,%
		Hoare:1997:UTPa,%
		Hoare:1997:UTPb,%
		Hoare:1998:UTP,%
		Hoare:1999:TPT,%
		Hoare:2001:ABC,%
		Hoare:2002:ABC,%
		Hoare:2002:APS,%
		Hoare:2002:TTP,%
		Hoare:2012:LPU,%
		Hoare:2013:GML,%
		Jones:2021:TPL,%
		Kaubisch:1976:QP,%
		Kernighan:1984:WPM,%
		Liu:2013:TPF,%
		ODonnell:1982:CFH,%
		Priestley:2010:SOM,%
		Ryder:1999:PAS,%
		Wolff:2013:UTP,%
		Woodcock:2021:HHU,%
		Bergstra:1984:HLP,%
		Chlipala:2013:BSP,%
		Dijkstra:1972:NSP,%
		Dijkstra:1976:DP,%
		He:1990:CSP,%
		He:1997:LTP,%
		He:1999:LTP,%
		Hoare:1964:EAP,%
		Hoare:1970:BRC,%
		Hoare:1972:PBP,%
		Hoare:1973:CPE,%
		Hoare:1973:HLP,%
		Hoare:1974:ADP,%
		Hoare:1974:HPL,%
		Hoare:1975:HDP,%
		Hoare:1975:PPA,%
		Hoare:1976:HCP,%
		Hoare:1976:HDP,%
		Hoare:1976:PPA,%
		Hoare:1976:SPI,%
		Hoare:1980:HP,%
		Hoare:1981:TMB,%
		Hoare:1985:MP,%
		Hoare:1986:MPI,%
		Hoare:1987:CLP,%
		Hoare:1987:LP,%
		Hoare:1989:VPL,%
		Hoare:1990:AAV,%
		Hoare:1990:CSP,%
		Hoare:1996:PPA,%
		Hoare:2001:UTL,%
		Hoare:2009:VRA,%
		Hoare:2013:LPC,%
		Hoare:2013:USC,%
		Hoare:2014:LCP,%
		Hoare:2014:LPU,%
		Kernighan:1981:WPM,%
		Ni:2006:CAP,%
		Ribeiro:2019:UTP,%
		Roscoe:1986:LOP,%
		Roscoe:1988:LOP,%
		Seres:1999:ALP,%
		Barth:1974:BRJ,%
		Hoare:1996:PAB,%
		Barron:1975:BRS,%
		Lloyd:1974:BRS%
		}.
\NAMECITE{{{programmirovanie}}}{%
		Dahl:1975:CSP%
		}.
\NAMECITE{Programs}{%
		Bergstra:1984:ASP,%
		Csirmaz:1981:PPV,%
		Greif:1981:SSW,%
		Hartog:2002:VPP,%
		Hoare:1984:PEP,%
		Hoare:1984:PP,%
		Hoare:1985:PP,%
		Hoare:1993:PP,%
		Joseph:1987:PRF,%
		Lamport:1980:HLC,%
		Naumann:2019:WSP,%
		Poskitt:2012:HSV,%
		Bergstra:1982:SNS,%
		Boyer:1992:ACP,%
		Chisholm:1989:ARP,%
		Hoare:1982:SPI,%
		Hoare:1986:MAS,%
		Hoare:2008:VFG,%
		Hortala-Gonzalez:1989:HLN,%
		LeGuyadec:1996:SLP,%
		Lifschitz:1984:VPG,%
		Nanevski:2008:YDT,%
		Naumann:1995:PTH,%
		Nielson:1987:HLP,%
		Olderog:1983:CHL,%
		Olderog:1984:CPP,%
		Shaner:2007:MVH,%
		Shapiro:2006:PPC,%
		Stoller:1995:VPU,%
		Ying:2011:FHL%
		}.
\NAMECITE{Progress}{%
		Guttmann:2019:CFC%
		}.
\NAMECITE{Project}{%
		Hoare:2008:VST,%
		Bowen:1996:PIP,%
		Mller:2021:FFY%
		}.
\NAMECITE{Proof}{%
		Foley:1971:PRP,%
		Hoare:1971:PP,%
		Hoare:1971:PPF,%
		Hoare:1972:PCD,%
		Hoare:1972:PSP,%
		Hoare:1976:PCD,%
		Hoare:1996:HDS,%
		Hoare:2001:PCD,%
		Hoare:2002:PCD,%
		Joseph:1987:PRF,%
		Sokolowski:1987:SHL,%
		DeBoer:1997:HSC,%
		Fokkinga:1987:CPS,%
		He:1987:ASP,%
		Hoare:1986:ASP,%
		Hoare:1987:DPM,%
		Hoare:1991:DPM,%
		Kapur:1994:OTP,%
		Nielson:1987:HLP,%
		VanGasteren:1990:CPD,%
		Verjus:1987:PDA,%
		Hoare:1996:PPC%
		}.
\NAMECITE{Proofs}{%
		Barthe:2012:PRH,%
		Hoare:1987:ASP,%
		Barthe:2009:FCC,%
		Boyer:1992:ACP,%
		Boyer:1996:APO,%
		Brotherston:2008:CPP,%
		Gardiner:1995:APC,%
		Hoare:1975:PCP,%
		Hoare:1991:ASP,%
		LeGuyadec:1996:SLP,%
		Shapiro:2006:PPC,%
		denHartog:2008:TMC%
		}.
\NAMECITE{Properties}{%
		Hoare:1978:SPP,%
		Hoare:1986:ASP,%
		Sousa:2016:CHL%
		}.
\NAMECITE{Proposal}{%
		Kral:1966:NHP,%
		Hoare:1966:PSA%
		}.
\NAMECITE{propositional}{%
		Cohen:2000:NCP,%
		Hoare:1985:CNP%
		}.
\NAMECITE{Prospects}{%
		Hoare:1972:PBP%
		}.
\NAMECITE{Protocols}{%
		Hoare:1981:PCC%
		}.
\NAMECITE{prototyping}{%
		Hoare:1990:AAV%
		}.
\NAMECITE{{protsessy}}{%
		Khoar:1989:CVC%
		}.
\NAMECITE{Provably}{%
		He:1994:PCS%
		}.
\NAMECITE{proves}{%
		Hoare:1990:RAPa,%
		Hoare:1990:RAPb,%
		Hoare:1992:RAP%
		}.
\NAMECITE{Proving}{%
		Ashcroft:1976:RPP,%
		Bergstra:1984:PPI,%
		Clint:1972:PPJ,%
		Vafeiadis:2006:PCH,%
		Chisholm:1989:ARP,%
		Hoare:2010:TPH%
		}.
\NAMECITE{Publications}{%
		Baer:1965:RPP,%
		Jones:2021:LTH%
		}.
\NAMECITE{purpose}{%
		Hoare:1972:OSTb%
		}.


\NAMECITE{Qatar}{%
		Berghammer:2009:RKA%
		}.
\NAMECITE{quality}{%
		Hoare:1972:GEQ%
		}.
\NAMECITE{Quantum}{%
		Feng:2021:QHL,%
		Ying:2011:FHL%
		}.
\NAMECITE{Quasiparallel}{%
		Kaubisch:1976:QP%
		}.
\NAMECITE{Queen}{%
		Hoare:1972:OST,%
		Hoare:1971:CSI%
		}.
\NAMECITE{quest}{%
		Hoare:2003:KTK%
		}.
\NAMECITE{Question}{%
		Lewis:1997:BCI%
		}.
\NAMECITE{questions}{%
		RodriguezArtalejo:1985:SQA%
		}.
\NAMECITE{queueing}{%
		Hoare:1973:GCL%
		}.
\NAMECITE{quick}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{quick-sort}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{{Quickselect}}{%
		Prodinger:1995:MQH%
		}.
\NAMECITE{Quicksort}{%
		JaJa:2000:PQ,%
		Foley:1971:PRP,%
		Fouz:2012:SAQ,%
		Hoare:1961:AQ,%
		Hoare:1962:Q,%
		Hoare:1996:PQ,%
		Neuhold:1977:UHM%
		}.


\NAMECITE{R}{%
		Anonymous:1987:BRC,%
		Ashcroft:1976:RPP,%
		Baer:1965:RPP,%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Brockhaus:1973:BRC,%
		Dijkstra:1970:LPC,%
		Dijkstra:1974:LCR,%
		Dijkstra:1975:VTO,%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa,%
		Dijkstra:1982:PTP,%
		Dijkstra:1982:VTO,%
		Dijkstra:20xx:ERC,%
		Hoare:1982:VTO,%
		Horning:1989:BRE,%
		Jones:2010:RWC,%
		Lloyd:1974:BRS,%
		Roscoe:1994:CME,%
		Shustek:2009:IIC%
		}.
\NAMECITE{{R.}}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{RAMiCS}{%
		Hofner:2014:RAM%
		}.
\NAMECITE{{Randell}}{%
		Jones:2011:DHC%
		}.
\NAMECITE{reactive}{%
		DeBoer:1997:HSC%
		}.
\NAMECITE{Real}{%
		Enslow:1975:ILRa,%
		Enslow:1975:ILRb,%
		Enslow:1975:ILRc,%
		Hooman:1992:CVR,%
		Hoare:1975:HDP,%
		Hoare:1976:HDP,%
		Hooman:1994:EHL%
		}.
\NAMECITE{Real-Time}{%
		Enslow:1975:ILRa,%
		Enslow:1975:ILRb,%
		Enslow:1975:ILRc,%
		Hooman:1992:CVR,%
		Hoare:1975:HDP,%
		Hoare:1976:HDP,%
		Hooman:1994:EHL%
		}.
\NAMECITE{Realizations}{%
		Reus:2001:HCV%
		}.
\NAMECITE{Reasoning}{%
		Shankar:1993:IAR,%
		deBoer:2021:CCR,%
		vonHenke:1985:RHS,%
		Chisholm:1989:ARP,%
		Delbianco:2013:HSR,%
		Gardner:2008:LHR,%
		Gordon:1992:MRH,%
		Pettersson:1991:LEC,%
		Turon:2013:URH%
		}.
\NAMECITE{receipt}{%
		Hoare:2012:MT,%
		Hoare:2012:MTR%
		}.
\NAMECITE{Recommendation}{%
		Hoare:1968:RDR%
		}.
\NAMECITE{Record}{%
		Hoare:1965:RH,%
		Hoare:1968:RH,%
		Dijkstra:20xx:ERC%
		}.
\NAMECITE{Recovery}{%
		Hoare:2011:RB,%
		He:1987:ASP%
		}.
\NAMECITE{Recursion}{%
		Mamouras:2016:HLD%
		}.
\NAMECITE{Recursive}{%
		Hoare:1975:RDS,%
		Nipkow:2002:HLR,%
		Foley:1971:PRP%
		}.
\NAMECITE{Reduction}{%
		Johnston:1975:MRE%
		}.
\NAMECITE{redundant}{%
		Mancini:1988:HLD%
		}.
\NAMECITE{reference}{%
		Spivey:1989:ZNR%
		}.
\NAMECITE{refined}{%
		He:1986:DRR%
		}.
\NAMECITE{Refinement}{%
		Hoare:1990:RAPa,%
		Hoare:1990:RAPb,%
		Hoare:1992:RAP,%
		He:1986:DRR,%
		He:1990:DRC,%
		Hoare:1987:PDR,%
		Hoare:1990:DRC,%
		Turon:2013:URH%
		}.
\NAMECITE{refinements}{%
		vanAmmers:1998:PCC%
		}.
\NAMECITE{Reflections}{%
		Jones:2010:RWC%
		}.
\NAMECITE{regular}{%
		Hortala-Gonzalez:1989:HLN%
		}.
\NAMECITE{relation}{%
		Gritzner:1996:RAM%
		}.
\NAMECITE{Relational}{%
		Banerjee:2022:RPL,%
		Barthe:2012:PRH,%
		Berghammer:2009:RKA,%
		Hofner:2014:RAM%
		}.
\NAMECITE{Relations}{%
		Berghammer:2009:RKA,%
		Foster:2019:HRI%
		}.
\NAMECITE{relative}{%
		RodriguezArtalejo:1985:SQA%
		}.
\NAMECITE{Relatively}{%
		Damm:1983:SRH%
		}.
\NAMECITE{Reliability}{%
		Broy:2007:SSR,%
		Hoare:1975:DR%
		}.
\NAMECITE{Reliable}{%
		Hoare:1996:HDS%
		}.
\NAMECITE{RelMiCS}{%
		Berghammer:2009:RKA%
		}.
\NAMECITE{Rely}{%
		Hayes:2019:DAR%
		}.
\NAMECITE{Rely/Guarantee}{%
		Hayes:2019:DAR%
		}.
\NAMECITE{Remark}{%
		Brown:1976:RAA%
		}.
\NAMECITE{Remarks}{%
		Ashcroft:1976:RPP%
		}.
\NAMECITE{Remote}{%
		BrinchHansen:2002:OCP%
		}.
\NAMECITE{Report}{%
		Bates:1976:SPI,%
		Dijkstra:1970:NIM,%
		Hoare:1962:REA,%
		Hoare:1968:RDR,%
		Woodger:1969:MRA,%
		Bowen:1996:PIP%
		}.
\NAMECITE{repository}{%
		Bicarregui:2006:VSR%
		}.
\NAMECITE{Representations}{%
		Hoare:2001:PCD,%
		Hoare:2002:PCD,%
		Hoare:1972:PCD,%
		Hoare:1976:PCD,%
		Hoare:1996:PPC%
		}.
\NAMECITE{Reprint}{%
		Hoare:1983:ABC,%
		Hoare:1983:CSP%
		}.
\NAMECITE{Research}{%
		Bottaci:2010:TAI,%
		Hoare:2003:VCGa,%
		Hoare:2004:GCC,%
		Hoare:2005:GCC,%
		Bowen:1996:PIP,%
		Cleaveland:1996:SDC,%
		Hoare:2003:VCGb,%
		Hoare:2005:VCG%
		}.
\NAMECITE{Researcher}{%
		Anonymous:20xx:THE%
		}.
\NAMECITE{Resources}{%
		Gray:2021:OR%
		}.
\NAMECITE{Responses}{%
		Anonymous:2007:DIPb%
		}.
\NAMECITE{Result}{%
		Wand:1978:NIR,%
		Wand:1976:NIR%
		}.
\NAMECITE{resume}{%
		He:1986:DRR%
		}.
\NAMECITE{retract}{%
		He:2010:CRC%
		}.
\NAMECITE{Retrospective}{%
		Hoare:2009:VRA%
		}.
\NAMECITE{Review}{%
		Anonymous:1987:BRC,%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Hoare:1970:BR,%
		Hoare:1970:BRC,%
		Hoare:1977:BR,%
		Horning:1989:BRE,%
		Lloyd:1974:BRS,%
		Brockhaus:1973:BRC,%
		Hoare:1964:BRA%
		}.
\NAMECITE{Reviews}{%
		Hoare:1963:BR%
		}.
\NAMECITE{Revised}{%
		Abdallah:2005:CSP,%
		Meyer:2008:VST,%
		Wolff:2013:UTP%
		}.
\NAMECITE{Revisited}{%
		vonOheimb:2002:HLN,%
		Kirkerud:1982:CHC%
		}.
\NAMECITE{Rewriting}{%
		Jones:2001:PRR,%
		Sun:1996:TRH%
		}.
\NAMECITE{Richard}{%
		Black:2012:PSD,%
		Dijkstra:1999:FWT,%
		Frana:2002:ICA%
		}.
\NAMECITE{{RoboChart}}{%
		Woodcock:2019:PSR%
		}.
\NAMECITE{robust}{%
		Gritzner:1996:RAM%
		}.
\NAMECITE{{Roger}}{%
		Herbert:2004:CST,%
		Hoare:2004:RMN%
		}.
\NAMECITE{role}{%
		Hoare:1973:TMR%
		}.
\NAMECITE{Roles}{%
		Borgstrom:2011:RSH%
		}.
\NAMECITE{Royal}{%
		Dijkstra:1982:PTP,%
		Gordon:1992:MRH%
		}.
\NAMECITE{rule}{%
		Olderog:1983:NER,%
		Takaoka:1987:DRH%
		}.
\NAMECITE{Rules}{%
		Joseph:1987:PRF,%
		Olderog:1981:SCH,%
		Cocco:1982:MEH,%
		Jones:2001:PRR,%
		Thielecke:2006:FRA%
		}.
\NAMECITE{Running}{%
		Butler:2005:TSL%
		}.


\NAMECITE{Safety}{%
		Broy:2011:SSS,%
		Hoare:1986:MAS,%
		Sousa:2016:CHL%
		}.
\NAMECITE{Said}{%
		McReynolds:1997:LBS%
		}.
\NAMECITE{Salute}{%
		Feijen:1990:BOB%
		}.
\NAMECITE{San}{%
		Abadi:2005:CCT%
		}.
\NAMECITE{Sanderson}{%
		Hoare:1970:BRC%
		}.
\NAMECITE{Saratoga}{%
		Kapur:1992:ADC%
		}.
\NAMECITE{Schemes}{%
		Mamouras:2016:HLD%
		}.
\NAMECITE{School}{%
		Hoare:2001:ETS,%
		Bauer:1976:LHI,%
		Johnston:1975:MRE,%
		Muller:2010:ALS%
		}.
\NAMECITE{Science}{%
		Hoare:1976:CST,%
		Hoare:1984:PSS,%
		Hoare:1989:ECS,%
		Hoare:1996:UTC,%
		Hoare:2001:ETS,%
		Hoare:2007:SEC,%
		Hofner:2014:RAM,%
		IEEE:1976:ASF,%
		IEEE:1988:ASL,%
		Lewis:2021:ICF,%
		Priestley:2010:SOM,%
		Berghammer:2009:RKA,%
		Davies:2000:MPC,%
		Hoare:1971:CSI,%
		Hoare:1996:MMC,%
		Hoare:1998:SCE,%
		Horning:1989:BRE%
		}.
\NAMECITE{Sciences}{%
		Hoare:2001:ETS%
		}.
\NAMECITE{Scientific}{%
		Elliott:1989:SAM,%
		Hoare:2002:APS%
		}.
\NAMECITE{Scientists}{%
		Hoare:1989:NAC%
		}.
\NAMECITE{scope}{%
		Hoare:1972:OSTb%
		}.
\NAMECITE{{Scotland}}{%
		IEEE:1988:ASL%
		}.
\NAMECITE{sd\&m}{%
		Broy:2001:PTC%
		}.
\NAMECITE{second}{%
		Makowsky:1989:WSO%
		}.
\NAMECITE{Security}{%
		Barthe:2012:PRH,%
		Broy:2007:SSR%
		}.
\NAMECITE{SELECT}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA%
		}.
\NAMECITE{Selected}{%
		Dijkstra:1982:SWC,%
		Meyer:2008:VST,%
		Wolff:2013:UTP%
		}.
\NAMECITE{Selection}{%
		Grubel:1996:ADT,%
		Grubel:1998:HSA%
		}.
\NAMECITE{self}{%
		Cai:2007:CSM%
		}.
\NAMECITE{self-modifying}{%
		Cai:2007:CSM%
		}.
\NAMECITE{Semantical}{%
		Pratt:1976:SCF%
		}.
\NAMECITE{Semantics}{%
		Aichernig:2019:TPA,%
		Bergstra:1984:ASP,%
		Butler:2005:TSL,%
		Francez:1978:SNC,%
		Francez:1979:SNC,%
		Greif:1981:SSW,%
		Hoare:1974:CCF,%
		Hoare:1994:ACO,%
		Hoare:2005:TSO,%
		Hoare:2008:SLS,%
		Olderog:1986:SOS,%
		PeytonJones:1999:SIE,%
		Woodcock:2019:PSR,%
		Wu:2019:USC,%
		He:1990:CSP,%
		He:1993:AOS,%
		Hoare:1990:CSP,%
		Hoare:1997:ADO,%
		Hoare:2000:ADO,%
		Hoare:2013:USC,%
		Jones:1999:SIE,%
		Olderog:1983:SOS,%
		Saabas:2007:CNS,%
		Tennent:1991:CPW%
		}.
\NAMECITE{Semaphores}{%
		BrinchHansen:2002:OCP%
		}.
\NAMECITE{Seminar}{%
		Hoare:1972:OST%
		}.
\NAMECITE{Sentences}{%
		Hoare:1961:MSS,%
		vonHenke:1985:RHS%
		}.
\NAMECITE{Separation}{%
		Hoare:2008:SLS,%
		Brotherston:2008:CPP,%
		Nanevski:2006:PSH,%
		Nanevski:2008:HTT,%
		Wehrman:2009:GMS%
		}.
\NAMECITE{September}{%
		Anonymous:1976:SSE,%
		Bottaci:2010:TAI,%
		Hoare:1972:OST,%
		Jones:2013:ICC,%
		Pettersson:1991:LEC%
		}.
\NAMECITE{Sequential}{%
		Anonymous:1987:BRC,%
		Brookes:1984:TCS,%
		Dijkstra:1971:HOS,%
		Hoare:1978:CCS,%
		Hoare:1978:CSPb,%
		Hoare:1983:CSP,%
		Hoare:1985:CSP,%
		Hoare:1986:NCS,%
		Hoare:1987:ASP,%
		Hoare:2002:CSP,%
		Hoare:2021:CSP,%
		Kaubisch:1982:DES,%
		LeGuyadec:1996:SLP,%
		vonKarger:1995:SC,%
		Abdallah:2005:CSP,%
		Enikeev:1987:MTC,%
		Hoare:1978:CSPa,%
		Hoare:1980:MCSa,%
		Hoare:1980:MCSb,%
		Hoare:1981:MCS,%
		Hoare:1983:NCS,%
		Hoare:1985:NCS,%
		Hoare:1991:ASP,%
		Zhou:1981:PCC%
		}.
\NAMECITE{Sequential-like}{%
		LeGuyadec:1996:SLP%
		}.
\NAMECITE{Series}{%
		Hoare:2001:ETS%
		}.
\NAMECITE{service}{%
		Hoare:1985:SSN,%
		Hoare:1986:ASP,%
		Hoare:1987:DPM,%
		Hoare:1991:DPM,%
		Morgan:1985:SSN%
		}.
\NAMECITE{Set}{%
		Hoare:1968:SM%
		}.
\NAMECITE{setting}{%
		Csirmaz:1981:PPV,%
		He:1990:DRC,%
		Hoare:1990:DRC%
		}.
\NAMECITE{Seventh}{%
		IEEE:2000:PSA,%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{several}{%
		Prodinger:1995:MQH%
		}.
\NAMECITE{shared}{%
		DeBoer:1997:HSC%
		}.
\NAMECITE{shifts}{%
		Hoare:2004:FSP%
		}.
\NAMECITE{Side}{%
		vonOheimb:2002:HLN%
		}.
\NAMECITE{sieve}{%
		Hoare:1972:PSP%
		}.
\NAMECITE{SIGACT}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{SIGART}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{SIGMOD}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{SIGMOD-SIGACT-SIGART}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{SIGPLAN}{%
		Hoare:2012:MT,%
		Ryder:1999:PAS,%
		Black:2012:PSD,%
		Hoare:2012:MTR%
		}.
\NAMECITE{Simple}{%
		Cherniavsky:1979:CCH%
		}.
\NAMECITE{simplified}{%
		Hoare:1985:SSN,%
		Morgan:1985:SSN%
		}.
\NAMECITE{Simulation}{%
		Engelhardt:1996:SSS,%
		Kaubisch:1982:DES%
		}.
\NAMECITE{{Simulink}}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{{Simulink/Stateflow}}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{Single}{%
		Hoare:1966:SPC%
		}.
\NAMECITE{Sir}{%
		Davies:2000:MPC,%
		Hoare:2016:PST,%
		Black:2012:PSD,%
		Dale:1994:CST%
		}.
\NAMECITE{size}{%
		Hoare:1974:OSS%
		}.
\NAMECITE{Smallest}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA%
		}.
\NAMECITE{Smoothed}{%
		Fouz:2012:SAQ%
		}.
\NAMECITE{{Smyth}}{%
		Flannery:1990:HSP%
		}.
\NAMECITE{Society}{%
		Gordon:1992:MRH,%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{Software}{%
		Beckert:2006:ISF,%
		Broy:2001:PTC,%
		Broy:2002:SPC,%
		Broy:2003:MAL,%
		Broy:2005:ETS,%
		Broy:2007:SSR,%
		Broy:2011:SSS,%
		Daylight:2012:DSE,%
		Hayes:2021:SS,%
		Hoare:1974:SDP,%
		Hoare:1975:SE,%
		Hoare:1978:ESS,%
		Hoare:1978:SEK,%
		Hoare:1994:HSCa,%
		Hoare:1996:HDS,%
		Hoare:2001:ETS,%
		Hoare:2008:VST,%
		Hoare:2021:PSI,%
		Hoare:2021:VSI,%
		IEEE:2000:PSA,%
		IEEE:2002:AIC,%
		Meyer:2008:VST,%
		Mller:2021:FFY,%
		Bicarregui:2006:VSR,%
		Bjorner:1990:VVZ,%
		Hoare:1972:GEQ,%
		Hoare:1993:WSE,%
		Hoare:1994:HSCb,%
		Hoare:1998:SCE,%
		Hoare:2002:AMS,%
		Hoare:2006:IVS,%
		Hoare:2009:PSI,%
		Hoare:2009:VSI,%
		Muller:2010:ALS,%
		Rehof:2010:ADS,%
		Anonymous:1976:SSE%
		}.
\NAMECITE{solution}{%
		Page:1989:SME%
		}.
\NAMECITE{Solutions}{%
		Dijkstra:1982:MSMa,%
		Dijkstra:1977:MSM%
		}.
\NAMECITE{Some}{%
		Bergstra:1982:SNS,%
		Hoare:1978:SPP,%
		Hoare:1987:OSF,%
		RodriguezArtalejo:1985:SQA%
		}.
\NAMECITE{Sorcery}{%
		Hoare:1984:PSS%
		}.
\NAMECITE{Sorry}{%
		Santini:2005:WSI%
		}.
\NAMECITE{sort}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{sorting}{%
		Fokkinga:1987:CPS%
		}.
\NAMECITE{Sound}{%
		Damm:1983:SRH,%
		Olderog:1981:SCH,%
		Arthan:2009:GFS,%
		Bergstra:1982:SNS,%
		Hoare:2004:FSP%
		}.
\NAMECITE{Soundness}{%
		Sokolowski:1987:SHL%
		}.
\NAMECITE{Space}{%
		Hoare:2019:CST,%
		Hoare:2019:CSTa%
		}.
\NAMECITE{Spain}{%
		Gibbons:2012:MPC%
		}.
\NAMECITE{Special}{%
		Hoare:2021:PSI,%
		Hoare:2009:PSI%
		}.
\NAMECITE{Specific}{%
		Enslow:1975:ILRc%
		}.
\NAMECITE{Specification}{%
		Broy:2011:SSS,%
		Hayes:2021:SS,%
		Hoare:1985:SSN,%
		Morgan:1985:SSN,%
		Olderog:1983:SOS,%
		Olderog:1986:SOS,%
		Engelhardt:1996:SSS,%
		He:1987:ASP,%
		Hoare:1986:ASP,%
		Hoare:1990:AAV,%
		Rehof:2010:ADS%
		}.
\NAMECITE{Specification-Oriented}{%
		Olderog:1986:SOS,%
		Olderog:1983:SOS%
		}.
\NAMECITE{Specifications}{%
		Hoare:1982:SPI,%
		Hoare:1987:ASP,%
		Naumann:2019:WSP,%
		Hoare:1990:RAPa,%
		Hoare:1990:RAPb,%
		Hoare:1991:ASP,%
		Sergey:2016:HSS%
		}.
\NAMECITE{specified}{%
		Shaner:2007:MVH%
		}.
\NAMECITE{Specifying}{%
		Greif:1981:SSW%
		}.
\NAMECITE{spheres}{%
		Hoare:2004:FSP%
		}.
\NAMECITE{Springs}{%
		Kapur:1992:ADC%
		}.
\NAMECITE{stacks}{%
		Borgstrom:2011:RSH%
		}.
\NAMECITE{standard}{%
		Xu:2016:CHL%
		}.
\NAMECITE{{Standardisation}}{%
		Enslow:1975:ILRa%
		}.
\NAMECITE{Startling}{%
		Hoare:1978:ESS%
		}.
\NAMECITE{State}{%
		Bates:1976:SPI,%
		Becker:2010:LSM%
		}.
\NAMECITE{state-modifying}{%
		Becker:2010:LSM%
		}.
\NAMECITE{{Stateflow}}{%
		Zhan:2019:UGC%
		}.
\NAMECITE{Statement}{%
		Hoare:1972:NS,%
		Hoare:1996:UTP%
		}.
\NAMECITE{statements}{%
		Engelhardt:1996:SSS,%
		Lifschitz:1984:VPG%
		}.
\NAMECITE{step}{%
		Bicarregui:2006:VSR%
		}.
\NAMECITE{{STOC}}{%
		ACM:1976:SPE%
		}.
\NAMECITE{store}{%
		Hoare:1968:DST,%
		Hoare:1972:SSMa,%
		Hoare:1972:SSMb,%
		Hoare:1974:OSS%
		}.
\NAMECITE{Stories}{%
		Hoare:2000:SLI%
		}.
\NAMECITE{Story}{%
		Hoare:1991:TOP%
		}.
\NAMECITE{Strategic}{%
		Cleaveland:1996:SDC%
		}.
\NAMECITE{Strict}{%
		Guttmann:2019:CFC%
		}.
\NAMECITE{Structure}{%
		Hoare:1982:SOS,%
		Hoare:1976:SOS%
		}.
\NAMECITE{Structured}{%
		Barth:1974:BRJ,%
		Bates:1976:SPI,%
		Dahl:1972:SP,%
		Hoare:1976:SPI,%
		Chlipala:2013:BSP,%
		Dijkstra:1972:NSP,%
		Hoare:1972:PSP,%
		Hoare:1973:SPS,%
		Barron:1975:BRS,%
		Lloyd:1974:BRS%
		}.
\NAMECITE{structures}{%
		Bergstra:1982:SNS,%
		Dahl:1972:HPS,%
		Hoare:1968:DST,%
		Hoare:1975:RDS%
		}.
\NAMECITE{Structuring}{%
		Hoare:1974:MOS,%
		Hoare:2002:MOS,%
		Hoare:1972:NDS%
		}.
\NAMECITE{Strukturnoe}{%
		Dahl:1975:CSP%
		}.
\NAMECITE{Stuck}{%
		Fournet:2004:SFC%
		}.
\NAMECITE{Stuck-free}{%
		Fournet:2004:SFC%
		}.
\NAMECITE{Student}{%
		Jones:2013:ICC%
		}.
\NAMECITE{Students}{%
		Jones:2021:DS%
		}.
\NAMECITE{{Studer}}{%
		Pritchard:1979:CPJ%
		}.
\NAMECITE{Study}{%
		Broy:1996:DPD,%
		Hoare:2010:MJD%
		}.
\NAMECITE{stvuyushchie}{%
		Khoar:1989:CVC%
		}.
\NAMECITE{Style}{%
		ODonnell:1982:CFH,%
		Poskitt:2012:HSV,%
		DeBoer:1997:HSC,%
		Delbianco:2013:HSR,%
		Sergey:2016:HSS,%
		Turon:2013:URH,%
		denHartog:2008:TMC%
		}.
\NAMECITE{substitution}{%
		Rehof:2010:ADS%
		}.
\NAMECITE{Success}{%
		Apt:2021:ASI,%
		Gozum:1997:LWC%
		}.
\NAMECITE{Successor}{%
		Hoare:1966:PSA%
		}.
\NAMECITE{suggested}{%
		Dijkstra:20xx:ERC%
		}.
\NAMECITE{Summer}{%
		Hoare:2001:ETS,%
		Bauer:1976:LHI,%
		Muller:2010:ALS%
		}.
\NAMECITE{Survey}{%
		Apt:1981:TYH,%
		Apt:1984:TYH,%
		Hoare:1972:SSMa,%
		Hoare:1972:SSMb%
		}.
\NAMECITE{sweet}{%
		Hoare:2004:FSP%
		}.
\NAMECITE{switching}{%
		Hoare:1988:PCC,%
		Hoare:1990:MSS,%
		Zhou:1992:MSS%
		}.
\NAMECITE{Switzerland}{%
		Meyer:2008:VST%
		}.
\NAMECITE{Symposium}{%
		ACM:1983:PFA,%
		Bjorner:1990:VVZ,%
		Davies:2000:MPC,%
		Ershov:1974:IST,%
		IEEE:1976:ASF,%
		IEEE:1988:ASL,%
		Lenzerini:2008:PTS,%
		Ribeiro:2019:UTP,%
		Wolff:2013:UTP,%
		ACM:1976:SPE,%
		Abdallah:2005:CSP%
		}.
\NAMECITE{Synchronisation}{%
		Hoare:1980:SPP%
		}.
\NAMECITE{synchronous}{%
		Hoare:1990:MSS,%
		Zhou:1992:MSS%
		}.
\NAMECITE{synchrony}{%
		He:1990:TSA%
		}.
\NAMECITE{Syntagmatic}{%
		Hoare:1961:MSS%
		}.
\NAMECITE{Synthesizing}{%
		Hoare:1961:MSS%
		}.
\NAMECITE{System}{%
		Broy:2007:SSR,%
		Hoare:1974:MOS,%
		Hoare:1982:SOS,%
		Hoare:2002:MOS,%
		Qian:1990:ASD,%
		Wand:1978:NIR,%
		Chajed:2017:CFS,%
		Chlipala:2013:BSP,%
		Hoare:1963:EAI,%
		Hoare:1964:EAP,%
		Hoare:1973:SPS,%
		Hoare:1976:SOS,%
		Hoare:1989:FMC,%
		Kapur:1994:OTP,%
		Nielson:1987:HLP,%
		Szczepanska:1991:HLV,%
		Wand:1976:NIR%
		}.
\NAMECITE{Systems}{%
		Beckert:2006:ISF,%
		Brockhaus:1973:BRC,%
		Broy:2005:ETS,%
		Broy:2011:SSS,%
		Clarke:1979:PLC,%
		Enslow:1975:ILRa,%
		Enslow:1975:ILRb,%
		Enslow:1975:ILRc,%
		He:1994:PCS,%
		Herbert:2004:CST,%
		Hoare:1972:OST,%
		Hoare:1986:NCS,%
		Hoare:2001:ETS,%
		Hooman:1992:CVR,%
		Lenzerini:2008:PTS,%
		Shankar:1993:IAR,%
		Zhan:2019:UGC,%
		Anonymous:1976:SSE,%
		Arthan:2013:HLL,%
		DeBoer:1997:HSC,%
		Enikeev:1987:MTC,%
		Hoare:1972:OSTb,%
		Hoare:1985:NCS,%
		Makowsky:1989:WSO,%
		Mancini:1988:HLD,%
		Rehof:2010:ADS,%
		Ridge:2009:VDS%
		}.


\NAMECITE{TAIC}{%
		Bottaci:2010:TAI%
		}.
\NAMECITE{talk}{%
		Hoare:2000:LC,%
		Hoare:2006:IVS%
		}.
\NAMECITE{Tame}{%
		Struth:2021:THA%
		}.
\NAMECITE{Tasks}{%
		Hoare:1993:MPM%
		}.
\NAMECITE{TC}{%
		Meyer:2008:VST%
		}.
\NAMECITE{Teaching}{%
		Sufrin:2021:TBO%
		}.
\NAMECITE{Tears}{%
		Macnaghten:1977:FFT%
		}.
\NAMECITE{technique}{%
		Hoare:2010:MJD,%
		Jones:2001:PRR%
		}.
\NAMECITE{Techniques}{%
		Bottaci:2010:TAI,%
		Hoare:1972:OST,%
		Hoare:1972:SSMa,%
		Hoare:1972:SSMb,%
		Brockhaus:1973:BRC%
		}.
\NAMECITE{Technology}{%
		Herbert:2004:CST,%
		Hoare:1976:CST,%
		Hoare:1983:TF%
		}.
\NAMECITE{{Tecton}}{%
		Kapur:1994:OTP%
		}.
\NAMECITE{Ten}{%
		Apt:1981:TYH,%
		Apt:1984:TYH,%
		McReynolds:1997:LBS%
		}.
\NAMECITE{Term}{%
		Sun:1996:TRH%
		}.
\NAMECITE{Termination}{%
		Huisman:2000:JPV,%
		Brotherston:2008:CPP%
		}.
\NAMECITE{Testing}{%
		Aichernig:2019:TPA,%
		Hoare:2010:TPH,%
		Bottaci:2010:TAI%
		}.
\NAMECITE{tests}{%
		Kozen:2000:HLK%
		}.
\NAMECITE{Texas}{%
		IEEE:1976:ASF%
		}.
\NAMECITE{text}{%
		Woodger:1969:MRA%
		}.
\NAMECITE{th}{%
		Brown:1976:RAA,%
		Floyd:1975:AAA%
		}.
\NAMECITE{thanks}{%
		Hoare:2012:MT,%
		Hoare:2012:MTR%
		}.
\NAMECITE{Their}{%
		Broy:2001:PTC,%
		Bergstra:1982:SNS,%
		Hoare:1972:OSTb,%
		Hoare:1976:CST,%
		Rishe:1990:PIC%
		}.
\NAMECITE{Theme}{%
		Hoare:1982:VTO,%
		Dijkstra:1975:VTO,%
		Dijkstra:1982:VTO%
		}.
\NAMECITE{Theorems}{%
		Bergstra:1982:TTA%
		}.
\NAMECITE{Theoretical}{%
		Ershov:1974:IST,%
		Hoare:1993:PPT%
		}.
\NAMECITE{Theories}{%
		Baeten:1990:CTC,%
		Bloom:1991:FHL,%
		Broy:2005:ETS,%
		Hoare:1974:CCF,%
		Hoare:1994:UTP,%
		Hoare:1996:UTC,%
		Hoare:1997:UTPa,%
		Hoare:1997:UTPb,%
		Hoare:1998:UTP,%
		Hoare:1999:TPT,%
		Hoare:2001:ETS,%
		Hoare:2008:VST,%
		Jones:2021:TPL,%
		Liu:2013:TPF,%
		Meyer:2008:VST,%
		Wolff:2013:UTP,%
		Woodcock:2021:HHU,%
		He:1997:LTP,%
		He:1999:LTP,%
		He:2000:UTH,%
		He:2005:LTC,%
		Hoare:1996:UTP,%
		Hoare:1997:UTC,%
		Hoare:2001:UTL,%
		Ribeiro:2019:UTP%
		}.
\NAMECITE{Theory}{%
		ACM:1976:SPE,%
		ACM:1983:PFA,%
		Baer:1965:RPP,%
		Bazilevskii:1963:TMM,%
		Brookes:1984:TCS,%
		Grubel:1996:ADT,%
		Haddad:2012:ATP,%
		Herbert:2004:CST,%
		Hoare:1972:TTP,%
		Hoare:1989:NAC,%
		Hoare:2002:APS,%
		Hoare:2002:TTP,%
		Abadi:2005:CCT,%
		Enikeev:1987:MTC,%
		He:1990:TSA,%
		Hoare:1980:TND,%
		Hoare:1990:MSS,%
		Hoare:1990:TCC,%
		Hoare:1990:TDC,%
		Hoare:1991:TCC,%
		Hoare:1991:TDCa,%
		Hoare:1991:TDCb,%
		Hoare:2010:MJD,%
		Josephs:1989:TAP,%
		Kennaway:1980:TN,%
		Nanevski:2006:PSH,%
		Nanevski:2008:HTT,%
		Zhou:1992:MSS%
		}.
\NAMECITE{there}{%
		Hoare:1981:TMB%
		}.
\NAMECITE{think}{%
		Hoare:2004:YWT%
		}.
\NAMECITE{Third}{%
		Bjorner:1990:VVZ,%
		Hoare:2007:IPC%
		}.
\NAMECITE{thousand}{%
		Dijkstra:1999:FWT%
		}.
\NAMECITE{Time}{%
		Enslow:1975:ILRa,%
		Enslow:1975:ILRb,%
		Enslow:1975:ILRc,%
		Hoare:2019:CST,%
		Hooman:1992:CVR,%
		Manna:2010:TVE,%
		Hoare:1975:HDP,%
		Hoare:1976:HDP,%
		Hoare:2019:CSTa,%
		Hooman:1994:EHL,%
		Nielson:1987:HLP%
		}.
\NAMECITE{times}{%
		Hoare:2000:SLI%
		}.
\NAMECITE{timetables}{%
		Johnston:1975:MRE%
		}.
\NAMECITE{Tolerant}{%
		Joseph:1987:PRF%
		}.
\NAMECITE{Tomorrow}{%
		Hoare:1973:TMR%
		}.
\NAMECITE{Tony}{%
		Hoare:2016:PST,%
		Ribeiro:2019:UTP,%
		Anonymous:2007:DIPa,%
		Anonymous:2007:DIPb,%
		Anonymous:20xx:THE,%
		Daylight:2012:THM,%
		Dijkstra:1989:ETH,%
		Jones:2021:LTH,%
		Jones:2021:TPL%
		}.
\NAMECITE{Tools}{%
		Hoare:2008:VST,%
		Meyer:2008:VST%
		}.
\NAMECITE{Top}{%
		Cipra:2000:BCE,%
		Hoare:1999:TPT%
		}.
\NAMECITE{Top-Down}{%
		Hoare:1999:TPT%
		}.
\NAMECITE{toppled}{%
		Hoare:2003:KTK%
		}.
\NAMECITE{Total}{%
		Hoare:1981:CTCb,%
		Hoare:1981:CTCa,%
		Hoare:1982:CCT%
		}.
\NAMECITE{Trace}{%
		Butler:2005:TSL,%
		Hoare:1999:TMPb,%
		Hoare:1999:TMPa%
		}.
\NAMECITE{Transactions}{%
		Butler:2005:TSL,%
		Hoare:2007:CT,%
		Hoare:2010:CT,%
		Qian:1990:ASD%
		}.
\NAMECITE{Transform}{%
		Macnaghten:1977:FFT%
		}.
\NAMECITE{Transformations}{%
		vanDiepen:1986:PDT%
		}.
\NAMECITE{Transformers}{%
		Hoare:1978:SPP,%
		Dijkstra:1982:PTP,%
		Naumann:1995:PTH%
		}.
\NAMECITE{Translation}{%
		Hoare:1961:MSS%
		}.
\NAMECITE{translator}{%
		Hoare:1962:REA%
		}.
\NAMECITE{Transputer}{%
		Hoare:1991:TOP%
		}.
\NAMECITE{{Traub}}{%
		Dijkstra:1977:MSM,%
		Dijkstra:1982:MSMa%
		}.
\NAMECITE{Tree}{%
		Hoare:2005:TSO%
		}.
\NAMECITE{tribute}{%
		Herbert:2004:CST%
		}.
\NAMECITE{Trick}{%
		Hoare:2010:UCT%
		}.
\NAMECITE{Trimming}{%
		Struth:2021:THA%
		}.
\NAMECITE{triple}{%
		Borgstrom:2011:RSH%
		}.
\NAMECITE{Triples}{%
		Hooman:1992:CVR%
		}.
\NAMECITE{true}{%
		Pettersson:1991:LEC,%
		VanGasteren:1990:CPD%
		}.
\NAMECITE{{Tuesday}}{%
		Dijkstra:1982:PTP%
		}.
\NAMECITE{Turing}{%
		Ashenhurst:1987:ATA,%
		Hoare:2016:PST,%
		Hoare:2021:ATA,%
		Daylight:2012:DSE%
		}.
\NAMECITE{Tutorial}{%
		Greif:1981:SSW%
		}.
\NAMECITE{Twenty}{%
		Lenzerini:2008:PTS,%
		Ashenhurst:1987:ATA%
		}.
\NAMECITE{Twenty-Seventh}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{Two}{%
		Bergstra:1982:TTA,%
		Bergstra:1984:HLP,%
		Bruni:2005:CTA,%
		Hoare:1968:DST%
		}.
\NAMECITE{two-level}{%
		Hoare:1968:DST%
		}.
\NAMECITE{Type}{%
		Damm:1983:SRH,%
		Nanevski:2006:PSH,%
		Nanevski:2008:HTT%
		}.
\NAMECITE{types}{%
		Bergstra:1984:HLP,%
		Nanevski:2008:YDT,%
		Thielecke:2006:FRA,%
		Wing:1989:VAD%
		}.


\NAMECITE{UK}{%
		Abdallah:2005:CSP,%
		Bottaci:2010:TAI%
		}.
\NAMECITE{Unbounded}{%
		Nipkow:2002:HLR%
		}.
\NAMECITE{uncertainty}{%
		Hoare:2002:LLU%
		}.
\NAMECITE{Unification}{%
		Baeten:1990:CTC,%
		Hoare:1996:UTC%
		}.
\NAMECITE{Unified}{%
		Butterfield:2019:IOA,%
		Hoare:1994:UTP,%
		Hoare:1997:UTPa,%
		Zhan:2019:UGC%
		}.
\NAMECITE{Unifies}{%
		vanStaden:2013:AUO%
		}.
\NAMECITE{Unify}{%
		Hoare:2012:LPU,%
		Hoare:2014:LPU%
		}.
\NAMECITE{Unifying}{%
		He:2000:UTH,%
		Hoare:1996:UTP,%
		Hoare:1997:UTC,%
		Hoare:1997:UTPb,%
		Hoare:1998:UTP,%
		Hoare:2001:UTL,%
		Hoare:2005:PAUa,%
		Hoare:2005:PAUb,%
		Hoare:2011:UMD,%
		Hoare:2013:USC,%
		Turon:2013:URH,%
		Wolff:2013:UTP,%
		Woodcock:2021:HHU,%
		Ribeiro:2019:UTP%
		}.
\NAMECITE{United}{%
		Horning:1989:BRE,%
		Jones:2013:ICC%
		}.
\NAMECITE{universe}{%
		Hoare:2004:VIF%
		}.
\NAMECITE{University}{%
		Hoare:1971:CSI,%
		Hoare:1972:OST,%
		Hoare:1973:TMR,%
		Hoare:1986:MPI%
		}.
\NAMECITE{Unraveling}{%
		Hoare:2010:UCT%
		}.
\NAMECITE{USA}{%
		Abadi:2005:CCT,%
		Kapur:1992:ADC%
		}.
\NAMECITE{use}{%
		Dasgupta:1984:UHL,%
		Neuhold:1977:UHM,%
		Pritchard:1979:CPJ,%
		Stoller:1995:VPU%
		}.
\NAMECITE{used}{%
		Boyer:1996:APO%
		}.
\NAMECITE{Using}{%
		Hartog:2002:VPP,%
		Hooman:1992:CVR,%
		Sokolowski:1987:SHL,%
		Zhan:2019:UGC,%
		Bergstra:1984:PPI,%
		Chajed:2017:CFS,%
		Chisholm:1989:ARP%
		}.
\NAMECITE{UTP}{%
		Ribeiro:2019:UTP,%
		Wolff:2013:UTP,%
		Foster:2019:HRI,%
		Wu:2019:USC%
		}.


\NAMECITE{Value}{%
		deBoer:2021:CCR%
		}.
\NAMECITE{Vancouver}{%
		Lenzerini:2008:PTS%
		}.
\NAMECITE{variable}{%
		DeBoer:1997:HSC%
		}.
\NAMECITE{Variables}{%
		Feng:2021:QHL,%
		Kleymann:1999:HLA,%
		vonOheimb:2002:HLN,%
		Olderog:1984:CPP%
		}.
\NAMECITE{Variations}{%
		Dijkstra:1975:VTO,%
		Dijkstra:1982:VTO,%
		Hoare:1982:VTO%
		}.
\NAMECITE{varieties}{%
		Hoare:1989:VPL%
		}.
\NAMECITE{various}{%
		Makowsky:1989:WSO%
		}.
\NAMECITE{VDM}{%
		Bjorner:1990:VVZ,%
		Bjorner:1990:VVZ,%
		Coenen:1995:HLV%
		}.
\NAMECITE{verifiable}{%
		Hoare:1990:AAV%
		}.
\NAMECITE{Verification}{%
		Broy:2011:SSS,%
		Hoare:2008:VFG,%
		Hoare:2021:PSI,%
		Hooman:1992:CVR,%
		Huisman:2000:JPV,%
		Manna:2010:TVE,%
		Poskitt:2012:HSV,%
		Woodcock:2021:VGC,%
		Cocco:1982:MEH,%
		Dasgupta:1984:UHL,%
		Fetzer:1988:PVV,%
		Hoare:2002:APV,%
		Hoare:2009:PSI,%
		Homeier:1995:MVV,%
		Lifschitz:1984:VPG,%
		Makowsky:1989:WSO,%
		Neuhold:1977:UHM,%
		Pritchard:1979:CPJ,%
		Shaner:2007:MVH,%
		Szczepanska:1991:HLV%
		}.
\NAMECITE{verifications}{%
		Csirmaz:1981:PPV%
		}.
\NAMECITE{Verified}{%
		Hoare:2008:VST,%
		Meyer:2008:VST,%
		Bicarregui:2006:VSR,%
		Hoare:2006:IVS,%
		Hoare:2009:VSI,%
		Homeier:1995:MVV,%
		Hoare:2021:VSI,%
		Mller:2021:FFY%
		}.
\NAMECITE{verifier}{%
		Chlipala:2013:BSP%
		}.
\NAMECITE{Verifying}{%
		Hartog:2002:VPP,%
		Hoare:2003:TVC,%
		Hoare:2003:VCGa,%
		Hoare:2004:TVC,%
		Reus:2001:HCV,%
		Ridge:2009:VDS,%
		Stoller:1995:VPU,%
		Wing:1989:VAD,%
		Bicarregui:2006:VSR,%
		Hoare:2003:VC,%
		Hoare:2003:VCGb,%
		Hoare:2005:VCG,%
		Sousa:2016:CHL%
		}.
\NAMECITE{very}{%
		Fetzer:1988:PVV%
		}.
\NAMECITE{via}{%
		Huisman:2000:JPV,%
		Rehof:2010:ADS%
		}.
\NAMECITE{Viewpoint}{%
		Hoare:2009:VRA%
		}.
\NAMECITE{viii}{%
		Anonymous:1987:BRC%
		}.
\NAMECITE{Virtual}{%
		vonOheimb:2002:HLN%
		}.
\NAMECITE{Vision}{%
		Hoare:2008:VST%
		}.
\NAMECITE{Visions}{%
		Hoare:2004:VIF%
		}.
\NAMECITE{VSTTE}{%
		Meyer:2008:VST%
		}.
\NAMECITE{{{Vzaimode{{i}}}}}{%
		Khoar:1989:CVC%
		}.


\NAMECITE{W}{%
		Barron:1975:BRS,%
		Barth:1974:BRJ,%
		Boyer:2002:MEW,%
		Feijen:1990:BOB,%
		Lloyd:1974:BRS%
		}.
\NAMECITE{Was}{%
		Lewis:1997:BCI%
		}.
\NAMECITE{Watered}{%
		Olsen:1997:LWJ%
		}.
\NAMECITE{way}{%
		Hoare:1973:HLP%
		}.
\NAMECITE{Weak}{%
		Makowsky:1989:WSO%
		}.
\NAMECITE{Weakest}{%
		Hoare:1985:WP,%
		Hoare:1986:WPa,%
		Hoare:1986:WPb,%
		Hoare:1987:WP%
		}.
\NAMECITE{Weakly}{%
		Hoofman:1991:WEM%
		}.
\NAMECITE{WG}{%
		Meyer:2008:VST,%
		Hoare:1966:LWM%
		}.
\NAMECITE{Which}{%
		Clarke:1979:PLC,%
		Bergstra:1982:SNS,%
		Page:1989:SME%
		}.
\NAMECITE{while}{%
		Bergstra:1982:SNS,%
		Greif:1981:SSW,%
		Stirling:1988:GOG%
		}.
\NAMECITE{while-programs}{%
		Bergstra:1982:SNS%
		}.
\NAMECITE{{Whitehead}}{%
		Hoare:1979:CGW%
		}.
\NAMECITE{Whither}{%
		Naumann:2019:WSP%
		}.
\NAMECITE{widely}{%
		Boyer:1996:APO%
		}.
\NAMECITE{{Wijngaarden}}{%
		Hoare:1968:LVW%
		}.
\NAMECITE{{Windows}}{%
		Gozum:1997:LWC%
		}.
\NAMECITE{Windsor}{%
		Bottaci:2010:TAI%
		}.
\NAMECITE{Winner}{%
		Hoare:2016:PST%
		}.
\NAMECITE{{Wirth}}{%
		Simauti:1967:CCD%
		}.
\NAMECITE{Without}{%
		Hoare:1996:HDS,%
		Olderog:1984:CPP%
		}.
\NAMECITE{Work}{%
		Apt:2022:EWD,%
		Jones:2010:RWC%
		}.
\NAMECITE{Works}{%
		Jones:2021:TPL%
		}.
\NAMECITE{Workshop}{%
		Jones:2013:ICC%
		}.
\NAMECITE{world}{%
		Tennent:1991:CPW%
		}.
\NAMECITE{worth}{%
		Dijkstra:1999:FWT%
		}.
\NAMECITE{Writings}{%
		Dijkstra:1982:SWC%
		}.
\NAMECITE{Wybe}{%
		Apt:2022:EWD,%
		Hoare:2003:EWD%
		}.


\NAMECITE{Ya}{%
		Baer:1965:RPP%
		}.
\NAMECITE{Years}{%
		Apt:1981:TYH,%
		Hoare:2022:FYE,%
		McReynolds:1997:LBS,%
		Mller:2021:FFY,%
		Abdallah:2005:CSP,%
		Apt:1984:TYH,%
		Apt:2019:FYH,%
		Ashenhurst:1987:ATA%
		}.
\NAMECITE{Yes}{%
		Hoare:2004:YWT%
		}.
\NAMECITE{{Ynot}}{%
		Nanevski:2008:YDT%
		}.
\NAMECITE{{Yu.}}{%
		Baer:1965:RPP%
		}.


\NAMECITE{Z}{%
		Bjorner:1990:VVZ,%
		Morgan:1985:SSN,%
		Spivey:1989:ZNR%
		}.
\NAMECITE{Zurich}{%
		Meyer:2008:VST%
		}.