Point of contact
- Pablo Arrighi, LMF
- Marc Baboulin, LISN
- Sébastien Bardin, CEA
- Virgile Prevosto, CEA List
- Benoît Valiron, LMF
- Renaud Vilmart, LMF
Summary
Even though a real quantum processor is not there yet, there are already algorithms and programming languages dedicated to quantum computing, as well as proposals for verifying their properties.
Similarly, massively distributed applications among untrusted actors (blockchains and smart contracts) pose interesting problems in terms of verification.
A few references
- Christophe Chareton et al. Qbricks: formal verification in quantum computing. In 1st International Workshop on Programming Languages for Quantum Computing. 2020
- Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle and Benoit Valiron. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. In Proceedings of the 30th European Symposium on Programming (ESOP 2021)
- Timothée Goubault de Brugière, Marc Baboulin Benoît Valiron Cyril Allouche, Synthesizing Quantum Circuits via Numerical Optimization, CCS 2019: Computational Science – ICCS 2019 pp 3-16
- Pablo Arrighi, Alejandro Dı́az-Caro, Benoı̂t Valiron, The vectorial λ–calculus, Information & Com-
putation 254, 105–139, (2017), Pre-print arXiv :1012.4032. - Pablo Arrighi, An overview of Quantum Cellular Automata, Natural Computing 18, 885, (2019).
Pre-print arXiv :1904.12956. - Pablo Arrighi, Simon Martiel, Quantum Causal Graph Dynamics., Phys. Rev. D. 96(2), 024026,
(2017). Pre-print arXiv :1607.06700.