This research line aims at scaling up classical computer programming technology to quantum computing, contributing to a better understanding of the mathematics of quantum programming and developing formal methodologies and tools aiding in the conception, validation, verification, and construction of quantum programs.
Our research addresses a number of challenges emerging from the conceptual complexity of quantum physics phenomena and the consequent restrictions imposed to the quantum computing models (reversibility of the operations, the no-cloning theorem and decoherence). Moreover, real world quantum computing techniques are becoming increasingly complex: they can involve interaction with classical systems, encompass decoherence and stochastic effects or they can be completely analog, by the direct use of timed-evolutionary Hamiltonians. Such diversity poses relevant challenges to finding “the right theories” and developing suitable semantic analysis tools — the main aim of this proposal.
Research topics in this line:
– Quantum programming languages and calculi
– Dynamic logic for quantum algorithms
– Proof theory for quantum logic
– Categorical quantum semantics