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