Carroll Morgan

Charles Carroll Morgan (born 1952) is an American/Australian computer scientist who moved from the US to Australia in his early teens. He completed his education there (high school, university, several years in industry), including a Doctor of Philosophy (Ph.D.) degree from the University of Sydney, and then moved to the United Kingdom in the early 1980s. In 2000, he returned to Australia.

During the 1980s and 1990s, Morgan was based at the Oxford University Computing Laboratory in England as a researcher and lecturer working in the area of formal methods, and was a Fellow of Pembroke College. Having been influenced by the Z notation of Jean-Raymond Abrial, he authored Programming from Specifications as an attempt to combine the high-level specification aspects of Z, with the rigorous computer program derivation methods of Edsger W. Dijkstra. His treatment concentrated on elementary program constructs to make the material accessible to undergraduates in their early years. Some of the ideas there were later incorporated as elements of the B-Method by Abrial, when Abrial returned to Oxford in the last half of the 1980s.

Together with Annabelle McIver, Morgan later authored Abstraction, Refinement and Proof for Probabilistic Systems, in which the same themes were pursued for probabilistic programs. His more recent text (with five others) The Science of Quantitative Information Flow extends the same themes further, to program security.

His latest text Formal Methods, Informally: How to write programs that work targets early-in-course computer-science students, aiming to teach the principles of rigorous program construction without requiring formal logic first.

Morgan is now professor emeritus in the School of Computer Science and Engineering at the University of New South Wales, a Senior Principal Researcher at Trustworthy Systems and an Honorary Professor at Macquarie University, all three in Australia. His main research interests are probabilistic models for computer security and concurrency. He is a known proponent of a formalized approach to program development called the refinement calculus. including IFIP Working Group 2.1 on Algorithmic Languages and Calculi, which specified, maintains, and supports the programming languages ALGOL 60 and ALGOL 68.

Books Carroll has authored or co-authored the following books:

Programming from Specifications (1990, 2nd ed. 1994). Prentice Hall, Series in Computer Science. Abstraction, Refinement and Proof for Probabilistic Systems (2005), with Annabelle McIver. Springer, Monographs in Computer Science. The Science of Quantitative Information Flow (2020), with Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi, and Geoffrey Smith. Springer, Information Security and Cryptography. Formal Methods, Informally: How to Write Programs that Work (2026). Cambridge University Press.