Algebra unifies calculi of programming, Part 1
We survey the well-known algebraic laws of sequential programming, and propose some less familiar laws for concurrent programming. On the basis of these laws, we derive the rules of a number of classical programming calculi, for example, those due to Hoare, Milner, Dijkstra, Back, Morgan, Kahn, Plotkin and Jones. The laws are simpler than each of the calculi, and yet stronger than all of them put together. We end with a discussion of the role of unification in Science and Engineering.
This is the first part of two related talks. The second part will be presented in the verification seminar on 22 Feb 2012.