February 2001, 28pp.
Nonlocality is an intriguing aspect of quantum mechanics which has puzzled scientists since the seminal work of Einstein, Podolsky and Rosen in 1935: events may have simultaneous effects, no matter how far one from the other they occur. Here we use a programming language developed for quantum computation, qGCL, to formalize and reason about the most famous examples of this phenomenon. qGCL makes use of the modern programming techniques such as program refinement, abstraction and algebraic laws. Our formalism offers a unified rigorous treatment of various quantum systems, where all formal reasoning is accomplished by using algebraic laws rather than semantics, with corresponding simplicity and clarity.