A Small Quantum Intermediate Representation

The compiler and interpreter for the high-level quantum programming language Qunity, based on compositional quantum control flow.

Coq library for reasoning about quantum programs

A repository of lean problems for GPT-4 to attempt

Verifying the ZX Calculus

The working directory for the development of the QRK

Coq library for reasoning about quantum programs

A Coq module for working with linear typing contexts.

A Small Quantum Intermediate Representation

A quantum circuit language and formal verification tool

An introductory tutorial for the Coq proof assistant.

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

Adding linear types to Haskell in the style of Linear/Non-Linear (LNL) logic

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]