Quipper: A Scalable Quantum Programming Language
arXiv:1304.3390 · doi:10.1145/2499370.2462177
Abstract
The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level of toy problems. We address this issue by introducing Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and can generate quantum gate representations using trillions of gates. It is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Quipper has proven effective and easy to use, and opens the door towards using formal methods to analyze quantum algorithms.
10 pages, PLDI 2013
References in corpus (5)
Cited by in corpus (44)
- Toward the first quantum simulation with quantum speedup
- ProjectQ: An Open Source Software Framework for Quantum Computing
- Quantum Risk Analysis
- Automated optimization of large quantum circuits with continuous parameters
- MQT Bench: Benchmarking Software and Design Automation Tools for Quantum Computing
- A Software Methodology for Compiling Quantum Programs
- Performing Quantum Computing Experiments in the Cloud
- Overview and Comparison of Gate Level Quantum Software Platforms
- A Deductive Verification Framework for Circuit-building Quantum Programs
- Formal Verification of Quantum Programs: Theory, Tools and Challenges
- Algorithm for the solution of the Dirac equation on digital quantum computers
- Predicting Good Quantum Circuit Compilation Options
- Formal Constraint-based Compilation for Noisy Intermediate-Scale Quantum Systems
- A Categorical Model for a Quantum Circuit Description Language (Extended Abstract)
- Toward Automatic Verification of Quantum Programs
- A tutorial introduction to quantum circuit programming in dependently typed Proto-Quipper
- Two linearities for quantum computing in the lambda calculus
- Quantivine: A Visualization Approach for Large-scale Quantum Circuit Representation and Analysis
- Realizability in the Unitary Sphere
- Hybrid quantum-classical circuit simplification with the ZX-calculus
- Reversible monadic computing
- Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model
- Enabling Accuracy-Aware Quantum Compilers using Symbolic Resource Estimation
- Deterministic Algorithms for Compiling Quantum Circuits with Recurrent Patterns
- Initial-State Dependent Optimization of Controlled Gate Operations with Quantum Computer
- Quantum types: going beyond qubits and quantum gates
- Advantages of a modular high-level quantum programming framework
- Grover's oracle for the Shortest Vector Problem and its application in hybrid classical-quantum solvers
- Locality-aware Pauli-based computation for local magic state preparation
- Automated Verification of Silq Quantum Programs using SMT Solvers
- A concrete model for a typed linear algebraic lambda calculus
- A lambda calculus for density matrices with classical and probabilistic controls
- A Biset-Enriched Categorical Model for Proto-Quipper with Dynamic Lifting
- Fractional Types: Expressive and Safe Space Management for Ancilla Bits
- The Quantum Monadology
- The Quantum Effect: A Recipe for QuantumPi
- High-Precision Multi-Qubit Clifford+T Synthesis by Unitary Diagonalization
- Generating Compilers for Qubit Mapping and Routing
- Encoding High-level Quantum Programs as SZX-diagrams
- A Quantum-Control Lambda-Calculus with Multiple Measurement Bases
- Classically Time-Controlled Quantum Automata: Definition and Properties
- Compositional Quantum Control Flow with Efficient Compilation in Qunity
- QSSA: An SSA-based IR for Quantum Computing
- Proto-Quipper with Reversing and Control