  We present a formalization in Isabelle/HOL of quantum projective
measurements, a class of measurements involving orthogonal projectors that is
frequently used in quantum computing. We also formalize the CHSH inequality, a
result that holds on arbitrary probability spaces, which can used to disprove
the existence of a local hidden-variable theory for quantum mechanics.
