quantumlib

Coq library for reasoning about quantum programs

https://github.com/inqwire/quantumlib

Science Score: 44.0%

This score indicates how likely this project is to be science-related based on various indicators:

  • CITATION.cff file
    Found CITATION.cff file
  • codemeta.json file
    Found codemeta.json file
  • .zenodo.json file
    Found .zenodo.json file
  • DOI references
  • Academic publication links
  • Academic email domains
  • Institutional organization owner
  • JOSS paper metadata
  • Scientific vocabulary similarity
    Low similarity (12.2%) to scientific vocabulary
Last synced: 10 months ago · JSON representation ·

Repository

Coq library for reasoning about quantum programs

Basic Info
  • Host: GitHub
  • Owner: inQWIRE
  • License: other
  • Language: Rocq Prover
  • Default Branch: main
  • Homepage:
  • Size: 2.67 MB
Statistics
  • Stars: 39
  • Watchers: 7
  • Forks: 12
  • Open Issues: 7
  • Releases: 6
Created almost 5 years ago · Last pushed 11 months ago
Metadata Files
Readme Changelog License Citation

README.md

QuantumLib

CI coqdoc

QuantumLib is a Coq library for reasoning about quantum programs. It was co-developed with (and is used in) several other projects in inQWIRE including QWIRE, SQIR, and VyZX.

Compilation

QuantumLib is currently compatible with Coq 8.16 -- 8.19.

This project requires opam & dune to be installed.

Install dune using opam install dune

To compile run make all.

Stable versions of QuantumLib may be installed using opam install coq-quantumlib

Using With Other Projects

Official Release

To install the official release of QuantumLib, run the following. opam repo add coq-released https://coq.inria.fr/opam/released opam update opam install coq-quantumlib

Dev

To install the development version of QuantumLib, run opam pin coq-quantumlib https://github.com/inQWIRE/QuantumLib.git. This should allow you to import QuantumLib files into other Coq files. To pull subsequent updates, run opam install coq-quantumlib. When importing/exporting specific files, refer to QuantumLib files as QuantumLib.FILENAME.

Directory Contents

Auto-generated documentation is available at https://inqwire.github.io/QuantumLib/toc.html.

  • Complex.v - Definition of Complex numbers, extending Coquelicot's.
  • Ctopology.v - A topology of open/closed sets is defined for the complex numbers, with lemmas about compactness.
  • DiscreteProb.v - Theory of discrete probability distributions and utility to describe running a quantum program ("apply_u") and sampling from the output distribution.
  • Eigenvectors.v - A continuation of VecSet.v, this file contains more linear algebra that is sort of specific to quantum.
  • FTA.v - This file is mostly just a messy proof of the fundamental theorem of algebra.
  • Matrix.v - Definition of matrices of complex numbers, associated lemmas and automation.
  • Measurement.v - Useful predicates for describing the result of measurement.
  • Pad.v - Definition of "pad" function to extend a matrix to a larger space.
  • Permutations.v - Facts about permutation matrices.
  • Polar.v - Defining polar complex numbers and showing that they are isomorphic to rectangular complex numbers.
  • Polynomial.v - Definition of polynomials and corresponding lemmas.
  • Prelim.v - Basic utility definitions and proofs.
  • Proportional.v - Definition of equality up to a global phase.
  • Quantum.v - Definitions of and proofs about common matrices used in quantum computing.
  • RealAux.v - Supplement to Coq's axiomatized Reals.
  • VecSet.v - More advanced linear algebra definitions such as linear independence, invertability, etc. and corresponding lemmas.
  • VectorStates.v - Abstractions for reasoning about quantum states as vectors.

Owner

  • Name: INQWIRE
  • Login: inQWIRE
  • Kind: organization

Verified Software for the Computers of Tomorrow

Citation (CITATION.cff)

cff-version: 1.2.0
message: "If you use this software, please cite it as below."
title: "INQWIRE QuantumLib"
abstract: "QuantumLib is a Coq library for reasoning about quantum programs."
authors:
  - name: "The INQWIRE Developers"
version: 1.3.0
date-released: 2022-01-06
license: MIT
repository-code: "https://github.com/inQWIRE/QuantumLib"

GitHub Events

Total
  • Create event: 3
  • Release event: 1
  • Issues event: 3
  • Watch event: 7
  • Delete event: 2
  • Issue comment event: 2
  • Push event: 8
  • Pull request review comment event: 2
  • Pull request event: 3
  • Pull request review event: 4
  • Fork event: 1
Last Year
  • Create event: 3
  • Release event: 1
  • Issues event: 3
  • Watch event: 7
  • Delete event: 2
  • Issue comment event: 2
  • Push event: 8
  • Pull request review comment event: 2
  • Pull request event: 3
  • Pull request review event: 4
  • Fork event: 1

Issues and Pull Requests

Last synced: 10 months ago

All Time
  • Total issues: 16
  • Total pull requests: 32
  • Average time to close issues: 28 days
  • Average time to close pull requests: 22 days
  • Total issue authors: 6
  • Total pull request authors: 9
  • Average comments per issue: 1.69
  • Average comments per pull request: 1.38
  • Merged pull requests: 26
  • Bot issues: 0
  • Bot pull requests: 0
Past Year
  • Issues: 3
  • Pull requests: 0
  • Average time to close issues: N/A
  • Average time to close pull requests: N/A
  • Issue authors: 1
  • Pull request authors: 0
  • Average comments per issue: 0.33
  • Average comments per pull request: 0
  • Merged pull requests: 0
  • Bot issues: 0
  • Bot pull requests: 0
Top Authors
Issue Authors
  • khieta (7)
  • letouzey (3)
  • jakezweifler (3)
  • fvoichick (1)
  • adrianleh (1)
  • kylechui (1)
Pull Request Authors
  • YoungchanCho (8)
  • jakezweifler (7)
  • k4rtik (6)
  • adrianleh (5)
  • caldwellb (4)
  • wjbs (4)
  • bhaktishh (2)
  • khieta (2)
  • rnrand (1)
  • lczielinski (1)
Top Labels
Issue Labels
nice to have (3) documentation (1) performance bug (1) good first issue (1) bug (1) enhancement (1)
Pull Request Labels
bug (2)

Packages

  • Total packages: 2
  • Total downloads: unknown
  • Total dependent packages: 0
    (may contain duplicates)
  • Total dependent repositories: 0
    (may contain duplicates)
  • Total versions: 16
proxy.golang.org: github.com/inqwire/quantumlib
  • Versions: 8
  • Dependent Packages: 0
  • Dependent Repositories: 0
Rankings
Dependent packages count: 5.4%
Average: 5.5%
Dependent repos count: 5.7%
Last synced: 11 months ago
proxy.golang.org: github.com/inQWIRE/QuantumLib
  • Versions: 8
  • Dependent Packages: 0
  • Dependent Repositories: 0
Rankings
Dependent packages count: 5.4%
Average: 5.5%
Dependent repos count: 5.7%
Last synced: 11 months ago

Dependencies

.github/workflows/coq-action.yml actions
  • actions/checkout v2 composite
  • coq-community/docker-coq-action v1 composite