@@ -181,7 +181,7 @@ IT MAY BE BEST THAT WE AVOID ANYTHING THAT SUGGESTS A GIANT OCTOPUS SPRAWLING OV
For classical programs, modern compiler toolchains such as LLVM\footnote{%
The LLVM Compiler Infrastructure, \url{http://llvm.org}}
decouple high-level programming from different hardware platforms, allowing for easy and customisable cross-compilation.
Building on recent developments in the theory and application of the \zxcalculus~\cite{BH-2017,NW-2017,JPV-2018,DKPdW-2019}, the opportunity exists to develop a more ambitious version of the LLVM concept for quantum computing, bringing forward the day that quantum computers can be exploited for practical application.
Building on recent developments in the theory and application of the \zxcalculus~\cite{BH-2017,HFW,JPV-2018,DKPdW-2019}, the opportunity exists to develop a more ambitious version of the LLVM concept for quantum computing, bringing forward the day that quantum computers can be exploited for practical application.
}
\paragraph{Targeted breakthrough:}
...
...
@@ -228,7 +228,7 @@ easily run existing programs, and future programming languages automatically gai
Coecke2017Picturing-Quant}, and can be viewed in two distinct ways: either (i)~as a formal axiomatic theory which encodes the properties of complementary observables in categorical algebra, or (ii)~as a symbolic notation for tensor networks representing quantum states and linear operators.
Terms in the \zxcalculus are labelled graphs; equations in the calculus are reified as a small number of graph rewrite rules.
This equational theory is frequently more tractable than working explicitly with matrix representations.
Recently, members of our consortium developed versions of the \zxcalculus which were complete for Clifford+T computations~\cite{Jeandel2017A-Complete-Axio,NW-2018} and for quantum computations including CNOTs and arbitrary single-qubit gates~\cite{NW-2017,JPV-2018}.
Recently, members of our consortium developed versions of the \zxcalculus which were complete for Clifford+T computations~\cite{Jeandel2017A-Complete-Axio,NW-2018} and for quantum computations including CNOTs and arbitrary single-qubit gates~\cite{HFW,JPV-2018}.
This means that one can formally prove every equality of quantum circuits in these gate models through the application of a small number of relatively simple rules for rewriting tensors.
This stunning achievement opens the door to many
new possibilities for optimisation and verification of quantum
...
...
@@ -472,7 +472,7 @@ to achieving our goal of supporting multiple targets.
The \dzxc system}
will retain the mature and effective formal tensor language of
the \zxcalculus at its heart, ensuring semantic soundness, logical
and allowing us to leverage techniques from earlier work (cf.~\texttt{quantomatic}~\cite{Kissinger2015Quantomatic:-A-} and~\texttt{PyZX}~\cite{DKPdW-2019}).}%, as well as new techniques developed as part of this project,
This denotational kernel specifies the
...
...
@@ -805,7 +805,7 @@ As well as the \zx terms to translate, this will take as input a specification t
Recent breakthroughs in the theory of the \zx-calculus
\cite{Jeandel2017A-Complete-Axio,NW-2017}, have shown that whenever two
\cite{Jeandel2017A-Complete-Axio,HFW}, have shown that whenever two
\zxcalculus diagrams describe the same linear operator, then one can be
transformed into the other using just a finite set of local,
diagrammatic transformations.
...
...
@@ -1988,7 +1988,7 @@ and non-locality in categorical quantum mechanics. LiCS 2012. IEEE Computer Soci
(2) ---. The ZX-calculus is complete for the single-qubit Clifford+T group. EPTCS 172. arXiv:1412.8553.
(3) --- and A.~Kissinger. ZH: A Complete Graphical Calculus for Quantum Computations Involving Classical Non- linearity. QPL 2018. arXiv: 1805.02175.}
\textbf{Prof.\ Bob Coecke} is Professor of Quantum Foundations, Logics and Structures, and pioneered categorical and diagrammatic methods for quantum computing (1), and \zxcalculus\ in particular (with Duncan) (2). He is/has supervised approx.~50 PhD students, which include Hadzisasanivic, Ng and Wang who proved universal completeness of the \zx-calculus \cite{NW-2017}, and included Backens who proved stabiliser completeness \cite{1367-2630-16-9-093021}. He co-authored \em Picturing Quantum Processes \em (3), which presents diagrammatic methods for quantum computing to a broader audience.
\textbf{Prof.\ Bob Coecke} is Professor of Quantum Foundations, Logics and Structures, and pioneered categorical and diagrammatic methods for quantum computing (1), and \zxcalculus\ in particular (with Duncan) (2). He is/has supervised approx.~50 PhD students, which include Hadzisasanivic, Ng and Wang who proved universal completeness of the \zx-calculus \cite{HFW}, and included Backens who proved stabiliser completeness \cite{1367-2630-16-9-093021}. He co-authored \em Picturing Quantum Processes \em (3), which presents diagrammatic methods for quantum computing to a broader audience.
\textit{\color{gray}\textbf{Publications:} (1) S.~Abramsky and ---. A categorical semantics of quantum protocols. In LICS 2004. (2) --- and R.~Duncan. Interacting quantum observables: Categorical algebra and
diagrammatics. NJP 13 (043016), 2011. (3) --- and A.~Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. CUP, 2017. }
