The novel field of quantum computation and quantum
information has gathered significant impetus in the last few
years, and it has the potential to radically impact the future of
information technology. While the successful construction of a
large-scale quantum computer may be some years away,
equipment for quantum cryptography is commercially available
and a satellite has been launched by China to provide secure
quantum communication. However, it is well known from experience
with classical systems that it is notoriously difficult to achieve robust and
reliable implementations. Techniques based on
formal verification are now widely used by industry to ensure that
classical systems meet their specifications. In this talk, I
will introduce quantum programming/specification languages and give
an overview of our ongoing work on formal methods for modelling and analysis of
quantum protocols and, eventually, their implementations.
