Point of contact
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
- Palina Tolmach et al. A Survey of Smart Contract Formal Specification and Verification
- Luís Pedro Arrojado da Horta et al. WhylSon: Proving your Michelson Smart Contracts in Why3. In 2nd International Workshop on Formal Methods for Blockchains. 2020
- Zeinab Nehai, François Bobot. Deductive Proof of Industrial Smart Contracts Using Why3. In 1st International Workshop on Formal Methods for Blockchains. 2019
- Sylvain Conchon, Alexandrina Korneva, Fatiha Zaïdi Verifying Smart Contracts with Cubicle. In 1st International Workshop on Formal Methods for Blockchains. 2019
- Christophe Chareton et al. Qbricks: formal verification in quantum computing. In 1st International Workshop on Programming Languages for Quantum Computing. 2020
- 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.