Dynamic-logical approaches to Quantum Computation
|
Supervisor |
|
|
Suitable for |
Abstract
The project is to extend and improve on my recent work on developing a quantum version of Dynamic Logic (itself an improved version of Hoare logic), in order to provide uniform logical methods for proving correctness of quantum protocols. The main thing to be added to the above-mentioned work is a way of reasoning about local, agent-dependent information, to answer such questions as: what does Bob know after Alice has teleported a qubit to him, but before she sent him the results of her local measurements? This could be done e.g. by combining quantum dynamic logic with my work on logics for multi-agent information flow.
Background Needed
This project assumes some familiarity with, or a willingness and ability to quickly learn, some basic notions of Quantum Computation and of Modal Logic.