Richard Bornat and Raja Nagarajan

Analysis of Quantum Systems using Programming Languages/Tools

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. The successful construction of a large-scale quantum
computer may be some years away, but there has been significant
investment recently by companies like IBM, Microsoft and
Google. Quantum communication and cryptography, on the other hand, is
a mature field. Products are commercially available, networks have
been built and a satellite has been launched by China to provide
secure quantum communication.

It is well known from experience with classical (non-quantum) 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, we will provide a gentle introduction to quantum
computing and give an overview of some of our ongoing work on using
programming language based techniques and tools for formal analysis of
quantum protocols and, eventually, their implementations. This work is
part of a research project, joint with Jaap Boender and Florian
Kammueller.