Quantum computing offers the possibility of efficient algorithms for hard computational problems such as factorization, although practical quantum computers are a long way in the future. Quantum cryptography offers the possibility of secure communication even in the presence of quantum computers; quantum cryptographic systems have been demonstrated in practical situations and are commercially available. Other aspects of quantum communication have been in the news recently, for example "teleportation of the quantum state of an atom". These are topics of growing interest to computing scientists, and we can be sure that they will form the basis for important future technologies.
My research focuses on formally verifying quantum communication and cryptographic protocols, and especially protocols which combine quantum and classical (non-quantum) communication, by applying techniques which have been successful for verifying classical communication protocols. The approach is based on a modelling language called Communicating Quantum Processes (CQP) which is still at an early stage of development.
The aims of the project are:
The project would suit a student with interests in mathematics and/or physics, although an understanding of quantum theory is NOT a prerequisite.
Quantum computing offers the possibility of efficient algorithms for hard computational problems such as factorization, although practical quantum computers are a long way in the future. Quantum cryptography offers the possibility of secure communication even in the presence of quantum computers; quantum cryptographic systems have been demonstrated in practical situations and are commercially available. Other aspects of quantum communication have been in the news recently, for example "teleportation of the quantum state of an atom". These are topics of growing interest to computing scientists, and we can be sure that they will form the basis for important future technologies. The aim of this project is to produce animated demonstrations of some of the most significant quantum cryptographic and communication protocols. These demonstrations could be used as the basis of a tutorial introduction to quantum communication and cryptography. They could be implemented as a standalone application, or as a web site using some suitable technology. It might be possible to make use of an existing toolkit for simulation of quantum systems, for example QuCrypt. Ideally the demonstrations would be configurable with different parameters or variations of the protocols.
The project would suit a student with interests in mathematics and/or physics, although an understanding of quantum theory is NOT a prerequisite.
Session types allow complex protocols to be specified and, in principle, typechecked. For example, the type of a channel might specify that the first message is a string, the second message is an integer, and so on. More sophisticated types describe branching possibilities, so that the content of one message may affect the types of subsequent messages. In a language with session types, the programmer (implementing a client, say) would be able to declare the type of the channel which connects to the server, and the compiler would check that the messages sent and received by the client are compatible with this type and obey the correct protocol.
Session types have been studied and implemented in small idealised languages, and the next step is to work out how to put them into more realistic programming languages. The project will begin by adding session types to a simple imperative language, implementing a typechecker and compiler (probably compiling into Java), and experimenting with programming in the language. There is huge scope for extension, and investigating the interactions between session types and programming language features such as arrays, functions, objects, and threads.
There is also considerable interest at the moment in the idea of using session types to specify protocols for web services: there is a link with the growing area of "web choreography". An interested student could investigate this connection and develop case-studies in which session types could be applied.