Toward A Quantum Programming Language for Higher Level Formal Verification

on YouTube ↗15m

" summary

A new high-level language called quantum one targets formal verification by representing program state as superpositions of expressions and by encoding duplication as sharing rather than cloning. All definitions are formalized in the cockproof system. The team builds a compiler to squire that translates discard-free code to unitary circuits and non-discard-free code to circuits with measurements; output circuits are correct but blow up with swap gates. A verified compiler and proofs (type soundness, normalization) remain unfinished; vox optimizer can reduce the generated overhead.

AI-written summary · about

" chapters (6)

1. 0:00Introduction
2. 1:21Quantum One Syntax
3. 5:24Quantum One Semantics
4. 8:09Quantum One Typing
5. 10:37Quantum Compiler
6. 12:18Additional Features

" related talks

• 22mCoqQ: Foundational Verification of Quantum ProgramsGilles Barthe, Li Zhou, Mingsheng Ying, Pierre-Yves Strub, Junyi Liu · POPL 2023
• 13mQbC: Quantum Correctness by ConstructionAnurudh Peduri, Ina Schaefer, Michael Walter · OOPSLA 2025
• 42mQuantum program analysis: Verification and TestingNengkun Yu · WQS 2024
• 21mToward Certified Quantum ProgrammingChristophe Chareton · PLanQC 2020
• 40mDemocratizing quantum formal verification: the path-sum wayChristophe Chareton · PLanQC 2026
• 22mEfficient Formal Verification of Quantum Error Correcting ProgramsLi Zhou, Mingsheng Ying, Qifan Huang, Wang Fang, Mengyu Zhao · PLDI 2025
• 29mA Verified Optimizer for Quantum CircuitsMichael Hicks, Robert Rand, Kesha Hietala, Xiaodi Wu, Shih-Han Hung · POPL 2021
• 24mA Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum LanguagesKesha Hietala, Kartik Singhal · PLanQC 2020