Contents

# Contents

## Idea

CoqQ [Ying et al. (2022)] is the name of a domain specific quantum programming language which is embedded in the (classical) proof assistant Coq and used for studying software verification of quantum programs (such as quantum circuits but also more generally).

CoqQ uses an analytic formalization of (finite dimensional) Hilbert spaces (from Mahboubi & Tassi (2021)) in order to formalize quantum gates as actual linear maps between these.

## References

Created on November 12, 2022 at 09:52:38. See the history of this page for a list of all contributions to it.