| Reflections on the Work of C.A.R. Hoare 2010 Edition Contributor(s): Jones, Cliff B. (Editor), Roscoe, A. W. (Editor), Wood, Kenneth R. (Editor) |
|
 |
ISBN: 1447161521 ISBN-13: 9781447161523 Publisher: Springer OUR PRICE: $161.49 Product Type: Paperback - Other Formats Published: November 2014 |
| Additional Information |
| BISAC Categories: - Computers | History - Computers | Computer Science |
| Dewey: 004.09 |
| Physical Information: 0.9" H x 6.14" W x 9.21" (1.36 lbs) 430 pages |
| Descriptions, Reviews, Etc. |
| Publisher Description: ThisvolumehasitsoriginsinameetingheldatMicrosoftResearch, Cambridge, in April2009tocelebrateTonyHoare s75thBirthday(actually11Jan2009). Allthe technicalpapersexceptforthosewrittenbyAbramsky, Jackson, JonesandMeyer arebased sometimesclosely, sometimesnot onpresentationsgivenatthatme- ing. TheideaforthemeetingaroseinconversationsbetweenourselvesandAndrew HerbertofMicrosoft, whohostedatrulymemorableandhappyevent. ThemeetingwasorganisedbyourselvesandKenWood, withthe?nancials- portofMicrosoftResearchandFormalSystems(Europe)Ltd, andheldovertwo days. We wouldlike to recordparticularthanksto Angela Still of Microsoftfor makingallthelocalarrangementsatCambridgeandmuchmore: themeetingwould nothavehappenedwithouther. Whilethemajorityofthepapersinthisvolumearetechnical, weaskedauthorsto re?ectonthein?uenceofHoare sworkontheirown?eldsandtomakeappropriate remarksonit. Allthetechnicalpaperswererefereed. DiscussionswithWayneWheelerofSpringerinspiredthetwoofustowritethe scienti?cbiographyofHoarethatisthe?rstpaperinthisvolume. Thoughwehave bothknownTonywellformanyyears, wewereamazedathowmanydiscoveries abouthimwemadeduringtheprocessofwritingthisarticle. WewouldlikethankWayneandhisassistantSimonReesfortheirhelpinprep- ingthisvolumeaswellastheirpatience. Muchoftheworkingatheringthepapers, ensuringconsistencyofLaTeXstyles, etc., wasdonebyLucyLiofOxfordUniv- sityComputingLaboratoryandwethankherwarmly. Tragically, KenWood swifeLisadiedafteralongillnessinSeptember2009. Wededicatethisvolumetohermemory. January2010 CliffJones BillRoscoe ix Contents 1 Insight, InspirationandCollaboration. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 C. B. JonesandA. W. Roscoe 2 FromCSPtoGameSemantics. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 SamsonAbramsky 3 OnMereologiesinComputingScience. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 DinesBjorner 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 OnCSPandtheAlgebraicTheoryofEffects. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 333 RobvanGlabbeekandGordonPlotkin 16 CSPisExpressiveEnoughfor . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 371 A. W. Roscoe 17 TheTokeneerExperiments. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 405 JimWoodcock, EmineGokc ], eAydal, andRodChapman Chapter1 Insight, InspirationandCollaboration C. B. JonesandA. W. Roscoe Abstract TonyHoare smanycontributionstocomputingsciencearemarkedby insightthatwasgroundedinpracticalprogramming. Manyofhispapershavehada profoundimpactontheevolutionofour?eld;theyhavemoreoverprovidedasource ofinspirationtoseveralgenerationsofresearchers. Weexaminethedevelopmentof hisworkthroughareviewofthedevelopmentofsomeofhismostin?uentialpieces ofworksuchasHoarelogic, CSPandUnifyingTheories. 1. 1 Introduction To many who know Tony Hoare only through his publications, they must often looklikepolishedgemsthatcomefromamindthatrarelymakesfalsesteps, nor evenperhapshastoworkattheircreation. Assooften, thisimpressionisafurther complimenttosomeonewhoactuallyaddstoveryhardworkandmanydiscarded attempts the ?nal polish thatmakes complexideas relatively easy for the reader tocomprehend. Asindicatedonpagexiof HJ89], hisideastypicallygothrough manyrevisions. ThetwoauthorsofthecurrentpapereachhadthehonourofTonyHoaresuperv- ingtheirdoctoralstudiesinOxford. Theyknowat?rsthandhiskindandgenerous styleandwillcountitasanachievementifthispapercanconveysomethingofthe workingmethodsofsomeonebigenoughtoeschewcompetitionandpointscoring. Indeedit willbe apparentfromthe followingsectionshowoften, havingstarted somenewwayofthinkingorexcitingideas, hehappilyleavestheirexplorationand developmenttoothers. Wehavebothbene?tedpersonallyfromthis. C. B. Jones( ) SchoolofComputingScience, NewcastleUniversity, UK e-mail: cliff. jones@ncl. ac. uk A. W. Roscoe OxfordUniversityComputingLaboratory, UK e-mail: Bill. Roscoe@comlab. ox. ac. uk C. B. Jonesetal. (eds. ), Re?ection |