We present voqc , the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called sqir , a small quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of sqir programs. sqir programs denote complex-valued matrices, as is standard in quantum computation, but we treat matrices symbolically to reason about programs that use an arbitrary number of quantum bits. sqir ’s careful design and our provided automation make it possible to write and verify a broad range of optimizations in voqc , including full-circuit transformations from cutting-edge optimizers.

More from our Archive

• DOI: 10.3390/systems11070329 2023

  Smarter and Prosperous: Digital Transformation and Enterprise Performance

  Da Gao, Zhiliang Yan, Xiaotian Zhou, Xinlin Mo

• DOI: 10.3390/systems11070351 2023

  Harnessing the Power of ChatGPT for Automating Systematic Review Process: Methodology, Case Study, Limitations, and Future Directions

  Ahmad Alshami, Moustafa Elsayed, Eslam Ali, Abdelrahman E. E. Eltoukhy, Tarek Zayed

• DOI: 10.1002/spe.3237 2023

  Managing data replication and distribution in the fog with FReD

  Tobias Pfandzelter, Nils Japke, Trever Schirmer, Jonathan Hasenburg, David Bermbach

• DOI: 10.3390/systems11070336 2023

  Evaluation of Tourism Ecological Security and Its Driving Mechanism in the Yellow River Basin, China: Based on Open Systems Theory and DPSIR Model

  Xiaorong He, Chaoyue Cai, Jizhi Shi

• DOI: 10.3390/systems11070348 2023

  Failure Mode and Effect Analysis with a Fuzzy Logic Approach

  José Jovani Cardiel-Ortega, Roberto Baeza-Serrato

• DOI: 10.1002/cnm.3750 2023

  Mandibular bone remodeling around osseointegrated functionally graded biomaterial implant using three dimensional finite element model

  Sameh Elleuch, Hanen Jrad, Mondher Wali, Fakhreddine Dammak

• DOI: 10.1049/ipr2.12854 2023

  Image segmentation technology based on transformer in medical decision‐making system

  Keke He, Fangfang Gou, Jia Wu

• DOI: 10.3390/systems11070359 2023

  Post-COVID-19 Recovery: An Integrated Framework of Construction Project Performance Evaluation in China

  Han-Sen Guo, Ming-Xin Liu, Jin Xue, Izzy Yi Jian, Qian Xu, Qian-Cheng Wang

• DOI: 10.1177/00375497231183722 2023

  A review on simulation-based metamodeling in emergency healthcare: methodology, applications, and future challenges

  Fatima-Zahra Sahlaoui, Lina Aboueljinane, Maria Lebbar

• DOI: 10.1145/3607471 2023

  Co-lexicographically Ordering Automata and Regular Languages - Part I

  Nicola Cotumaccio, Giovanna D’Agostino, Alberto Policriti, Nicola Prezza