Rod Bustall: In Memoriam
J Strother Moore, Gordon Plotkin, David Rydeheard, Don Sannella

TL;DR
This paper memorializes Rod Burstall, highlighting his pioneering contributions to programming languages, formal methods, and the mathematical foundations of software development over his 40-year career.
Contribution
It details Rod Burstall's novel work on programming language design, formal verification, algebraic specifications, and the development of proof systems, which significantly influenced computer science.
Findings
Developed the POP-2 programming language and the HOPE language.
Pioneered the connection between program proof and modal logic.
Led early work on program transformation and proof-carrying code.
Abstract
This is an obituary of Rod Burstall, written in his honour. Rod was a prominent computer scientist whose contributions span over forty years. Most of his career was spent at Edinburgh University. He lead the team programming Freddy, the first hand-eye assembly robot, with much of his effort being devoted to the development of the POP-2 programming language. He became interested in a mathematical approach to software development: he recognised the central role of structural induction; his work on reasoning about mutable data structures was an influential precursor of separation logic; he was the first to point out the connection between program proof and modal logic; and he was responsible for the idea that stores are mappings from locations to their contents. As part of his quest for correctness of programs, Rod, with John Darlington, undertook the first major work on program…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
