Reflections on the Work of C.A.R. Hoare

. . . . . . . 33 SamsonAbramsky 3 OnMereologiesinComputingScience. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 DinesBjørner 4 Roles,Stacks,Histories:ATripleforHoare. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 Johannes Borgstrom, ¿ Andrew D. Gordon, andRiccardoPucella 5 ForwardwithHoare. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 MikeGordonandHel ¿ene ` Collavizza 6 ProbabilisticProgrammingwithCoordination. . . . . . . . . . . . . . . . . . . . . . . . . . . 123 HeJifeng 7 TheOperationalPrincipleandProblemFrames. . . . . . . . . . . . . . . . . . . . . . . . . 143 MichaelJackson 8 TheRoleofAuxiliaryVariablesintheFormal DevelopmentofConcurrentPrograms. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 167 C. B. Jones 9 AvoidaVoid:TheEradicationofNullDereferencing. . . . . . . . . . . . . . . . . . . . 189 BertrandMeyer,AlexanderKogtenkov,andEmmanuelStapf 10 UnfoldingCSP. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213 MikkelBundgaardandRobinMilner xi xii Contents 11 Quicksort:CombiningConcurrency,Recursion, andMutableDataStructures. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 229 DavidKitchin,AdrianQuark,andJayadevMisra 12 TheThousand-and-OneCryptographers. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 255 A. K. McIverandC. C. Morgan 13 On Process-AlgebraicExtensions of Metric TemporalLogic. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 283 ChristophHaase,Joel ¿ Ouaknine,andJamesWorrell 14 FunwithTypeFunctions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 301 OlegKiselyov,SimonPeytonJones,andChung-chiehShan 15 OnCSPandtheAlgebraicTheory

Written in honor of Sir Tony Hoare's 75th birthday Discusses the influence of Sir Tony Hoare's work on current research Provides a scientific biography of Sir Tony Hoare

Insight, Inspiration and CollaborationC. B. Jones and A. W. RoscoeFrom CSP to Game SemanticsSamson AbramskyOn Mereologies in Computing ScienceDines BjørnerRoles, Stacks, Histories: A Triple for HoareJohannes Borgstrom, Andrew D. Gordon and Riccardo PucellaForward with HoareMike Gordon and Helene CollavizzaProbabilistic Programming with CoordinationHe JifengThe Operational Principle and Problem FramesMichael JacksonThe Role of Auxiliary Variables in the Formal Development of Concurrent ProgramsCliff B. JonesAvoid a Void: The Eradication of Null DereferencingBertrand Meyer, Alexander Kogtenkov and Emmanuel StapfUnfolding CSPMikkel Bundgaard and Robin MilnerQuicksort: Combining Concurrency, Recursion, and Mutable Data StructuresDavid Kitchin, Adrian Quark and Jayadev MisraThe Thousand-and-One CryptographersAK McIver and CC MorganOn Process-algebraic Extensions of Metric Temporal LogicChristoph Haase, Joel Ouaknine and James WorrellFun with Type FunctionsOleg Kiselyov, Simon Peyton Jones and Chung-chieh ShanOn CSP and the Algebraic Theory of EffectsRob van Glabbeek and Gordon PlotkinCSP is Expressive Enough for ?A.W. RoscoeThe Tokeneer ExperimentsJim Woodcock, Emine Gokce Aydal and Rod Chapman