It allows users to apply basic quantum operations (unitary gates and branching SQIR is a deliberately low-level language, designed for optimization and verification. Which features in ongoing work as a target for the VOQC compiler. To that end, we will begin by introducing the small quantum language SQIR, Particular interest to POPL attendees: How do we program quantum computersĪnd how do we prove that these programs behave as desired? The second half of the tutorial (SQIMP.v) will turn towards subjects of How do we measure qubits and mathematically represent the outcomes?.What operations are valid in a quantum context?.What are superposition and entanglement?.What are qubits and how do we represent them?.The first half of the tutorial (Qubit.v and Multiqubit.v) willįocus on the basics of quantum computing. This will allow attendees to play with quantum systems,įamiliarizing themselves with their advantages and limitations.
We will take the opposite approach, explaining quantum computing in terms of a simple mathematical theory that we embed in the Coq proof assistant, relying on nothing but Coq’s real numbers and a lightweight formalization of complex numbers and matrix algebra. Popular presentations of quantum mechanics often portray quantum mechanics as “weird” or “spooky” and fundamentally difficult for laypeople, or even mathematicians and physicists, to wrap their heads around.
#Coq tutorial how to#
Beyond introducing attendees to the basics of quantum computing, it will introduce a simple quantum programming language, called SQIR, and demonstrate how to verify the correctness of quantum programs. This tutorial will introduce quantum computing to a programming languages audience through use of the Coq proof assistant. With Kesha Hietala and Kartik Singhal Materials
0 kommentar(er)
