The laws of Occam programming (Q2640348)

The authors describe an equational axiomatization of the semantics of OCCAM. They show that WHILE-free programs have a normal form, such that two programs are semantically equivalent if and only if their normal forms are syntactically equivalent. This shows that their equational axiomatization, together with an induction axiom, is a sound and complete proof system for proving the equivalence of OCCAM programs. The paper is very clearly written.