% !TEX TS-program = pdflatexmk
\RequirePackage[l2tabu,orthodox]{nag}
\documentclass[11pt,a4paper]{article}
\usepackage{etex}
%%%% do rwd stuff %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\pdfoutput=1
%\usepackage{rwd-drafting}
\usepackage[suppress]{rwd-drafting}
\input{margins.tex} % font and other formatting in here
\input{preamble.tex}
\usepackage{wrapfig}
\usepackage{diagrams}
\input{figures/cnot.tex}
\begin{document}
\newcommand\projtitle{Deep quantum compilation using the ZX-calculus}
\newcommand\projacro{DZXC}
\title{QuantERA Full Proposal}
\author{}
\date{}
\maketitle
\begin{center}
{\Huge \projacro :}\\[1ex]
{\LARGE \projtitle }
\end{center}
\newpage
%\textit{Title page will be replaced with file Front-Page\\
%\oldt{Text from previous proposal in blue}}
%\newt{/ Very recent revisions for the new proposal are in violet}
\REM{\textbf{Everything below this needs to fit under 4000
characters for the online submission system}}
\paragraph{Duration:} 36 months
\label{sec:duration}
\section*{Summary of the project}
\label{sec:abstract}
%currently 2510 characters
\REM{(publishable abstract, max. 1/2 page): Be precise and
concise. This summary will be used to select suited reviewers for
the proposal.}
We propose the development of ``deep quantum compilation" technology. This is the concept of a compiler for quantum systems which can be used to develop large portions of the software stack, in a way which is modular in design but tightly integrated once compiled. We propose to develop deep quantum compilation technology by leveraging the \zxcalculus, a versatile formal tool to efficiently reason about tensors, which recently demonstrated state-of-the-art capability to optimise unitary circuits. The graphical \zxcalculus has recently also be shown to be complete: all equations that hold in standard quantum theory can be derived in \zxcalculus. This provides us with the opportunity to develop compiler technology with a scope that would be difficult to achieve otherwise.
Recent investment in quantum technologies has brought us into the era of noisy intermediate-scale quantum (NISQ) devices. These computers are patchworks of components (including classical) that vary greatly between implementations such as silicon qubits, superconducting circuits, or ion traps. As the technology matures into the fault-tolerant regime, quantum computers will continue to be accompanied by a myriad of control systems, and a scarcity of resources. Programming such devices currently requires intimate knowledge of the hardware, and programs must be rewritten for every new device to closely match the hardware model. Any optimisation is purely ad-hoc. We face a situation where the ever-multiplying range of quantum computers has minimal software support.
Solving this problem requires a ``deep" quantum compiler -- one which can transform algorithms to match the resources and capabilities of diverse hardware platforms. Recent formal and practical advances in completeness and optimisation of the \zxcalculus demonstrate a proof-of-principle of the possibility of developing a deep quantum compiler, including provably-correct program transformations for automatically adding error correction and performing hardware-guided optimisations. We will target the compilation stack for three of the most promising hardware platforms, and develop the techniques and software tools to build a deep compiler. In addition, leveraging the foundational expressiveness of the calculus, we will isolate specific resources that give rise to quantum processing, providing in-compiler certification of quantum speed-up. Developing a ``deep" compiler will allow for the sound development of tightly integrated software stacks for quantum computers, becoming a standard for optimisation and benchmarking, and enabling quantum devices to perform computations demonstrably better and faster.
%The goal of this project is to develop the flexible intermediate for compilation and optimisation, which is necessary for the immediate-term practical implementation of post-classical protocols on noisy intermediate-scale quantum computers. %how many buzzwords can we get in this sentence
\REM{ OLDTEXT This project introduces \azx, a flexible intermediate language for
quantum computation, which removes this obstacle by providing a
common interface between the software and the hardware. This
intermediate language will be versatile enough to target a wide
variety of hardware implementations, and simple enough to support
any programming language. Further, \azx will expose a formal
algebraic structure based on an existing graphical formalism called
the \zxcalculus, which recently was proven to be complete: every equation that holds in Hilbert space QM can be derived in \zxcalculus. The latter enables provably-correct program
transformations for automatically adding error correction and
performing hardware-guided optimisations, e.g. by preferring certain
quantum gates over others or enforcing topological constraints. This
project will develop and standardise the \azx language for quantum
computation, integrate it into an effective stack of tools for
compiling quantum programs, and develop new techniques for automated
transformations that make quantum computations run better and
faster.}
\section*{Relevance to the topic addressed in the call}
\label{sec:relev-topic-addr}
%currently 1274 characters
\REM{(in particular specify here which part of the call text is
concerned by your project, max. 1/4 page):}
The project clearly comprises ``\textit{transformative research}'' that explores ``\textit{collaborative advanced interdisciplinary science and/or cutting-edge engineering with the potential to initiate or foster new lines of quantum technologies}'', which is the key overall objective of QuantERA.
We include several ``\textit{excellent young researchers}'', including from Poland, and partner with Cambridge Quantum Computing, a clearly ``\textit{ambitious high-tech SME}''.
In particular we address the \textit{Quantum Computation} area of the call.
The
retargettable nature of the compiler supports ``\emph{new architectures
for quantum computation}", in particular technologically heterogeneous
implementations. The optimising aspect of the compiler will allow the
``\emph{optimisation of error correction codes}", at both
intermediate and machine level. The ability to compile multiple
high-level languages will promote the ``\emph{development of novel
quantum algorithms}". Machine-dependent optimisation work will contribute to the ``\textit{development of devices to realise multiqubit algorithms}".
The ability to compile with specifically post-classical resources leads directly to ``\textit{demonstration of quantum speed-up}".
In total, this project is an enabling
technology that multiplies the impact of all the target
outcomes of QuantERA and the Quantum
Technology Flagship.
\REM{ FROM CALL DOCUMENT:
The QuantERA consortium has created a common funding instrument to support European research projects enabling long-term research in the area of Quantum Technologies.
Through this instrument, the national/regional funding organisations of the QuantERA consortium contribute to the Quantum Flagship agenda1. By launching joint European calls for research projects, they can support more diverse research communities, who are able to tackle the most challenging and novel research directions.
QuantERA projects should be of a FET-like nature and contribute to the development of the European research and innovation in Quantum Technologies. The transformative research done in QuantERA should explore collaborative advanced interdisciplinary science and/or cutting-edge engineering with the potential to initiate or foster new lines of quantum technologies and help Europe grasp leadership early on in promising future technology areas.
**warning this paragraph is patronising bullshit, fuck this "spreading research excellence" western-euro superiority nonsense:
To spread research excellence throughout Europe, QuantERA projects are encouraged to include partners from the widening countries participating in the call: Bulgaria, Croatia, Czech Republic, Hungary, Latvia, Lithuania, Poland, Portugal, Romania, Slovakia, Slovenia and Turkey.
To build leading innovation capacity across Europe and connect with industry, QuantERA projects are encouraged to involve key actors that can make a difference in the future, for example excellent young researchers, ambitious high-tech SMEs etc.
3. Quantum computation
Development of devices to realise multiqubit algorithms; demonstration and optimisation of error correction codes; interfaces between quantum computers and communication systems.
Development of novel quantum algorithms; demonstration of quantum speed-up; new architectures for quantum computation.
}
\newpage
\section{EXCELLENCE \REM{(6 pages)}}
\label{sec:overview}
\subsection{Targeted breakthrough, baseline of knowledge and skills}
\label{sec:targ-breakthr-basel}
\REM{
Describe the targeted breakthroughs of the project.
Describe how the science and technology contribute to the establishment of a solid baseline of knowledge and skills for the specific theme addressed.
Describe the specific objectives of the project, which should be clear, measurable, realistic and achievable within the duration of the project.
}
\paragraph{Summary: }
\label{sec:summary:-}
We propose to develop \emph{deep quantum compilation technology}.
This consists of techniques for a compiler to translate high-level specifications of quantum programs to operations on a variety of hardware platforms, automatically managing resources and architectural constraints in doing so. It uses the \zxcalculus, already the lead tool in circuit optimisation. This allows the software stack to be developed and organised in a modular fashion for multiple platforms, and then compiled in an intelligently-managed way. The addition of compile-time certification of quantum speed-up completes the ability of the deep compiler to make the most of valuable quantum hardware resources.
%\TODOb{Summary/context should contain a clear statement that NOW zx does better (i.e. "outperforms") than anything else for circuit simplification using PyZX. This should be explained in even more detail elsewhere. Aleks maybe?}
\paragraph{Context:}
\label{sec:context}
Effective programming practice allows the programmer to design software without paying very close attention to the nature of the hardware.
In the context of quantum technologies, this is made difficult by the fact that hardware platforms are varied~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla}\REM{[double-check this list of references for suitability]}, have limited resources, and are evolving quickly.
% Due to the overhead involved in making quantum computations fault-tolerant, different platforms will continue to be developed for different tasks (with and without error correction), even as quantum hardware technologies mature and demonstrate scalability.
% The complications presented by limited resources and divergent architectures will likely persist for the foreseeable future.
For classical programs, modern compiler toolchains such as LLVM (\url{llvm.org})
%\footnote{% The LLVM Compiler Infrastructure, \url{http://llvm.org}}
%decouple high-level programming from different hardware platforms, allowing
allow for easy, customisable cross-compilation; no such tools exist for quantum devices.
Optimisation, in particular around error correction, will be vital for running post-classical protocols on near-term hardware. Classically, this is part of an integrated compiler.
Quantum technologies will continue to be scarce and valuable; identifying truly quantum resources (beyond magic states) will be a vital tool for optimising resource use, demonstrating speed-up, and benchmarking quantum devices and protocols.
To build the deep compiler combining all these elements we will use the graphical \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.
This already outperforms all other formal methods for certain problems. For example, the {\tt PyZX} tool for quantum circuit optimisation is already obtaining state of the art results in T-count minimisation (cf.~theory in \cite{DKPdW-2019}), an important problem for effective fault-tolerant quantum computation. This is a further development on the recently achieved ultimate milestone for graphical reasoning: all equations that hold in standard quantum theory can be derived in \zxcalculus (a.k.a.~`completeness') \cite{Jeandel2017A-Complete-Axio, HFW}.
A deep-\zx compiler will significantly advance the deployment of practical quantum computing.
\paragraph{Targeted breakthrough:}
\label{sec:targ-breakthr}
We will develop \emph{the \dzxc system} for deep quantum compilation.
\begin{wrapfigure}{r}{0.50\textwidth}
\vspace*{-10mm}%
% \texttt{\color{red!70!black} [Placeholder?]} \\[-5ex]
\hspace*{-4mm}%
\cgraph[0.7]{dzxc-arch-diagram4.pdf}%
\vspace*{-9mm}
\end{wrapfigure}
This set of tools will intelligently translate high-
level quantum programs to low-level operations on quantum hardware platforms, including
\begin{itemize}
\item
incorporating architectural constraints
\item
optimising resource use
\item
certifying speed-up
\item
managing error correction.
\end{itemize}
These will be specified in a modular way but tightly integrated upon compilation.
%To demonstrate this technology, w
We will develop a \zxcalculus based compiler from a high-level quantum programming language to hardware, for (i)~coupled ion traps (NQIT), %~\cite{PhysRevX.4.041041},
(ii)~silicon spin qubits (Grenoble)\REM{ [do we have something here to cite?]}, (iii)~an IBM device. %The compiler stack will include open APIs, and t
The final milestone is a ready-to-run deep-zx compiler chain incorporating physical layout, error correction support and algorithmic optimisation, compiled for a target system, and demonstrating explicit post-classical resource use in a quantum computation.
% We will specifically pursue the development of deep quantum compilation technology by exploiting the versatility of the \zxcalculus, and further developing its application.
%This will greatly improve the software ecosystem for quantum computers:
%deep quantum compilation will allow future quantum devices to
%easily run existing programs, and future programming languages automatically gain support on a wide range of hardware.
\paragraph{Baseline of knowledge and skills:}
\label{sec:basel-knowl-skills}
Several powerful high-level languages (HLLs) have been proposed for quantum programs, such as Quipper~\cite{Alexander-S.-Green:2013fk} and \Qsharp~\cite{qsharp}.
As with classical HLLs, these languages are not designed to be run directly on quantum hardware. %: instead, their compilers typically output quantum circuit descriptions, which are not tailored well to run on any particular hardware platform.
Our proposal is to develop an analogue of the LLVM compiler system, for quantum computation.
The LLVM compiler system is a modularised collection of libraries for hardware realisation and optimisation for classical programming, providing the functionality which is expected of a well-designed modern compiler.
To build comparable quantum compiler technology we use the \zxcalculus, %has been extensively applied to quantum computation, and
a formal system for transforming quantum procedures in a way that preserves meaning.
It is the product of a decade of work by members of this consortium
on the mathematical foundations of quantum computing \cite{AbrCoe:CatSemQuant:2004,
%Coecke:2009db, CDKW-lics:2012qy,
Coecke2017Picturing-Quant}.
Powerful and flexible, the \zxcalculus can easily describe computations in both the circuit and measurement-based models of quantum computation (MBQC)~\cite{Raussendorf-2001,Duncan:2012uq,Duncan:2010aa} and can formulate and verify quantum error correcting codes \cite{Horsman:2011lr,Chancellor2016Coherent-Parity, Duncan:2013lr} and quantum algorithms \cite{Stefano-Gogioso2017Fully-graphical, Zeng2015The-Abstract-St}.
The calculus can be viewed both as a formal axiomatic theory of complementary observables in categorical algebra, and as a symbolic notation for tensor networks representing quantum states/linear operators. Reasoning is purely graphical.
% 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, in a stunning achievement, 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}.
%An analogue of LLVM for quantum systems would have to manage resources in spite of fundamentally quantum obstacles, such as the no-cloning theorem; and to be useful in the near term, it would also have to account for noise and the resources required for error correction, in addition to the functionality of the sort provided by LLVM.
% One way to realise a comparable compiler technology for quantum computers is to use the \zxcalculus~\cite{Coecke:2009aa}, which is a formal system for transforming quantum procedures in a way that preserves meaning.
% The \zxcalculus is the product of a decade of work by members of this consortium
% on the mathematical foundations of quantum computing \cite{AbrCoe:CatSemQuant:2004,
%%Coecke:2009db, CDKW-lics:2012qy,
% 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{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
%computations.
% and is complete for important subtheories such as the stablizer
% fragment \cite{1367-2630-16-9-093021} and single qubit Clifford+T
% equations \cite{Backens:2014aa}.
%\REM{The closely related ZW-calculus \cite{Hadzihasanovic2015A-Diagrammatic-} provides a complete characterisation of qubit entanglement-classes.}
% The \zxcalculus %has been extensively applied to quantum computation, and
% is powerful and flexible, can easily describe computations in both the circuit and measurement-based models of quantum computation (MBQC)~\cite{Raussendorf-2001} and can be used to formulate and verify quantum error correcting codes \cite{Chancellor2016Coherent-Parity, Duncan:2013lr} and quantum algorithms \cite{Stefano-Gogioso2017Fully-graphical, Zeng2015The-Abstract-St}. Its graphical representation is well-suited to describing systems which naturally have a graph structure, such as surface codes for topological cluster-states \cite{Horsman:2011lr}, and MBQC \cite{Duncan:2012uq}, where it has been used to translate \cite{Duncan:2010aa} between the 1-way model and the circuit model. \textit{\bfseries\ttfamily\color{red!70!black} \KILL{[Not sure whether we want to keep this paragraph but it has lots of good references]}}
%
\TODOb{The figure is especially placed to match the text DON'T CHANGE IT}
The tensor network structure means that the \zxcalculus represents all quantum operations such as
initialisation, unitaries, measurements and discarding in a single notation. This notation is significantly
\begin{wrapfigure}{r}{0.75\textwidth}
\vspace*{-8mm}%
% \texttt{\color{red!70!black} [Placeholder?]} \\[-5ex]
\hspace*{-4mm}%
\cgraph[0.7]{circuit-fig}%
\vspace*{-11mm}
\end{wrapfigure}
%\includegraphics[width=\textwidth]{figures/circuit-fig}
more powerful and flexible than quantum circuits. \zx-based transformations between quantum circuits
may have intermediate steps that cannot directly be expressed as equations between circuits \cite{DKPdW-2019}, as in the adjacent figure:
%An example of such a transformation is the following:
Members of our consortium have demonstrated these formal
reasoning techniques in software, including the interactive theorem
prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which
was used to formally verify quantum communication protocols and error
correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr})
and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early
demonstration of the capacity of the \zxcalculus to {outperform
other methods of circuit optimisation, minimising certain
circuit metrics such as total size, tree-width, or number of
T-gates. Our
industry partner CQC develops \tket, a retargetable quantum compiler
which, using \zx-based optimisations, outperforms all existing
compilers for quantum software.
\TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
%%% cutting because repeated later
% It is strictly more powerful than the stabiliser
% formalism~\cite{Backens:2012fk},
%\begin{figure}[t]
% \vspace{-2mm}
% \centering
% \[
% \cnoti[0.7] \rTo^*
% \cnotii[0.6] \rTo^*
% \cnotiii[0.6] \rTo^*
% \cnotiv[0.6] \rTo^*
% %\cnotv[0.6] \rTo^*
% \cnotvi[0.7]
% \]
% \vspace{-2mm}
% \caption{The \zxcalculus in action: translating from MBQC (left) to
% a quantum circuit (right)}
%\label{fig:zx-mbqc-cnot}
%\end{figure}
\paragraph{Contribution to the theme addressed:}
\label{sec:contr-theme-addr}
We address the theme of \emph{Quantum Computation}.
We develop tools for running quantum programs
on any available quantum device and benchmarking algorithms and machines, significantly
enhancing the capabilities of near-term quantum computers.
% speed new quantum devices and architectures into use, and broaden the range of potential users of quantum computers.
\subsection{Novelty, level of ambition and foundational character}
\label{sec:novelty-level-ambit}
\REM{Describe the advance your proposal would provide beyond the
state-of-the-art, and to what extent the proposed work is ambitious,
novel and of a foundational nature. \textbf{Your answer could refer
to the ground-breaking nature of the objectives, concepts
involved, issues and problems to be addressed, and approaches and
methods to be used.}
}
\paragraph{Novelty:}
\label{sec:novelty}
The concept of a `deep' quantum compiler is entirely novel. Integrating optimisation and error correction intelligently into the stack gives a completely new set of tools for developing and using quantum computers.
Using the \zxcalculus to manage resources in quantum hardware is a totally new application of the \zxcalculus, and an ambitious new way to realise computations on heterogenous quantum hardware.
% Unlike sequences of gates, the tensor networks which are the terms of the \zxcalculus have no preordained causal structure beyond the global input and output, helping us to achieve optimal implementations on diverse architectures.
Furthermore, our system allows transformations of tensor networks which cannot be expressed as equations between circuits as illustrated in the figure on the previous page.
In addition, the \zxcalculus is a sound and complete formal system for transforming quantum procedures, so that each program transformation which our compiler system comes with a proof of its correctness.
The way that the \zxcalculus represents quantum procedures also avoids the immediate dimensional explosion associated with explicit matrices, so that it will in many cases be more efficient than any other automated technique for reasoning about quantum procedures.
The categorisation of multiple post-classical resources is also novel, as is the incorporation into the compiler chain. The development of a compiler stack that also doubles as a benchmarking tool is entirely new.
\paragraph{Ambition:}
\label{sec:ambition}
A ``deep compiler'' for quantum computing systems allows for modular design of the software stack. This lets programmers write at a high level for any hardware and any quantum error correcting codes. It is nevertheless tightly integrated upon compilation. In addition, it is fully tailored to the specific resources, architecture, control systems, and hardware of a specific platform. Furthermore the project includes isolating, integrating, and then certifying quantum speed-up.
%\texttt{\bfseries \color{red!70!black}[refer to specific platforms here (NQIT + Grenoble)?]}
This is very technically ambitious: but while it has never been done before, we believe it to be achievable on the basis of our earlier work, and the ideal combination of skills within the project consortium.
\paragraph{Foundational Character:}
\label{sec:foundational-nature}
\REM{More here. semantics of quantum programming languages is still very young, and already many dead ends. This project gives a unique opportunity for applications to drive theory.}
Deep quantum compilation includes many tools that derive from foundational research.
The \dzxc system will be not just a compiler but also a foundational tool (for example for the characterisation of post-classical resources).
All other systems take the gate model of quantum computing as a given.
This is natural, as it is the \emph{lingua franca} of quantum computation researchers.
The project proposes a new foundation for quantum software, based on a flexible tensor-based representation, combined with mathematically rigorous semantics and formal verification.
A key example of why this is necessary, exploited by NQIT and others, is that lattice surgery operations on surface codes do not fit into the gate model, but have simple representations in the \zxcalculus \cite{BH-2017}.
The ability to demonstrate quantum speed-up at compile-time will enhance our understanding of what is unique about quantum processing.
The deep quantum compiler we will develop
will do the heavy lifting of managing resources and mapping operations to quantum hardware, %allowing the developers of both hardware and software to focus elsewhere.
%This will
facilitating the development of new architectures and technologies for quantum computing.
\subsection{Concept and methodology}
\label{sec:concept-methodology}
\REM{
Describe and explain the overall concept and research approach
underpinning the project. Describe the main ideas, models or
assumptions involved. Identify any interdisciplinary considerations
and, where relevant, use of stakeholder knowledge.
\textbf{Describe any national or international research and innovation
activities which will be linked with the project, especially where
the outputs from these will feed into the project.}
Describe the methodology and explain its relevance to the objectives.
Describe the appropriateness of the methodology to narrow down
multiple options and to address high scientific and technological
risks.
}
The proposed \dzxc (``\emph{deep ZX compilation}'') system is an advanced \textsc{zx}-style system
augmented with features needed for applications.
The \zxcalculus occupies a place in quantum computation similar to the
$\lambda$-calculus in classical computing providing a solid but
austere theoretical foundation. %, without any niceties for practical usage.
The \dzxc system will augment this basic formal system with a second layer of
\emph{annotations} on the tensor graph, describing program parameters
and architectural constraints of a specific hardware configuration.
This two-level design separates the specification (graph layer) from
the implementation (annotation layer) of the program, and is the key
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
completeness \cite{Jeandel2017A-Complete-Axio,HFW},
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
process to be carried out, independent of the target platform. Many
important transformations can be performed at this %platform independent
level,
%--- without recourse to matrix representations of the operations involved ---
such as simplifying the tensor network,
reducing Clifford fragments to minimal forms, and reducing T-count.
Development of such techniques is a low-risk extension of earlier
work, and will be done early in the project
(\ref{task:algorithms},\ref{task:basic-opt}). Further, at this stage
a program can be translated to a fault-tolerant equivalent with
respect to a chosen error-correcting code.
We will also develop translations for the \dzxc system from existing quantum programming languages~(\ref{task:trans1}) early in the project.
These will provide
examples and test cases, and allow comparative
evaluation.
The annotations of the second layer provide the basis of \emph{augmented
rewrites}: program transformations guided by the
annotations to achieve particular goals. %, not expressible in the basic tensor language.
For instance, there is an efficient algorithm
\cite{Mhalla:2008kx} to find the \emph{gflow} of a graph state; if the
state has a gflow then it supports deterministic 1-way computation
\cite{D.E.-Browne2007Generalized-Flo}. Annotating the graph with its
gflow provides guidance for a rewrite strategy which produces an
equivalent, space-optimal circuit \cite{Duncan:2010aa}.
The \dzxc system
generalises this concept to include other annotation information to inform re-writing.
% encompass other sorts of information which would inform how to transform (i.e.,~to re-write) a generic representation of a quantum computational procedure.
For example,
the \dzxc system could incorporate
a system which specifies both how to represent logical operations in a particular error correcting code, and how the operations are constrained in order to satisfy %basic precautions to keep the realisation
fault-tolerance (\ref{task:ECC}).
The \dzxc system will be modular, allowing for several different systems of annotations.
The \dzxc system
will re-write procedures, minimising the number of operations, subject to the constraints described by those annotations.
One such system of annotations will be to describe
the constraints and the costs of operations for particular hardware (\ref{task:runnable}).
%Augmented
%rewrites will be used to find a runnable implementation of the
%abstract tensor for the target platform, and to optimise resource use.
The development
of the general theory of annotations and augmented rewrites
(\ref{task:annotate1}, \ref{task:annotate2}), algorithms for inferring
specific annotations (\ref{wp:representation}), and rewrite strategies which exploit them
(\ref{task:opt-machine}) form a major novel component of the project.
%The \dzxc system
%can therefore re-write procedures, minimising the number of operations, subject to the constraints described by those annotations.
%
%The \dzxc system will be modular, and allow for several different systems of annotations, for different hardware platforms or constraints one might impose on a computation.
% One such system of annotations would be to describe
%the constraints and the costs involved for operations within a particular hardware platform (\ref{task:runnable}).
%Augmented
%rewrites will be used to find a runnable implementation of the
%abstract tensor for the target platform, and to optimise resource use.
%The development
%of the general theory of annotations and augmented rewrites
%(\ref{task:annotate1}, \ref{task:annotate2}), algorithms for inferring
%specific annotations (\ref{wp:representation}), and rewrite strategies which exploit them
%(\ref{task:opt-machine}) form a major novel component of the project.%
Concrete tensor networks have a fixed finite size, whereas algorithms
are described in parametric fashion, \eg varying according the
input size.
To use this, the \dzxc system will incorporate
a second class of annotations to represent limited forms of iteration and recursion, yielding \emph{parametric} \zx terms.
While the hardware-derived annotations are inferred in a bottom-up fashion, the parametric structure is produced top-down, based on the original
high-level quantum procedure provided as input.
While challenging, we have experience of
similar constructs from the \texttt{quantomatic}
project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
\REM{[apropos to refer to PyZX here?]}
A core component in optimising quantum computers is identifying which resources are necessary for non-classical computing. The identification of this quantum speed-up is a live open problem. Drawing on the foundational expressiveness of the \zxcalculus and the expertise in the consortium, and existing automated theorem provers for the calculus, we will identify and express these resources in the \dzxc system.This will enable optimising for use of these resources, and the ability to say at compile time that a procedure is using non-classical processing.
Furthermore, the compiler stack and associated library set of post-classical resources will naturally become a software tool for benchmarking quantum devices, greatly enhancing the maturity of quantum computing technology.
The four major work packages of the project are structured into
various themes: the relation between \zx and other quantum computing representations (\ref{wp:frontend}); necessary theoretical developments of \zx and the identification of quantum-unique resources (\ref{wp:representation}); optimisation strategies independent of implementations (\ref{wp:theory}); using annotated \zx to compile and optimise for specific hardware.(\ref{wp:usefulstuff}).
\subsubsection{A quantum compiler stack}
\label{sec:progr-lang-supp}
Several powerful high-level languages (HLLs) have been proposed for
quantum programs, such as Quipper~\cite{Alexander-S.-Green:2013fk},
\Qsharp~\cite{qsharp}, and the Python framework
ProjectQ~\cite{Steiger2016ProjectQ:-An-Op}.
As with classical HLLs, these languages are not designed to be run directly on quantum hardware: instead, their compilers typically output quantum circuit descriptions, which are not tailored well to run on any particular hardware platform.
Our proposed \dzxc system will represent an interface between multiple different HLLs for quantum procedures, and various quantum hardware platforms.
This system will use terms of the \zxcalculus as an internal representation of the procedure as it undergoes optimisations and translations, \newt{both abstractly and} to fit a particular hardware architecture.
This representation would not be required from or exposed to the user,\footnote{This said, the \zxcalculus has proved a very useful notation for mathematical proofs.}
but would be generated by a compiler front-end from programs written in existing high-level languages.
Therefore it is essential to provide a robust, general framework for compilation of HLLs to \zx terms.
As most existing quantum HLLs can output circuit descriptions, and
as circuits can easily be represented in the \zxcalculus, for the
front-end of~\ref{task:HHL} will first focus on the circuit language
QASM~\cite{Cross2017Open-Quantum-As} before moving towards the more
expressive HHLs Quipper~\cite{Alexander-S.-Green:2013fk},
\Qsharp~\cite{qsharp}, and
ProjectQ~\cite{Steiger2016ProjectQ:-An-Op}. With this expertise we
will then develop in Task~\ref{task:trans1} a general procedure
allowing virtually any extant quantum HLL to interface with the
\dzxc system.
%
Moving down the compilation toolchain towards quantum devices
requires the translation of \zx terms down to some lower-level
representation, specific to each quantum device.
%
Proposed and existing quantum devices differ along a variety of axes.
Realistic models of such devices include various restrictions such
as the limitation to a
fixed number of qubits, a bounded total execution time, or
restrictions on which qubits may interact directly.
%Looking more closely,
Primitive operations will require different amounts of time,
different qubit implementations have different failure
modes, be subject to various noise models, and suffer from low fidelity.
\REM{noise,fidelitY}
%
Due to the novelty of our proposal, we adopt an exploratory approach
with respect to back-end models. Initially, and in parallel, we study
the circuit model (\ref{task:circuit-model}) and the 1-way
model~\cite{Raussendorf-2001} (\ref{task:mbqc-model}). On one hand,
these models are well understood, stable, and have been extensively
treated in the \zxcalculus literature. On the other hand, these two
models have different execution concepts and primitive operations,
despite their computational equivalence. They will therefore allow us
to prototype the development of hardware annotations for the \dzxc
system, \newt{cf.\ Task~\ref{task:runnable}}. In both cases, this
involves three tightly related tasks:
\begin{enumerate}[label=(\roman*)]
\item
decomposing the tensor network into atomic operations;
\item
characterising runnability in the model, by predicates in monadic second order logic; and
\item
transforming the tensor network into an equivalent runnable version.
\end{enumerate}
This experience will inform the later work in \ref{wp:theory} and
\ref{wp:usefulstuff}.
To encourage interaction from other research groups, and to support other languages, the interfaces and functionality for the \dzxc system will be made public.
While we will provide specific modules for the tasks described above, the \dzxc system is intended to extensible: therefore we will publish an open
API and specification language to simplify the task of adding new architectures and error correcting schemes to the system (\ref{task:backendapi}).
Furthermore, in Task~\ref{task:testBench}, we will develop an open
database of tests, which will serve as a measuring tool for the
quality of the output from the \dzxc compiler. The database will be made available to the community for rating and testing future compilers or optimisation techniques.
\subsubsection{Representation, reasoning, and resources}
\label{sec:machines-models}
\REM{stuff about WP 2 here}
The purpose of the \dzxc system is to form the basis of a retargetable compiler, able to generate executables for multiple architectures.
We must then develop a way to take into account the different characteristics of these architectures.
The ability to synthesise hardware-appropriate implementations from abstract descriptions is one of the major novel contributions of this project.
\ref{wp:representation} carries out two research avenues towards this objective.
First, we will model the performance characteristics and architectural constraints of various idealised and realistic machines.
We will then develop the means for the \dzxc system to express these properties.
The goal is two-fold: to facilitate code-generation for a given machine from a \zx term; and to expose information needed by the optimiser.
A key research challenge of this first research avenue in \ref{wp:representation} consists in the management of the classical computation and classical information within quantum algorithms.
What computation should occur at the interface between an HLL and the \dzxc system, and which classical parameters are passed on to the \zx terms? Task~\ref{task:betterboxes} focuses on the question of tests based on measurement results: how should they be integrated within the \dzxc system?
While it will already be quite useful to study concrete diagrams of fixed size (e.g.,~a~quantum circuit on $N$ qubits for a previously-fixed $N$) in the early stages of the project, \newt{Task \ref{task:betterboxes} } %\ref{task:axioms}
will extend the \dzxc system to support parametrised families of diagrams (e.g.,~quantum circuits with $N$ qubits where $N$ can vary) mirroring the control structures present in a quantum HLL.
This will enable more sophisticated, generic optimisations to be run in advance of needing any particular computational procedure.
The test suite designed in in~\ref{task:testBench} will be used to compare and choose amongst the possible solutions.
In task~\ref{task:axioms}, we will extend the
\zx-calculus in two respects. The first is to expand into complete
and universal qudit variations to work effectively beyond 2-level
systems, and the second is to gain a deeper understanding of the role
played by W-type tensors as they interact with the generators of the
\zx-calculus, which are themselves of GHZ-type.
The second avenue of research in \ref{wp:representation} tackles a more foundational aspect of quantum computation, pertaining the identification of resources that enable quantum speed-up in computation.
On the one hand, it will use new results on \zx to try to identify what nonclassical aspects of quantum theory serve as a resource.
On the other hand, it will develop procedures to certify whether a quantum algorithm demonstrates speed-up.
This part of \ref{wp:representation} will take a novel\footnote{%
This work will be novel in the sense that it differs from the traditional approach within the fields of quantum foundations and quantum information theory.
}
approach to these questions, by tackling them from a \zx-centric perspective.
With this we will further develop the usefulness of \zx as a way in which to describe quantum theory.
This may provide insight on outstanding open problems beyond the scope of the current proposal.
The question of resources for quantum speedup will be the topic of Task \ref{task:resources}.
Different paradigms of computation, such as Clifford, Clifford+T, and
universal qubit QM, have been recently axiomatised in the language of \zx.
Each of those paradigms, however, offer different degrees of computational power.
By a comparative study of such axiomatic representations, we will aim at identifying, in the \zx language, what is the feature that enables quantum speed-up.
That is, we will characterise quantum resources in a systematic manner using the \zx framework.
By further building a bridge from the \zx formulation and traditional (e.g.,~device independent) approaches to quantum resources, we will be able to contrast our findings with the current intuitions of what may power quantum computing.
These current intuitions include the nonclassical feature of nature called Kochen--Specker contextuality, as well as Bell nonlocality.
Hence, the outcome of \ref{task:resources} will also include the development of \newt{representations} %proofs
of contextuality within the \zx language.
The certification of algorithms featuring quantum speed-up will be addressed in Task~\ref{task:resourcesagain}.
First, we will identify re-writing processes among the automated theorem proving tools, that cannot be efficiently done with classical algorithms.
This will allow us to identify candidate subroutines that require nonclassical resources to be carried out.
Such subroutines then will be used to develop procedures for characterising if a \zx-represented algorithm demonstrates speed-up.
\subsubsection{Machine-independent optimisation}
\label{sec:repr-reas-azx}
The formal mechanism which the \dzxc system will use to transform \zx terms (sourced by translation from an HLL) into optimised, physically implementable computations
are the theoretical core of this proposal.
Developing effective techniques for mapping \zx terms closely to the constraints of hardware is a prerequisite for our success.
We forsee four stages in the compilation process of a \zx
term into instructions for a physical machine.
%The tasks to be performed within \ref{wp:theory} and \ref{wp:usefulstuff} may be broadly described in terms of how the \dzxc system will transform \zx terms produced by the front-end, to obtain instructions to be realised by a quantum computer (or software quantum simulator) at the back-end.
These stages are:
\begin{enumerate}[label=(\roman*)]
\item
an initial round of generic, hardware-independent optimisations;
\item
application of some choice of strategy for error correction;
\item
translation to a specialised annotation system which represents the parameters and constraints of a specific hardware implementation; and finally,
\item
a round of optimisation within the constraints of the error correction and hardware models.
\end{enumerate}
The first two stages are machine-independent (\ref{wp:theory}) while the last two are machine dependent (\ref{wp:usefulstuff}).
In addition to the development of the tools for these stages, WP4 will develop an interface for the specification of the annotation systems used in stages (iii) and~(iv) above, allowing for easy extension of the \dzxc system to arbitrary hardware systems, making it suitable for the development of general-purpose quantum compilers.
The first stage of the compilation process represents a ``generic optimisation'' subroutine (\ref{task:basic-opt}), which may be applied to arbitrary \zx terms.
This subroutine will re-write \zx terms into ones with fewer resources in a broadly applicable sense, such as fewer total nodes or fewer nodes which realise non-Clifford transformations (for instance, corresponding to $T$ gates).
This may be developed independently of the results of WP1 or WP2 using existing techniques (as well as incorporating any further useful techniques developed in \ref{task:axioms} and~\ref{task:algorithms}).
Recent breakthroughs in the theory of the \zxcalculus~\cite{Jeandel2017A-Complete-Axio,NW-2018} have shown that whenever two \zx terms describe the same linear operator, then one can be transformed into the other using just a finite set of local, diagrammatic transformations.
However, knowing it is possible
\textit{in principle} to transform one computation (e.g. a quantum
circuit) into another one doesn't say anything about efficiency or our
ability to find effective optimisations. In
Tasks~\ref{task:algorithms} , we will employ theoretical and automated
techniques drawn from rewrite theory to search for better
presentations of \zx terms corresponding to Clifford+T operations, and develop strategies for effectively simplifying \zx terms.
These include Knuth-Bendix completion and theory synthesis.
In Task \ref{task:annotate1}, we will provide the \dzxc system with the ability to express topological constraints and causal ordering.
These could include a restriction to nearest-neighbour interactions for 2-qubit operations on a fixed lattice or enforcing a fixed ordering between two gates.
This will provide us with a test case for more complex annotation systems, such as we will require to treat error corrected systems~(\ref{task:ECC}).
The second stage of the compilation process is to take a generic \zx term expressing a computation on idealised quantum systems, and re-write it as a \zx term representing an equivalent transformation of error-corrected qubits (\ref{task:ECC}).
One of the purposes of ``deep compilation'' of quantum programs is to automatically produce the realisation of the error-corrected form of a procedure.
We have extensive experience in treating error correcting codes in the \zxcalculus
\cite{Duncan:2013lr,Chancellor2016Coherent-Parity,BH-2017,Garvie2017Verifying-the-S}.
Similar techniques will enable translating from ``raw'' \zx terms to error-corrected\,/\,fault-tolerant versions of the same program.
As well as the \zx terms to translate, this will take as input a specification the particular error correction code or other fault-tolerance construction to apply.
Additional annotations will be added to ensure that program transformations performed afterwards do not break the fault-tolerance.
% We identify two kinds of optimisation.
% First, generic, model-independent optimisations work on the raw tensor network, typically by reducing its graph complexity, or by minimising the number of non-Clifford operations in the graph.
% This draws on \ref{task:algorithms} and could be applied before the target hardwaere is known.
\subsubsection{Machine-dependent optimisation}
\label{sec:comp-quant-softw}
To realise our objective of ``deep compilation'' of quantum programs onto diverse hardware, we must translate the abstractly-described tensor networks represented by \zx terms to optimised code that can run on realistic quantum hardware.
\ref{wp:usefulstuff} concerns this functionality.
This work package represents the most technically involved and multi-disciplinary component of the project, and requires the integration of the front-end \ref{wp:frontend}, the theoretical work of \ref{wp:representation} and instantiation of the generic optimizations considered in \ref{wp:theory}.
We will develop a further layer of annotations for \zx terms, to provide a means for the \zxcalculus to respect real-world constraints coming from quantum hardware.
This annotation system will again be modular, in that any hardware platform may be described by an annotation system independently of other platforms.
This will make the \dzxc system extensible in principle to any sufficiently well-characterised quantum computing platform.
Annotation systems representing the hardware implementation are to be provided by the development environment, using a standardised interface, as developed in \ref{task:backendapi}.
As a way to demonstrate and to prototype this hardware-dependent annotation layer, we will study concrete hardware platforms quantum computers based on different technologies: silicon spin qubits (Grenoble) in Task~\ref{task:qdot-model}, and optically linked ion traps (NQIT) in Task~\ref{task:NQIT-model}.
In both cases we will interact strongly with the experimental groups working on these
models, who are close colleagues of our consortium members (D.~Horsman for Grenoble, and N.~de Beaudrap for NQIT).
Since these architectures are dissimilar, tackling both is an ideal demonstration of our approach.
The completion of this phase will allow quantum programs
generated by the \dzxc system
to be run on real hardware.
The final, machine-dependent part of the compilation process consists of two stages: formatting to the target system (\ref{task:runnable}) and a last round of machine-dependent optimizations (\ref{task:opt-machine}).
We identify three main tasks:
\begin{enumerate}[label=(\roman*)]
\item
to add suitable machine-dependent error protection to the program;
\item
to optimise the program according to whichever resources are most appropriate for the given machine; and
\item
to lay out the program for execution.
\end{enumerate}
Although we treat them separately, in practice these tasks
will interact in non-trivial ways, and their order need not be fixed.
The annotation system overlays the abstract rewrite theory of \zx-diagrams with real-world constraints coming from quantum hardware.
We will then develop the formal tools for rewriting \zx-diagrams in ways that
respect those constraints.
In task \ref{task:annotate2} we will explore methods to annotate a \zx-diagram with quantitative information such as timing, noise, or fidelity.
In real-world systems, these can vary vastly between qubits interacting in different ways (e.g.,~neighbouring in ion trap vs.\ interactions mediated by optical channel~\cite{PhysRevX.4.041041}) or stored in different physical modes.
The third stage of the compilation process attempts to map a \zx term into an equivalent \zx term which closely models the constraints of a target architecture (\ref{task:runnable}).
This represents the core of the compilation process, taking \zx terms representing a procedure in an abstract model of quantum computation such as circuits or MBQC patterns (with or without error correction), and mapping them into a form which conforms to the physical constraints of a specific hardware implementation.
%Particular implementations are specified by a system of annotations provided by the development environment, consisting of an ``architecture-targeted annotation'' (or ArcTAn) system.
%ArcTAn systems will generalise the particular examples of implementation-oriented annotation systems developed in \ref{wp:representation}, and will aim to encompass as many extant and forseeable quantum hardware platforms as possible, incorporating topological and time-ordering constraints as captured by the results of \ref{task:annotate1}.
The fourth and penultimate stage of the compilation process --- prior to emitting instructions in the machine language(s) of the target hardware --- is a final round of optimisation, which this time respects the constraints of the specific choice of error correction strategy and machine resources specified by the input~(\ref{task:opt-machine}).
%This will involve the development of a theory of re-writing techniques developed in \ref{task:annotate1} to ArcTAn annotation systems.
%By performing a final round of optimisations using a theory of rewrites which apply to all ArcTAn annotation systems, we aim to
This will make possible a reduction in the resources used in any particular hardware platform without requiring the use of bespoke techniques for each target architecture.
\subsection{Interdisciplinary nature}
\label{sec:interd-nature}
\TODOb{For some reason physics is missing: CQM/ZX emerged from compositional physical considerations.}
As shown the schema at the beginning of \S\ref{sec:summary:-},
the ambitious vertical structure of this project requires a uniquely
diverse range of expertise: from \textbf{Software Engineering \& Formal Methods} at the high level, through \newt{\textbf{Quantum Physics},} \textbf{Quantum Computation} and logic at the mid-level, down to quantum \textbf{Systems Architecture} at the low-level.
This project unites those working in \newt{quantum physics from operational compositionality, and} quantum information theory from logical and pure mathematical perspectives with those working on practical error correction, quantum
hardware, and more generally programming language
design and system engineering.
It thus provides a unique opportunity for theoretical insight to inform future technology, and for technological problems to drive future theory.
We will promote these cross-disciplinary interactions by a number of our planned activities, including holding a summer school which will provide both introductory tutorials and more advanced material on the range of techniques and methods which will be used and developed in the project, in a form accessible to both computer scientists and physicists from a wide range of backgrounds.
\newpage
\section{IMPACT \REM{(3 pages)}}
\label{sec:impact-2-pages}
\subsection{Expected impacts}
\label{sec:expected-impacts}
\REM{Be specific, and provide only information that applies to the proposal and its objectives. Wherever possible, use quantified indicators and targets.
Describe how the project will contribute to the expected impacts (see ‘Research Targeted in the Call’ of the Call Announcement).
Describe the importance of the technological outcome with regard to its transformational impact on technology and/or society.}
DZXC significantly advances the state-of-the-art across six of the seven expected impacts.
\paragraph{Develop a deeper fundamental and practical
understanding of systems and protocols for manipulating and
exploiting quantum information ---\!\!}
%The project will \textbf{develop a deeper fundamental and practical understanding} of systems for quantum information processing.
This project will take practical insights from different quantum technologies, along with fundamental techniques in quantum information processing, and embody them in the {\dzxc system}.
We will develop a deep quantum compiler that can take input in several high-level quantum programming languages, automatically add error correction, optimise the process, and output machine instructions for different devices.
Creating such a system necessarily will produce foundational insights into the capability of quantum devices, and quantum information as a physical phenomenon.
The system can also interface with current models of quantum computing, and will enable new hybrid procedures to be developed, as well as potentially new forms of information processing via the \zxcalculus.
Furthermore, expressing recursion will impact on our understanding of quantum causality.
An exciting element of the project is isolating a set of demonstrably-quantum resources, and using these to confirm the presence of quantum speed-up. This will give significant insight into what is possibly `the' foundational question of quantum computing.
The result of this project will be a step-change in our ability to describe how different quantum technologies store and manipulate information, and to design protocols that use their specific abilities.
% By embodying this expertise in \newt{a compiler system}, practitioners can employ push-button optimisations and fault-tolerant transformations of programs \newt{during compilation without needing} a deep understanding of the underlying theoretical techniques, effectively making these techniques available to a broader audience.
%
%The \newt{\dzxc system will compile from high-level (algorithmic) to low-level (physical) representations, allowing programmers to write at a high level for any hardware and any quantum error correcting technology.}
%For instance, causal and topological structure is a crucial restriction on what can be processed in networked computing, \newt{the \dzxc system will be able to take this into account when compiling.}
%The project also includes the ability to interface with current models of quantum computing (the circuit and one-way models), and will enable new hybrid procedures to be developed that include elements of both (as well as potentially new forms of information processing represented in \newt{the annotated \zxcalculus}).
%The result of this project will be a step-change in our ability to describe how different quantum technologies store and manipulate quantum information, and to design protocols that use their specific abilities.
\paragraph{Enhance the robustness and scalability of quantum
information technologies in the presence of environmental
decoherence ---\!\!}
The deep compilation techniques provided by the \dzxc system will reduce the resource requirements in quantum technologies via built-in optimisation techniques.
The latter will be based in part on our already state-of-the-art research (cf.\ \S~\ref{sec:basel-knowl-skills}).
We will develop new layers of annotations for the \zxcalculus and use them for fine-grained resource management around noise, error rates, and connectivity.
Using the annotated \zxcalculus as a design tool, specific error correction protocols can then be developed for different devices, customised to the different noise and error propagation models.
These models will be flexible as the devices get larger, ensuring scalability of robust devices.
Processes can be optimised for networked scalability and diffferent topologies by encoding timing and spacial constraints in the language.
With the annotated \zxcalculus as a common representation, hybrid devices can also be optimised for.
Error correction or mitigation strategies can be developed across multiple devices acting in tandem.
Since the \dzxc system is based on the \zxcalculus as an intermediate representation, this allows the integration of compilation and protection of coherence.
It also enables the system to adapt and optimise protocols for the individual requirements of different hardware platforms.
% and give a mutually-intelligible language for error correction theorists and device technologists, all integrated in the \dzxc system.
\paragraph{Identify new opportunities and applications fostered
through quantum technologies, and the possible ways to transfer
these technologies from laboratories to industries ---\!\!}
As the basis of a retargetable compiler, the \dzxc system will make it easy to support new quantum devices.
This will help make the latest developments in quantum technology available to all academic and industrial users, maximising the return on investment in quantum computing.
To help non-specialist users, we will provide push-button application of complicated transformations -- such as the introduction of error correction or the optimisation of sequences of operations.
Our consortium includes an industrial partner, Cambridge Quantum Computing, to help ensure the industrial relevance of our work.
We will also work closely with quantum technologies groups at QuEnG and NQIT to check the applicability of our work.
With the \dzxc system, high-level quantum languages and protocols can be designed without needing to know the underlying hardware they will eventually be run on.
This will streamline the production of quantum software, opening it up to individuals and companies with limited prior knowledge of quantum computing.
Quantum hardware will also be more accessible, both in academia and industry.
Individual developers will not need to know the entire architecture, as different elements can be adapted automatically during compilation.
This will accelerate the widespread commercial and academic development and exploitation of quantum technology.
\paragraph{Enhance interdisciplinarity in crossing traditional
boundaries between disciplines in order to enlarge the community
involved in tackling these new challenges ---\!\!}
Developing the \dzxc system will utilise the entire range of knowledge required for building quantum technologies, from experimental and theoretical physics, through to quantum computing theory and foundations, and on to formal methods of computer science.
All of these are needed to develop the deep compilation system, so developing the \dzxc system is a fundamentally interdisciplinary task.
Via its intelligent compilation chain and by aiding the development of intuitively accessible programming languages, the \dzxc system will also make quantum technologies accessible to a broader range of users and developers.
For example, algorithm and protocol designers will not need to interface directly with quantum technologies in order to test the effectiveness of their work, lowering the bar for development in the field.
End-users outside of quantum physics and computer science will also be able to build protocols for their own use that do not require them to understand the physical action of the hardware.
The \dzxc system will not be a closed system: our commitment to open
APIs (see \ref{task:trans1} and \ref{task:backendapi}) and our open
test suite (\ref{task:testBench}) will enable users from outside the
project to integrate new tools and techniques with the \dzxc system, and engage
the wider community.
The advent of quantum computation, and the diverse set of skills needed to bring an idea from algorithm to implementation, has shown the limitations of traditional subject boundaries. The breadth of expertise of this consortium, and its thematic focus on developing a common language and methodology from quantum technologies will help transcend these limitations within the project and in the wider community.
\paragraph{Spread excellence throughout Europe by involving partners from the widening countries ---\!\!}
One of our consortium partners is based at the ICTQT, a newly founded research institute in the strongly emergent Poland.
The university of Gdansk, host of the institute, has a long prominent track record on quantum information, with the core of entanglement theory having been developed there.
Sainz's newly founded Foundational Underpinnings of Quantum Technologies group will contribute to and complement the existing team in Gdansk by bringing in the new scope of process theories to tackle foundational and applied questions in quantum theory.
Her own team, funded by ICTQT, will initially consist of a postdoctoral research fellow and a PhD student. % (both TBA).
Oxford site head Coecke was involved in establishing Sainz's new team at Gdansk's new ICTQT institute, as a member of the institutes' International Scientific Committee. The scope of this research proposal aligns perfectly with part of the mission statement of Sainz's team, namely the study of process theories.
%\TODOb{Is this paragraph in the right section? Some of it seems more ``first-time participants''-ey}
%Oxford site head Coecke was involved in establishing Sainz's new team at Gdansk's new ICTQT institute, as a member of the institutes' International Scientific Committee.
%With this project we involve this new institute, and Sainz's team in particular, within an established research community for mutual exchange of knowledge.
%The scope of this research proposal aligns perfectly with part of the mission statement of Sainz's team, namely the study of process theories.
%As the ``Swiss army knife'' of process theories, the \zxcalculus will bring the foundations of quantum theory in direct contact with quantum technology.
%More generally, the experienced project partners will adopt a mentoring role towards this newly formed ICTQT group.
\paragraph{Build leading innovation capacity across Europe by involvement of key actors that can make a difference in the future, for example excellent young researchers, ambitious high-tech SMEs or first-time participants ---\!\!}
The consortium team is well-balanced between young and established researchers.
We are building innovation capacity by involving several research groups that have been founded in the past few years, namely those of Horsman, Kissinger, Valiron, and Sainz (the latter shortly to be established at the time of writing; see previous paragraph).
The team also includes other excellent young researchers on the brink of group development (Backens, de Beaudrap, Wang).
With team members Coecke (who had over 30 grants including several large networks), Jeandel (an INRIA project leader), and Perdrix (an established CR1 research lead), know-how on project design, management, and content will flow to the more junior partners
% In particular, Coecke will adopt a mentoring role throughout the project.
%at the drafting stage to execution will carry over to the more junior partners, as
Our industrial partner, CQC, is an ambitious high-tech SME, currently leading the sector in high performance compilation of quantum software.
The CQC project leader, Duncan, is an experienced researcher who brings expertise in technology transfer from academia to industry.
The junior team members at CQC will benefit from research exposure, while the younger academics will benefit from interaction with industry.
\subsection{Dissemination, exploitation of results, communication}
\label{sec:diss-expl-results}
\paragraph{Dissemination.\!\!}
\label{sec:dissemination}
%\bR personal opinion : we should be bold and say Fuck the (journal)
%System. We will publish only in true open venues like Quantum.
%Nature can go to hell. \e
The primary means of dissemination will be by publishing our results
in leading journals and conferences, with a strong preference for open access
venues. (We note that in computer science, the highest impact
publication venues are conferences with published proceedings.)
%We will target:
\begin{itemize}
\item Specialist quantum information venues: \emph{Quantum Information
and Computation} (QIC), \emph{Quantum Information Processing}
(QIP), \emph{Theory of Quantum Computation} (TQC), and \emph{Quantum
Physics and Logic} (QPL).
\item Mainstream computer science venues: the \emph{Journal of the
ACM} (JACM),
the \emph{International Conference on Computer-Aided Design} (ICCAD), \emph{Logic in Computer
Science} (LiCS), \emph{Principles of Programming Languages}
(POPL), \emph{Automata, Logic and Programming} (ICALP), \emph{Tools
and Algorithms for the Construction and Analysis of Systems}
(TACAS).
\item Mainstream physics journals: \emph{Physical Review Letters} (PRL),
\emph{Physical Review A} (PRA), the \emph{New Journal of Physics} (NJP), and
\emph{Communications in Mathematical Physics} (CMP),
\item {The diamond open access journal \emph{Quantum}.}
\item {Our own recently
established diamond open access journal \emph{Compositionality}.}
\end{itemize}
The consortium members have a strong record of publishing in all of these
leading venues. %Other venues will targeted opportunistically in order to achieve the most timely publication of our results.
As strong supporters of (diamond) open access principles, we will prioritise publishing in the latter two. %, as well as the other open access journals.}
We plan three annual workshops, which will
be open to any interested parties. The final workshop will include a
school aimed at PhD students and potential end-users in industry. We
allocate significant budget for student bursaries to maximise
participation.
\paragraph{Exploitation of results.\!\!}
We propose several direct and indirect routes to exploitation of our
results. Firstly, our consortium includes an industrial partner, CQC,
the Grenoble Quantum Engineering project chaire d'excellence (Horsman, consortium lead)
and {a key member} of the NQIT project (de Beaudrap).
Though CQC our research will be integrated with the leading quantum
software compiler system, \tket. Since \tket already incorporates
some \zxcalculus this offers a direct and natural route to
exploitation. Further, since \tket already supports several existing
software frameworks, and several hardware platforms, this promotes the
widest possible uptake of the project's results by end users, for no
additional work by the project members. To ensure a strong
relationship with CQC, the Oxford-based
post-doc will spend approximately 25\% of their time at the
CQC Cambridge offices.
With NQIT, we will provide a programming framework for the networked quantum computer developed as part of that project (and the quantum computing project which follows afterwards in Phase~II of the UK Quantum Technologies Programme), seek to collaborate with their architectures team, and present the project results at the UK Quantum Technologies annual showcase.
%In both cases, our work can be exploited
%directly by end-users. %% copied from Niel's document so I assume this is up-to-date
{We commit to produce public APIs (see
\ref{del:frontendapi} and \ref{del:backendapi})
which will allow any programming language to
generate code using our system, and make it easy to add support for
future hardware targets. This will enable other projects to
integrate \dzxc into their system. Further, the
software tools developed by our project will be released on an
open-source basis with a permissive license (See
\S~\ref{sec:cons-agre}.) }
\paragraph{Communication.\!\!}
Beyond online self-publishing we will also pitch articles to magazines
aimed at a general audience in several languages. We will
specifically target:
\begin{itemize}
\item English: \emph{Communications of the ACM}, \emph{IEEE Computer},
\emph{Physics Today}, \emph{Nautilus}, \emph{Quanta}, \emph{Aeon},
\emph{Ars Technica}, \emph{New Scientist}, \emph{FQXi blog}.
\item French: \emph{La Recherche}, \emph{Pour la Science}, and
\emph{Interstices}.
\end{itemize}
Several of members of the consortium have had their work featured in
these publications before.
%In addition, the \azx system itself will
%also be routinely presented in any industrial or public engagement
%events which touch on the software tools used by NQIT.
\paragraph{Advisory Personnel:\!\!}
\label{sec:advsiory-board}
In order to ensure the maximum impact, and to complement the expertise
present in the consortium, we have recruited additional
advisors who will consult with the project.
\begin{itemize}
\item \textbf{Prof. Alexia Auffeves} is the Lead scientist of the
Grenoble Quantum Engineering project
\item \textbf{Prof. Maud Vinet} is the head of the silicon spin qubit experimental team
\end{itemize}
Letters of support from are attached at the end of
this document.
\section{IMPLEMENTATION}
\label{sec:impl-2-pages}
\subsection{Work plan \REM{(2 pages)}} \label{sec:work-plan-work}
\REM{Provide a brief presentation of the overall structure of the work plan.
Clearly define the intermediate targets.
Provide a timing of the different work packages and their components
(Gantt chart or similar).
Provide a graphical representation of the work packages components
showing how they inter-relate (Pert chart or similar).
}
The work plan has four major scientific work packages (WPs),
%each focusing on a different \emph{theme} within the project. The work packages
which will proceed in parallel.
All will have at least some activities throughout the length of the project, with the exception of \ref{wp:usefulstuff} which builds on earlier work in the other WPs and thus only begins one year into the project. (There is also a fifth
work package grouping administrative and organisational activities.)
\begin{description}
\item[\ref{wp:frontend}] is focussed on \newt{the \dzxc interface with known high-level quantum programming languages}
%translating from HLLs into \azx, reflecting higher level programming constructs into \azx,
and building a test suite of programs \newt{for benchmarking}.
\item[\ref{wp:representation}] \newt{is focussed on the further development of zx calculus, its axiomatic formulation, and its status as a theory of resources.}
%is about modelling the properties of different machines in \azx, and translating \azx to hardware.
\item[\ref{wp:theory}]
\newt{focusses on resource optimization, such as gate reduction in circuit representations, efficient intelligent error-correction, and other deep algorithms.}
%develops the theory behind \azx and algorithms to realise the logical ideas.
\item[\ref{wp:usefulstuff}]
\newt{applies all the previous to specific quantum hardware.}
%applies these advances to the
%creation of useful quantum software, specifically focusing on
%optimisation and error correction.
\end{description}
Each work package is divided into more specific tasks, each of which
is designed to deliver a particular piece of the project: some are
theoretical results, some are software functions. Broadly speaking,
the tasks are sequenced in order of technical difficulty so that
experience gained on earlier tasks can be applied to the more
difficult ones. There are strong interactions between the tasks, and
early outputs of each WP will be used in later outputs of other WPs.
(Details about the tasks are found in \S~\ref{sec:work-packages}.)
\begin{figure}[th]
\centering
\makebox[\textwidth][c]{\input{ganttchart.tex}}
\caption{Approximate timings and durations of tasks (months)}
\label{fig:gantt}
\end{figure}
%%%%%%%%%%%%%%%%%%%%
%% Overall structure
%%%%%%%%%%%%%%%%%%%%
The project is a single integrated whole, so there are many linkages
between the work packages; these are displayed in
Figure~\ref{fig:pert}. As discussed in
\TODOb{I don't think this is actually discussed in \S~\ref{sec:manag-struct-milest}}
\S~\ref{sec:manag-struct-milest}, only some of these linkages are true
dependencies, where later tasks rely on results of earlier ones. On the other hand, many tasks can influence and enhance each other as they run in parallel.
Our work plan consists of a balance of short tasks with concrete software deliverables (e.g. \ref{task:circuit-model}, \ref{task:mbqc-model}) and longer term, more ambitious and open-ended tasks (e.g. \ref{task:algorithms} and \ref{task:opt-machine}) which can offer significant, but less predictable, step-changes in the state of the art.
Several tasks of \ref{wp:frontend} are ``long and thin'': that is, they are intended to work in parallel with the other WPs, with new features being integrated as they are developed.
Similarly, much of the theoretical work in \ref{wp:representation} and \ref{wp:theory} is intended to be developed alongside the more implementation-oriented WPs.
These theory-oriented WPs will draw inspiration from the practical ones and feed back into them in turn.
The early tasks of \ref{wp:frontend} are quite
practical and don't require much preparation to begin. They will provide
useful experience for the later tasks.
The first three tasks of \ref{wp:representation} build on a significant existing body of results and techniques for the \zxcalculus and quantum information theory.
Similarly, several tasks of \ref{wp:theory} are based on known results and techniques for the \zxcalculus and rewrite theory in general.
Hence, they can begin immediately.
This will provide an ample source of theoretical work to do until the more implementation-oriented tasks \ref{task:circuit-model} and \ref{task:mbqc-model} provide enough examples and use cases to feed into tasks \ref{task:resourcesagain}, \ref{task:annotate1} and \ref{task:annotate2}.
The more challenging machine models of \ref{task:qdot-model},
\ref{task:NQIT-model} and \ref{task:IBM-model} are scheduled to begin in parallel with the more challenging theoretical tasks in \ref{wp:theory}, anticipating a great deal of back-and-forth interaction between these two aspects of the project.
\ref{wp:usefulstuff} requires integrating and generalising many of the
ideas of \ref{wp:representation} and \ref{wp:theory}, so it is mostly
scheduled toward the end of the project.
\TODOb{update pert chart}
\begin{figure}[h]
\centering
\input{pertchart.tex}
\caption{Dependencies and interactions between tasks}
\label{fig:pert}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%
%% Intermediate targets
%%%%%%%%%%%%%%%%%%%%%%%
Our intermediate targets are described in the deliverables of each WP and in the milestones in \S~\ref{sec:manag-struct-milest}, with the latter focussed towards providing working pieces of software.
On the theory side, we aim to augment the \zxcalculus in several directions: by going from qubits to qudits (\ref{del:qudits}), developing representations for recursion and control (\ref{del:recursion}), and expressing topological and causal constraints (\ref{del:topology}).
Throughout the project, we will check the performance of our methods against competitors (\ref{del:outperform}) and benchmark our software using the open test-suite we will develop (cf.\ \ref{task:testBench}).
\TODOb{is this paragraph needed/needed here?}
The allocation of staff to work packages is discussed in
\S~\ref{sec:consortium-as-whole} and \S~\ref{sec:descr-cons}.
However, because of the integrated nature of the project, and the high
degree of past collaboration among the consortium members, most tasks
receive attention from the personnel of several sites. This degree of
collaboration is a strong point of this project.
\newpage
\def\partnerref#1{{\hypersetup{hidelinks}\ref{#1}}}
\subsection{Work Packages \REM{1page per WP}}
\label{sec:work-packages}
\begin{WP}{A quantum compiler stack}{1M}{36M}{wp:frontend}
\WPleaderLOR
\WPeffort{12}{20}{32}{4}{12}{3}
\begin{WPaim}
This WP develops elements of \zx as an abstract intermediate
compiler language. We provide interface between \zx and known
high-level quantum languages (HLL), and between \zx and standard
circuit and measurement-based models, in which all current quantum
protocols are framed.
% This WP provides multiple \emph{compiler front-ends}. We design the
% framework of interaction between high-level languages (HLL) and the
% \azx intermediate representation. We show how to compile several
% languages to \azx, and investigate efficient representations of
% quantum algorithms in \azx. We also discuss how best to annotate
% \azx terms to reflect high-level constructs given by the programmer,
% and the possibility of reflecting \azx annotation back to the HLL.
% Crucially, this WP provides a source of examples to be used in other
% parts of the project. Aside from \ref{task:transQASM}, the tasks are
% extended in time, absorbing features from other parts of the project
% as they are ready.
\end{WPaim}
\begin{WPtasks}
%
%
%
% \WPtask[\label{task:transHLL}]{Compilation from HLL (M6--M36;
% responsible 3; involved 2,4,5)}{%
% Based on the expertise gained from \ref{task:transQASM}, we will
% develop native\footnote{\emph{Native} here meaning ``not via a
% circuit translation.''} drivers for Quipper, {\liquid}, and
% possibly other languages. As well as achieving one of the key
% goals of the project,
% %
% }
\WPtask[\label{task:HHL}]{Front-end (M3--M36; responsible \partnerref{partner:loria};
involved \partnerref{partner:oxford},\partnerref{partner:CQC},\partnerref{partner:gdansk}) }{%
Propose compiler front-ends from known HLLs such as QASM, Quipper
or \Qsharp to \dzxc. This task serves as a test-bed
for~\ref{task:trans1} and~\ref{task:testBench}. It will make
it possible to test
the {\dzxc} framework on real, possibly very large instances of
programs. This task will progressively incorporate new features
of the \dzxc language %as they are
developed
% especially in concert with
in \ref{task:betterboxes}.
%
}
\WPtask[\label{task:trans1}]{Open API for \dzxc (M1--M36;
responsible \partnerref{partner:oxford}; involved \partnerref{partner:loria},\partnerref{partner:CQC},\partnerref{partner:gdansk},\partnerref{partner:radboud})}{%
Develop an open API for the description of ZX terms. While
largely technical, it is% nonetheless
essential as it will be used
as interface to express the benchmarks of
Task~\ref{task:testBench}.
% to feed to the other WPs.
The API will
first be built upon the existing JSON representation for the
\zxcalculus. It will be expanded with the features of \dzxc as they
become available. This task is tightly linked with
\ref{task:betterboxes}.
%
}
\WPtask[\label{task:testBench}]{Open test-suite (M6--M36;
responsible \partnerref{partner:oxford}; involved \partnerref{partner:loria},\partnerref{partner:CQC},\partnerref{partner:gdansk}) }{%
Devise test-suite of concrete instances of circuits and
algorithms to rate success of other WPs. This includes the task of protocol extraction from current known HLLs.
The tests will rate various aspects of algorithms, such as controls, manipulation of
classical wires, scalability, depth of circuits, topologies of
resources, {\em etc}. % The test suite will be continually expanded as the project progresses.
%
}
\WPtask[\label{task:circuit-model}]{Idealised quantum circuits
(M1--M15; Responsible \partnerref{partner:loria}; Involved: \partnerref{partner:grenoble},\partnerref{partner:oxford},\partnerref{partner:CQC})}{%
Translate an \zx term to an equivalent quantum circuit with ideal
gates. This will require algorithms for discovering a suitable
causal ordering on the \zx term, and for decomposing it into
parts that represent individual gates. We will also consider
circuits with constrained width, depth and/or layout. %The output format will be QASM \cite{Cross2017Open-Quantum-As}, suitable to run on a simulator.
}
\WPtask[\label{task:mbqc-model}]{Idealised
1-Way Quantum Computation (M1--M15; Responsible \partnerref{partner:loria}; Involved: \partnerref{partner:grenoble},\partnerref{partner:oxford})}{%
Translate a \zx term to a runnable 1WQC
\cite{Raussendorf-2001} with ideal measurements and state
preparation. Since every term of the \zxcalculus can be trivially
translated to a one-way program, this task focusses on finding
\emph{deterministic} programs, subject to constraints on the size
and topology of the underlying graph states, and limits on the
number of measurement rounds. The output
language will be the Measurement Calculus \cite{DanosV:meac}.}
\WPtask[\label{task:backendapi}]{Back-end API (M20--M36 Responsible: \partnerref{partner:gdansk}; Involved: \partnerref{partner:grenoble},\partnerref{partner:loria},\partnerref{partner:oxford},\partnerref{partner:CQC})}{%
Open specification of an API for back-end modules, facilitating third-party development of specifications of target architectures, providing the \dzxc compiler with extendability to arbitrary hardware platforms.
% \BREM{
% Define open API for back-end modules.}
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable[\label{del:earlyapi}]{M6}{Preliminary front-end for QASM, and initial \dzxc API}
%
\WPdeliverable{M12}{Preliminary benchtests of circuits and algorithms}
%
\WPdeliverable{M15}{Generation of 1WQC code and idealized
circuits from \dzxc terms}
%
\WPdeliverable{M30}{Advanced front-end for Quipper and one other
HLL -- updated API}
%
\WPdeliverable[\label{del:frontendapi}]{M36}{Finalized API for \dzxc, test-suite and front-ends}
\WPdeliverable[\label{del:backendapi}]{M36}{API for back-end
modules, incl.~specification language for architectures.}
\end{WPdeliverables}
\end{WP}
\newpage
%%%
%%%%%%%WP 2
%%%
\begin{WP}{Representation, reasoning, and resources in \zx}{1M}{36M}{wp:representation}
\WPleaderPOL
\WPeffort{{2}}{{12}}{{14}}{{0}}{{42}}{{6}}
\begin{WPaim}
%We build the theoretical foundations for \zx as an intermediate representation. This includes extending the capabilities of \zx to represent mixed states, qudit states, and control flows. We use \zx axiomatisations and automated theorem provers to extract out post-classical computing resources, which will be used both for further optimisation work, and for characterisation of quantum algorithmic speed-up.
We build the theoretical foundations for \zx as an intermediate representation. This includes extending the capabilities of \zx to represent qudit states with a fixed $d$, arbitrary finite-dimensional quantum states, and control flows. We explore the structure of W-type tensors with interaction with \zx generators of GHZ-type. We use \zx axiomatisations and automated theorem provers to extract out post-classical computing resources, which will be used both for further optimisation work, and for characterisation of quantum algorithmic speed-up.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:axioms}]{Beyond qubits and stabilisers
{ (M1--M14; Responsible: \partnerref{partner:oxford}; Involved: \partnerref{partner:loria},\partnerref{partner:gdansk})}}{%
%We will exploit further the recent completeness results to give representations for mixed state qubit quantum theory. We will
%extend the \textsc{zx} tensor formalism from the qubit domain to higher dimensions.
We will extend the completeness results of the \textsc{zx}-calculus from the qubit domain to higher dimensions, to have complete qudit \textsc{zx}-calculus. Furthermore, we will combine all the qudit \textsc{zx}-calculus into a single framework so that we can deal with the whole finite-dimensional quantum theory in a \textsc{zx} style. In addition, we will exploit techniques from the \textsc{zw}-calculus to understand the deep structure of W-type tensors.
% and exploit the translation from \textsc{zx}- to \textsc{zw}-calculus.
}
\WPtask[\label{task:betterboxes}]{Control in \zx
{ \ (M1--M18; Responsible: \partnerref{partner:gdansk}; Involved: \partnerref{partner:grenoble},\partnerref{partner:loria},\partnerref{partner:oxford})}}{%
% Support simple control flow at the level of \azx, making it a more suitable target for compiling from a high-level language. In particular, add support for repetition and recursive definitions of diagrams, e.g. for expressing and transforming regular families of circuits.
We will use parametric \zx terms to support simple control flow at the level of the \dzxc system, making it a more suitable target for compiling from a high-level language. In particular, we will add support for repetition and recursive definitions of diagrams, e.g. for expressing and transforming regular families of circuits.
}
\WPtask[\label{task:resources}]{Resources and axioms
{ (M1--M36; Responsible: \partnerref{partner:gdansk}; Involved: \partnerref{partner:grenoble},\partnerref{partner:loria},\partnerref{partner:oxford})}}{%
We will exploit the three axiom sets for Clifford, Clifford+T, and universal qubit QM,
to identify and distill specific resources that are necessary to quantum speed-up. In particular, to focus on finding multiple resource elements (rather than simply magic states), and to characterise post-classical composition as a resource.
This includes developing \zx representations of contextuality, as a possible post-classical resource.
}
\WPtask[\label{task:resourcesagain}]{Computational resources
{ (M12--M36; Responsible: \partnerref{partner:gdansk}; Involved: \partnerref{partner:grenoble},\partnerref{partner:oxford},\partnerref{partner:CQC},\partnerref{partner:radboud})}}{%
We will use the existing graph re-writing and automated theorem proving tools of Quantomatic and PyZX to determine parts of the re-writing process that are difficult to compute classically. This will then be used to extract candidate subroutines for sources of quantum speed-up. Along with the previous task, these will be used to develop procedures for characterising if a \zx-represented algorithm demonstrates speed-up or not.
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M9}{Preliminary assessment of the comparative study of the axiomatizations of paradigms of quantum computation}
\WPdeliverable[\label{del:qudits}]{M14}{Completeness of qudit \zxcalculus}
\WPdeliverable[\label{del:recursion}]{M18}{\zx formalism for recursion and control}
\WPdeliverable{M20}{Preliminary assessment of nonclassicality of re-writing processes}
\WPdeliverable{M24}{\zx representation and explanation of the result that promotes magic states as a resource of quantum computation}
\WPdeliverable{M30}{\zx formulation of contextuality (Kochen--Specker and/or Spekken's)}
\WPdeliverable[\label{del:non-classicality}]{M36}{Characterisation of set of generic non-classical resources for quantum speed-up}
\end{WPdeliverables}
\end{WP}
\newpage
%%%
%%%%%%%WP 3
%%%
\begin{WP}{Machine-independent optimisation}{M1}{M36}{wp:theory}
\WPleaderOXF
\WPeffort{{12}}{{9}}{{30}}{{6}}{{12}}{{12}}
\begin{WPaim}
We develop practical logical and algorithmic techniques for transforming ``abstract'' \zx terms produced from a high-level program in ways
which will be required by any practical compiler, and reasoning about their properties. Examples include:
resource optimisation, adding error-correction, and execution
layout. This workpackage \newt{genuinely pushes the deep nature of zx compilation}.
%lays the groundwork for machine-dependent optimisation in the next work package.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:algorithms}]{Reduction strategies, algorithms,
and complexity (M1--M36; {Responsible: \partnerref{partner:radboud}; Involved: \partnerref{partner:loria}, \partnerref{partner:oxford}, \partnerref{partner:CQC}})}{%
Develop new strategies for simplifying \textsc{zx}-style tensor
networks and reducing to (pseudo) normal forms, with the help of
automated techniques such as Knuth-Bendix completion and
graphical theory synthesis, \newt{or those in \cite{DKPdW-2019}}. Implement these strategies in
software \newt{(cf.~{\tt PyZX})} and give bounds on computational complexity.
}
\WPtask[\label{task:annotate1}]{Topological and causal constraints
(M1--M18; {Responsible: \partnerref{partner:oxford}; Involved: \partnerref{partner:loria}, \partnerref{partner:CQC}, \partnerref{partner:radboud}})}{%
Extend \dzxc language and tools to express and enforce: (1) topological
constaints, such as nearest-neighbour connectivity of qubits and
(2) causal/temporal constraints, such as sequential ordering of
measurements and classically-controlled operations.
}
\WPtask[\label{task:annotate2}]{Quantitative Properties (M13--M24;
{Responsible: \partnerref{partner:oxford}; Involved: \partnerref{partner:grenoble}, \partnerref{partner:CQC}, \partnerref{partner:radboud}})}{%
Extend \dzxc language and tools to account for several kinds of
numerical annotations, e.g.~timing data related to performing
operations, gate fidelities, channel fidelities, and decoherence
over time. Allow these to vary by location and develop
techniques to maximise exploitation of resources with varying
fidelities. Provide formal methods to propagate these
quantities from local to global properties.
}
\WPtask[\label{task:basic-opt}]{Generic optimisations of \zx-terms
(M13--M24; {Responsible: \partnerref{partner:oxford}; Involved: \partnerref{partner:loria}, \partnerref{partner:CQC}, \partnerref{partner:radboud}})}{%
Use the results of task~\ref{task:algorithms} to develop
procedures to optimise \zx-terms, in a way which is applicable
for families of circuits (e.g.~Clifford, Clifford+T, CNOT+T,
...) as well as measurement-based quantum computations,
independently of any particular hardware implementation or
approach to fault-tolerance and minimising different possible
metrics (such as total size, tree-width, or number of
non-Clifford subterms such as T-gates).
}
%%
\WPtask[\label{task:ECC}]{Application of Error-Correction
(M1--M36; {Responsible: \partnerref{partner:oxford}; Involved: \partnerref{partner:grenoble}, \partnerref{partner:gdansk}})}{%
Develop algorithms which rewrite abstract tensor networks to
equivalent tensors in codeword space of a chosen
error-correcting code. This may be combined with additional
constraints from the annotation system, representing the
implementation of a specific approach to fault-tolerant
quantum computation, which is provided by the development
environment.
}
\end{WPtasks}
\begin{WPdeliverables}
%\WPdeliverable{M18}{\zx language constructs for basic control flow, repetition and recursion}
\WPdeliverable{M36}{\newt{Generalisations of {\tt PyZX} and other general-purpose techniques and
algorithms + software for simplifying \zx terms}.}
\WPdeliverable[\label{del:topology}]{M18}{An extended \zx language which expresses
topological and quantitative properties, with associated
reasoning techniques.}
\WPdeliverable[\label{del:outperform}]{M24}{\newt{Setting the state-of-the-art for all forms of circuit optimization}.}
\WPdeliverable{M24}{\newt{Optimization techniques for a variety of computational models}.}
% \WPdeliverable{M24}{Routines for adding error-correction to \zx programs}
\WPdeliverable{M36}{Routines for adding error-correction to \zx programs.}
\end{WPdeliverables}
\end{WP}
\REM{\emph{Leader:} Coecke.
\emph{Others:} de Beaudrap, Duncan, Jeandel, Kissinger, %Jacobs
Perdrix, Valiron, Carette.}
% in two ways:
% to describe the classical control parameters in quantum programs, and to
% accommodate annotations for machine models and cost models for optimization, bridging between %We will also further improve our understanding of the ZX-calculu
% s, aiming towards a complete set of rules, and built analogues for arbitrary dimensions.
\newpage
%%%
%%%%%%%WP 4
%%%
\begin{WP}{Machine-dependent optimisation}{M13}{3M6}{wp:usefulstuff}
\WPleaderGREN
\WPeffort{20}{9}{12}{2}{6}{0}
\begin{WPaim}
We import machine-dependent specifications to \zx terms, and use this to optimise algorithms further for specific hardware constraints. We focus on the silicon spin qubits developing in Grenoble, the ion traps developed in Oxford, and the superconducting devices accessible through CQC and partnership with IBM. This is the culmination of all previous work packages, and feeds back into them. The final result will be a full ready-to-run deep-\zx compiler chain incorporating physical layout, error correction support and algorithmic optimisation, compiled for a target system, and demonstrating provably post-classical resource use in a quantum computation.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:qdot-model}]{Grenoble silicon spin qubits (M13--M36 Responsible: \partnerref{partner:grenoble};
Involved: \partnerref{partner:loria},\partnerref{partner:gdansk})}{
We will model the silicon spin qubits being developed in Grenoble, and extract specific annotations for
\zx that describe key elements of the architecture. This will
include qubit layout on wafers, network connectivity, and timing/fidelity of potential entanglement links. A suitably annotated \zx term
will then be translated to an executable sequence of hardware
instructions -- output language to be defined in collaboration with
the team at LETI.
}
\WPtask[\label{task:NQIT-model}]{Oxford ion traps (M13--M30 Responsible: \partnerref{partner:grenoble};
Involved: \partnerref{partner:oxford},\partnerref{partner:CQC})}{%
In collaboration with the Oxford ion trap group and the NQIT team, we will design an output module which generates code for a realistic model of
ion trap quantum computers, including qubit losses and leakage, gate
timings, and circuit layout. Output language to be defined in collaboration with hardware experts at Oxford.
}
\WPtask[\label{task:IBM-model}]{IBM superconducting devices (M18--M36 Responsible: \partnerref{partner:grenoble};
Involved: \partnerref{partner:oxford},\partnerref{partner:CQC},\partnerref{partner:gdansk})}{%
Using the IBM devices accessed through the collaboration with CQC, model the devices and extract annotations. Compare with similar annotations from Grenoble and Oxford devices to extract core common components.
}
\WPtask[\label{task:runnable}]{Formatting for target systems
(M15--M30; Responsible: \partnerref{partner:loria}; Involved: \partnerref{partner:grenoble},\partnerref{partner:oxford},\partnerref{partner:gdansk})}{%
Develop algorithms which, given a collection of constraints
representing a machine model
(c.f.~\ref{task:annotate1}, \ref{task:annotate2}), re-writes \zx terms
to a form which can be executed on that machine model.
%\BREM{ Develop a specification system for the operations and constraints of a hardware system, in order to specify how to transform a ``logical'' \azx term to a procedure to realise that transformation on a specific machine.}
}
\WPtask[\label{task:error}]{Error correction for target devices
(M15--M30; Responsible: \partnerref{partner:grenoble}; Involved: \partnerref{partner:oxford},\partnerref{partner:CQC})}{%
Develop specific small-scale and optimised error-correction and/or mitigation techniques for ion trap and spin qubit devices. Using the annotations extracted for the devices, and protocols developed in task \ref{task:ECC}, minimise qubit overheads and match codes to the specific error models of the Oxford and Grenoble devices.
}
%%
\WPtask[\label{task:opt-machine}]{Model-guided optimisation
(M21--M36; Responsible: \partnerref{partner:grenoble}; Involved: \partnerref{partner:loria},\partnerref{partner:oxford},\partnerref{partner:CQC},\partnerref{partner:gdansk})}{%
Develop procedures to optimise \zx-terms subject to a machine
model, within the confines of
an annotation system for a particular hardware platform
employing a particular approach to fault-tolerance, informed by
techniques from \ref{task:annotate1} and~\ref{task:annotate2}.
}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M19}{Initial device-specific annotations for Grenoble and Oxford machines}
\WPdeliverable{M24}{Initial optimised error correction techniques for ion traps and spin qubits}
\WPdeliverable{M28}{Back-end module for Oxford ion traps}
\WPdeliverable{M30}{Back-end module for Grenoble spin qubits and IBM devices}
\WPdeliverable{M36}{Fully optimising \dzxc with compilation to Grenoble, Oxford, or IBM architecture}
\end{WPdeliverables}
\end{WP}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% WP admin and comms
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{WP}{Administation and Communications}{M1}{M36}{wp:admin}
\WPleaderGREN
\WPeffort{3}{3}{2}{0}{4}{0}
\begin{WPaim}
This work package collects general administrative activities and
the organisation of the project meetings. All meetings will be
organised as open scientific workshops, co-located where possible
with a relevant conference.
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:admin}]{Project administration (M1--M36;
responsible \partnerref{partner:grenoble}; involved \partnerref{partner:loria},\partnerref{partner:oxford},\partnerref{partner:CQC},\partnerref{partner:gdansk})}{Global administration and
project coordination.}
\WPtask[\label{task:website}]{Creation and maintenance of project
website (M1--M36; responsible \partnerref{partner:grenoble}; involved \partnerref{partner:loria},\partnerref{partner:oxford},\partnerref{partner:CQC},\partnerref{partner:gdansk})}{As part of
our commitment to open science, we will create and maintain a
unified website for the project, including latest scientific
works, downloadable software, end-user documentation, and
popularising articles aimed at a general audience.}
\WPtask[\label{task:wkshopone}]{Kick off meeting (M1--M2;
responsible \partnerref{partner:loria}; involved \partnerref{partner:grenoble})}{Project workshop to define
state of the art, establish plans for the next year.}
\WPtask[\label{task:wkshoptwo}]{Midpoint meeting (M17--M18;
responsible \partnerref{partner:gdansk}; involved \partnerref{partner:grenoble})}{Project workshop to disseminate
initial results, evaluate progress and determine next steps.}
\WPtask[\label{task:wkshopthree}]{Final meeting and school (M33--M36;
responsible \partnerref{partner:oxford}; involved \partnerref{partner:grenoble},\partnerref{partner:gdansk})}{Project workshop and school to disseminate
project results.}
\end{WPtasks}
\begin{WPdeliverables}
\WPdeliverable{M2}{Website up and running}
\WPdeliverable{M3}{First workshop}
\WPdeliverable{M18}{Second workshop}
\WPdeliverable{M36}{Final workshop and school}
\end{WPdeliverables}
\end{WP}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\input{old-wps.tex}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\paragraph{Work package overview}
\label{sec:work-pack-overv}
\newt{\begin{center}
\begin{tabular}{|p{0.2\textwidth}|c|c|c|c|c|c|}
\hline
\textbf{Partner}
& \ref{wp:frontend}
& \ref{wp:representation}
& \ref{wp:theory}
& \ref{wp:usefulstuff}
& \ref{wp:admin}
& \textbf{TOTAL} \\\hline
1. Grenoble & 12 & 2 & 12 & 20 & 3 & 49 \\\hline
2. LORIA & 20 & 12 & 9 & 9 & 3 & 53 \\\hline
3. Oxford & 32 & 14 & 30 & 12 & 2 & 90 \\\hline
4. CQC & 4 & 0 & 6 & 2 & 0 & 12 \\\hline
5. Gdansk & 12& 42 & 12 & 6 & 4 & 76 \\\hline
6. Nijmegen & 3 & 6 & 12 & 0 & 0 & 21 \\\hline
\textbf{TOTAL}& 83 & 76 & 81 & 49 & 12 & 301 \\\hline
\end{tabular}
\end{center}}
\REM{(total effort per WP and partner in person.months)}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\subsection{Management structure, milestones, risk assessment \REM{(2 pages)}}
\label{sec:manag-struct-milest}
\REM{Describe the organisational structure and the decision-making.
\textbf{including a list of milestones (template provided). A
milestone is a major and visible achievement. It should be SMART:
Specific, Measurable, Attainable, Relevant, Time-bound.}
Explain why the organisational structure and decision-making
mechanisms are appropriate to the complexity and scale of the
project.}
\paragraph{Coordinator}
\label{sec:overall}
Coordination between sites and between work packages will be overseen
by D. Horsman at the Grenoble site, which will also handle the
overall administration of the project.
\paragraph{Sites}
\label{sec:sites}
The project will be managed by a senior scientist from each site:
B. Coecke (Oxford), R. Duncan (CQC), D. Horsman (Grenoble), A. B. Sainz (Gdansk),
S. Perdrix (LORIA), and A. Kissinger (Nijmegen). They will track
global progress to ensure milestones are reached, and facilitate
collaboration across tasks at their individual sites. They will be in close contact throughout the project to assure coherence and concurrence of the activities at the different sites.
\paragraph{Work packages}
\label{sec:work-packages-1}
Each work package will be lead by a responsible PI who will coordinate
research activity between sites to ensure that deliverables are met,
achieve WP-specific objectives, and organise collaboration meetings as
needed.
\textbf{\ref{wp:frontend}}: S. Perdrix (LORIA),
\textbf{\ref{wp:representation}}: A. B. Sainz (Gdansk),
\textbf{\ref{wp:theory}}: B. Coecke (Oxford),
\textbf{\ref{wp:usefulstuff}}: D. Horsman (Grenoble),
\textbf{\ref{wp:admin}}: D. Horsman (Grenoble).
\paragraph{Experimental and integration advisory board}
\label{sec:monit-advis-board}
Every six months there will be a meeting of both the work package leaders
and the site leaders, either electronically (\eg via Skype) or at a
project event. At these meetings progress towards research objectives
will be evaluated, and any new opportunities will also be discussed. These
meetings will be organised by the coordinator.
To assist in monitoring and evaluating progress, as well as to collaborate on WP4,
we have recruited Alexia Auffeves and Maud Vinet as external advisors. Prof. Auffeves is the Lead of the
Grenoble Quantum Engineering project, and Prof. Vinet is the head of the silicon spin qubit experimental team.
The entire project and advisory board (see \S\ref{sec:impact-2-pages})
will meet once a year to evaluate progress, set priorities, and plan
next steps.
\bR
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{List of milestones}
\label{sec:list-milestones}
The milestones of the project are conceptually simple: at each
milestone we will deliver a functioning piece of software. With each
milestone, we add more, and more advanced, functionality. By
delivering the software incrementally, we follow best practice in the
industry: by regularly integrating parts from all work packages, we
reduce risk and improve communication across the consortium.
\begin{center}
\makebox[\textwidth][c]{
\begin{tabular}{|c|c|c|l|}
\hline
\textbf{Milestone} &
\textbf{Delivery Month} &
\textbf{WP involved} &
\textbf{Title} \\\hline
%
\ms \label{ms:qasmqasm}&
12 &
\ref{wp:frontend} &
Minimal QASM $\to$ QASM circuit optimiser \\\hline
%
\ms \label{ms:quippermbqc}&
18&
\ref{wp:frontend},\ref{wp:representation},\ref{wp:theory}&
Support for one HLL using parametric \zx,\\
&&& with 1WQC and idealized circuit output \\\hline
%
\ms \label{ms:optimise-ecc}&
24&
\ref{wp:representation},\ref{wp:theory},\ref{wp:usefulstuff}&
Architecture sensitive, fidelity aware optimiser\\
&&& Error correction support
\\\hline
%
\ms \label{ms:nqitbackend}&
30&
\ref{wp:frontend},\ref{wp:theory},\ref{wp:usefulstuff}&
Back-end support for Oxford Ion Traps,\\
&&& initial back end API\\\hline
%
\ms \label{ms:delftbackend} &
36&
All&
Complete deep-\zx compiler stack with open\\
&&& APIs, and a target compiled protocol\\
&&& demonstrating explicit quantum speed-up. \\\hline
\end{tabular}}
\end{center}
\e
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\paragraph{Critical risks for implementation}
\label{sec:crit-risks-impl}
\REM{Describe any critical risks, relating to project implementation, that
the stated project's objectives may not be achieved. Detail any risk
mitigation measures.\textbf{Please provide a table with critical risks
identified and mitigating actions (template provided).}
}
The project is overall quite high-risk, in the sense that what we
propose is in the most part entirely novel, and might fail. The
rewards for success would be correspondingly great. However, we have
designed the project to survive the failure of many (or even most) of
its tasks and still deliver value.
We mix low and high risk activities. Success in low
risk activities (\ref{task:trans1}, \ref{task:basic-opt}, \ref{task:ECC},
%\ref{task:axioms}, THIS IS NOT REAALY LOW RISK
\ref{task:circuit-model}, \ref{task:mbqc-model})
will still deliver significant progress towards our overall objective.
\oldt{\ref{wp:theory} is the most critical; here we mitigate the risk by
(i) developing experience on easier objectives before addressing more
demanding ones and (ii) consulting our board of advisors to foresee
problems. Due to its high dependence on other tasks, we consider
\ref{wp:usefulstuff} to be highest risk.}\TODOb{This doesn't seem quite up-to-date, also see below}
\begin{center}
\begin{tabular}{|p{0.25\textwidth}|c|c|p{0.4\textwidth}|}
\textbf{Description of risk}
& \textbf{Likelihood}
& \textbf{WPs involved}
& \textbf{Proposed mitigation measures}\\\hline
%
Can't hire suitable post-docs&
Medium&
All&
While we have already identified several suitable candidates for each
role, the investigators also collectively supervise a large body of PhD
students and post-docs who could be channelled to the project.
\\\hline
%
NQIT or Grenoble machine info unavailable or not detailed enough&
Low&
\ref{wp:usefulstuff}&
\oldt{(i) We have members of the consortium from NQIT, and letters of
support from DiCarlo who agrees to help. (ii) We can approach other
members of our board of advisors, or other friendly
experimentalists. (iii) We can target an more abstract model of the
machine} \\\hline
%
Some desired technique or algorithm isn't found&
High&
All&
All tasks where this is a risk have been structured as a collection of
related goals; if some part doesn't succeed then the finished system
will be will have fewer features, or worse performance. However it's
very unlikely that an entire task will fail in a way that jeopardises
the project. \\\hline
%
Software integration issues&
Medium&
All&
(i) We will establish a common API in \ref{del:earlyapi} to allow
loose coupling of the software components (ii) We appoint the most
experienced software developer in the consortium (Valiron) to act as ``integration tzar'' and ensure
the global design is good. (iii) As noted above, we will integrate
often and deliver new features more than once a year.
\\\hline
\end{tabular}
\end{center}
\newpage
\subsection{Consortium as a whole} %\REM{(1 page)}
\label{sec:consortium-as-whole}
%%\REM{The individual members are described in section 3.5, there is no
% need to repeat that information there.
%Describe the consortium. How will it match the project's objectives
%and bring together the necessary expertise? How do the members
%complement one another?
%In what way does each of them contribute to the project? Show that
%each has a valid role and adequate resources in the project to fulfil
%that role.
%If applicable, describe the industrial/commercial involvement in the
%project and explain why this is consistent with and will help to
%achieve the specific measures which are proposed for exploitation of
%the results of the project.
%}
\newt{The members of the consortium are chosen to provide the best
combination of skills to deliver this project, including the fathers of \zxcalculus, those who established it as a universal and complete calculus, those who have developed applications of \zxcalculus to quantum technologies, and those who have outperformed all other methods using \zxcalculus.
%They also contributed greatly to community building.
\TODOb{Do we think it's really good to say we are the Oxford mafia?
Also i had two other positions between Oxford and CQC -rd}
Many members also have a long history of collaboration, and in fact have been at different consortium sites at some point of their career, for example Wang was a postdoc at Nancy before moving to Oxford and CQC. Duncan, Horsman, Kissinger and Perdrix were postdocs at Oxford before moving to CQC, Grenoble, Nijmegen and Nancy respectively. Sainz has a long-standing collaboration with members of the Oxford Group, and organised Quantum Physics and Logic X, the main conference for \zxcalculus alike research, while at Barcelona. Coecke is a member of the International Scientific Committee of ICTQT-Gdansk, the new institute that hosts Sainz' new group.
Several members have ongoing collaborations with Cambridge Quantum Computing Inc. In particular, co-inventor of \zxcalculus Ross Duncan is now the leading researcher at CQC, which clearly demonstrates CQC's commitment to \zxcalculus. Quantum compilation is moreover the key focus of CQC. Several members are part of the NQIT Quantum Technologies Hub.\footnote{nqit.ox.ac.uk}
%We now provide details on each of these.
Expertise on the
{\bf theoretical aspects} underpinning the project is provided by Oxford site leader Coecke and CQC research leader Duncan
who jointly invented the \zxcalculus\ \cite{Coecke:2009aa}. Backens, Perdrix, Jeandel and Wang are the key contributors to establishing universal completeness of \zxcalculus \cite{1367-2630-16-9-093021, Jeandel2017A-Complete-Axio, HFW}. Coecke pioneered general categorical and diagrammatic methods in quantum computing \cite{AbrCoe:CatSemQuant:2004}, and with Kissinger co-authored the textbook of the field \cite{Coecke2017Picturing-Quant}.
Expertise on {\bf quantum technology applications} is provided by those who pioneered these applications. Duncan, Perdrix and Horsman pioneered zx-based translations between different computational models \cite{Duncan:2010aa, Horsman:2011lr}, Horsman and Kissinger pioneered zx-based error-correction \cite{Chancellor2016Coherent-Parity}, and Horsman and de Beaudrap demonstrated the equivalence of zx-rules and lattice surgery \cite{BH-2017}.
Duncan and Kissinger pioneered {\bf automation} of diagrammatic reasoning (cf.~{\tt quantomatic} and {\tt PyZX}), which also will play a key role in this project, as they already have in setting the state-of-the-art in circuit optimization \cite{DKPdW-2019}.
We also include pioneers in {\bf quantum
programming languages} (Valiron), important contributors to the
theory of {\bf MBQC} (Perdrix, de Beaudrap, and Duncan) and
{\bf quantum circuits} (Jeandel). }
The consortium has also been instrumental in community building, for example with the QPL conference series which now attracts well over 100 participants every year and approx.~75 paper submissions on foundational and structural research in the area of quantum computing. It also has organised several schools e.g.~the QiCS School\footnote{www.cs.ox.ac.uk/people/bob.coecke/QICS$\underline{\ }$School.html} and the CAP Spring School,\footnote{www.cs.ox.ac.uk/ss2014/} and a substantial talks archive is maintained.\footnote{www.youtube.com/user/OxfordQuantumVideo} \newt{More recently, the several members are
involved in the Compositionality community, which has diagrammatic/categorical reasoning as its core focus, with a new journal, a new conference series, and a new workshop series.}
\TODOb{Keeping any of this? Introducing anything else?}
\bR Of utter importance is the alignment with Networked Quantum Information Technologies Hub (NQIT) at the Oxford site, which means that several members of the consortium have already direct expertise with interacting with quantum hardware (de Beaudrap, Horsman). The NQIT is the largest of the four Hubs in the UK National Quantum Technology Programme, a 270 GBP million investment by the UK government to establish a quantum technology industry in the UK. %We are working towards building a quantum computer demonstrator, the Q20:20 engine, which demonstrates a networked, hybrid light-matter approach to quantum information processing.
Concretely, the most important aspect is the fact that the modular architecture motivated using lattice surgery on surface codes for the logical operations, and that these are in effect \zx-operations \cite{{BH-2017}}. This will certainly make the ambition here much more achievable. \e
%\REM{From cyril to address industrial/commericial}
%Bull brings expertise in high performance simulation as well as
%industrial guidances in software. \REM{more}
\newpage
\subsection{Description of the consortium \REM{(1 page each)}}
\label{sec:descr-cons}
\newcounter{partners}
\REM{Describe expertise and role in the project for each partner
(templates provided). The information provided here will be used to
judge the operational capacity. Use the following templates for the
coordinator, the other partners requesting funding, and partners not
requesting funding if any. If the project relies on input to be
provided by a third party, append a letter of commitment at the end
of the proposal}
%%%% Grenoble
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 1} & University of Grenoble\\
Project Coordinator & Laboratoire Informatique de Grenoble \end{tabular}
\vspace{1mm}\hrulefill\vspace{1mm}
\refstepcounter{partners}\label{partner:grenoble}
\textbf{Expertise:}
The Laboratoire Informatique de Grenoble at the UGA is the largest informatics research laboratory in France, and the key computer science partner in the Quantum Engineering Grenoble ecosystem, a major new multi-disciplinary project funded by the French government and the EU. Quantum Engineering Grenoble aims to foster an ecosystem for quantum technologies, connecting science, the humanities and entrepreneurship. Building on the unique concentration of expertises in Grenoble, the project is investigating the whole spectrum of challenges, from the industrial transfer of a quantum processor to the philosophical and societal implications of quantum theory and technologies.
Grenoble is world renowned for its fundamental research institutes in computer science, condensed matter physics, nanosciences, and mathematics as well as its high-tech innovative companies ranging from local start-ups to multinational groups. Grenoble's ecosystem is ranked within the top 5 innovative cities in nanotechnologies worldwide and 1st in Europe. The CAPP group at the LIG had a large base of expertise in classical formal methods and verification, and the growing quantum group is embedded within this space.
As part of the Quantum Engineering project, the quantum group collaborates directly with partner in Institute Ne\'el and CEA-LETI. In particular, the latter
brings expertise in devices large scale fabrication and characterization (DCOS de- partment) and coding and information theory (DSYS department). Over the recent years, CEA- LETI/DCOS has acquired high-level expertise on Si CMOS technology for quantum information processing, demonstrating, in collaboration with CEA-INAC, the first qubit implemented on a foundry-compatible Si CMOS platform. Grenoble contains precisely the informatic, foundational, and experimental/implementation expertise to ground this project.
\textbf{Dr Dominic Horsman} is the Chair of Excellence in Quantum Engineering (physics and computer science) at the Universit\'e Grenoble Alpes, one of the two Chairs on the Quantum Engineering project. He has worked on quantum architectures and error correction, and is inventor of the well-known lattice surgery technique for fault-tolerant computation. He has contributed greatly to applications of \zx-calculus, including the study of non-circuit quantum computational models, error-correction, and lattice surgery. \textit{\color{gray} \textbf{Publications:} (1) Surface code quantum computing by lattice surgery. ---, Fowler, Devitt, Van Meter New Journal of Physics 14 (12), 123011.
(2) de Beaudrap, ---. The \zxcalculus is a language for surface code lattice surgery. arXiv:1704.08670. (3)Quantum picturalism for topological cluster-state computing. New J. Phys., 13(095011), 2011. (4) N. Chancellor, A. Kissinger, S. Zohren, and ---. Coherent parity check construction for quantum error correction. arXiv:1611.08012, 2016. (5) Van Meter, ---. A Blueprint For Building a Quantum Computer. CACM 56:10, 2013. }
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Role in Project:}
As the coordinating site, Grenoble will handle the overall
management of the project. With expertise in the \zxcalculus, error correction, and co-ordinating with Grenoble experimentalists, Horsman will be involved in all the
work packages, especially \ref{wp:theory}, and tasks
\ref{task:mbqc-model} and \ref{task:ECC}. The postdoc employed at
Grenoble will focus on \ref{wp:theory} (15 months),
\ref{wp:usefulstuff} (12 months) and \ref{wp:representation} (9 months).
\end{minipage}
}
\newpage
%%%% LORIA + LRI
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 2} & Universit\'e de Lorraine / CNRS / INRIA\\
& LORIA (UMR 7503) \\
& LRI (UMR 8623) ({\small Universit\'e Paris-Sud / CNRS })
\end{tabular}
\refstepcounter{partners}\label{partner:loria}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:}
LORIA % (UMR 7503)
is a research unit common to the CNRS, the University of Lorraine and Inria. % -- is the French acronym for the "Lorraine Research Laboratory in Computer Science and its Applications".
Its missions mainly deal with fundamental and applied research in
computer sciences. Bolstered by the 500 people working in the
lab, LORIA is today one of the %
%biggest research units in Lorraine, and one of the
biggest computer science labs in France.
The Inria project team Mocqua, led by Prof. Emmanuel Jeandel is expert in models of quantum computation, quantum information theory and in particular \zx-calculus.
% Beno\^it Valiron (Assistant Prof. CentraleSup\'elec / LRI) will be associated with
%new CR1
% \REM{blah blah blah blah}
% \REM{Expertise of the organisation related to the project
% objectives. For the principal investigators give a brief CV,
% including gender, highlighting research experience; and list up
% to 5 relevant publications, and/or products, services
% (incl. widely-used datasets or software), or other achievements
% relevant to the call content. }
\textbf{Dr Simon Perdrix} is researcher at CNRS having previously held positions at LIG (Grenoble) as a charge de recherche, and at OUCS (Oxford), LFCS (Edinburgh) and PPS (Paris) as Postdoc. He is an expert of \zx-calculus introducing several new axioms to the language (1,2,3). He is also an expert of measurement-based quantum computing, introducing in particular a graphical characterisation of determinism in the model (4,5). He leads the Quantum Computation French network (GT IQ at CNRS GdR IM) and is board of the CNRS Quantum Technology network (GdR IQFA). %He has been PI of several projects (PEPS, Region Lorraine), and led work-packages in ANR and EU STREP projects. In 2016, he has been elected scientific secretary of section 6 at CoNRS. Section 6 is in charge, among other expertise duties, of hiring, promoting, and evaluating CNRS researchers in computer science.
\textit{\color{gray} \textbf{Publications:} (1) R. Duncan and ---. Graph states and the necessity of Euler decomposition. In CiE 2009, Springer LNCS 5635. (2) --- and Q. Wang. Supplementarity is Necessary for Quantum Diagram Reasoning. In MFCS 2016. LIPIcs, Dagstuhl, Germany, 2016. (3) R. Duncan and ---. Rewriting measurement-based quantum computations with generalised flow. In ICALP 2010, Springer LNCS 6199. (4) D. E. Browne, E. Kashefi, M. Mhalla, and ---. Generalized flow and determinism in measurement-based quantum computation. New J. Phys, 9(250), 2007. (5) M. Mhalla and ---. Finding optimal flows efficiently. In Automata, Languages and Programming, In ICALP 2008, Springer LNCS 5125.}
%\medskip
\textbf{Prof.~Emmanuel Jeandel} is Professor at Universit\'e de
Lorraine, leader of the Inria project team Mocqua. He did a PhD in
quantum computing, he is also an expert in dynamical systems (tiling, cellular automata). He contributed to the development of the \zx-calculus (2) %(cyclotomic supplementarity)
and, together with Simon Perdrix and Renaud Vilmart, also at LORIA, they recently proved the completeness of the \zx-calculus for a universal Clifford+T fragment of quantum mechanics (3).
\textit{\color{gray} \textbf{Publications:} (1) ---. Universality in Quantum Computation. In ICALP 2004, Springer LNCS 3142. (2) ---, S. Perdrix, R. Vilmart, and Q. Wang. ZX-calculus: Cyclotomic supplementarity and incompleteness for Clifford+T quantum mechanics. MFCS 2017. (3) ---, S. Perdrix, and R. Vilmart. A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics. LICS, 2018.}
%\medskip
% \textbf{Beno\^it Valiron} (Assistant Prof. CentraleSup\'elec) obtained his Ph.D. In Mathematics at the University of Ottawa (Canada) in 2008. He is currently assistant professor at CentraleSup\'elec and researcher at LRI (laboratoire de recherche en informatique), Orsay. His research topics on interests include quantum computation, semantics of programming languages and models of computations. %He authored 8 journal articles, 1 book chapter and 11 international workshop and conference papers. He is currently co-supervising 1 Ph.D. Student.
\textbf{Dr Beno\^it
Valiron} (Assistant Prof.\ CentraleSup\'elec) from LRI (UMR 8623)
is also included within the LORIA site.
He obtained his Ph.D.\ in Mathematics at the University of Ottawa (Canada) in 2008. He is currently assistant professor at CentraleSup\'elec and researcher at LRI (laboratoire de recherche en informatique), Orsay. His research topics on interests include quantum computation, semantics of programming languages and models of computations, he is in particular co-inventor of the Quipper language. %He authored 8 journal articles, 1 book chapter and 11 international workshop and conference papers. He is currently co-supervising 1 Ph.D. Student.
\textit{\color{gray} \textbf{Publications:} (1) A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and ---. Quipper: A scalable quantum programming language. PLDI 2013.
(2) A. Scherer, ---, S.-C. Mau, Scott Alexander, E. van den Berg and T. E. Chapuran. Concrete resource analysis of the quantum linear-system algorithm used to compute the electromagnetic scattering cross section of a 2D target. Quantum Information Processing 2017
(3) ---, N. J. Ross, P. Selinger, D. S. Alexander and Jonathan M. Smith. Programming the Quantum Future. Communications of the ACM, 2015.
(4) M. Pagani, P. Selinger, ---. Applying quantitative semantics to higher-order quantum computing. In POPL 2014.}
%\medskip
% \textbf{Renaud Vilmart}, PhD student supervised by E. Jeandel and S. Perdrix, has greatly contributed to make the \zx-calculus complete for Clifford+T quantum mechanics.
\hrulefill
\emph{Note that LORIA and LRI are administratively two different
partners. For logistic and scientific reasons, they are grouped
together in the presentation of the project.}
\hrulefill
\textbf{Role in Project:} LORIA will develop the front-end compilation of HLLs into \dzxc terms.
As one of the main contributors to the \zxcalculus and expert of 1WQC, LORIA will also play a key role in the development of \dzxc taking into account the different models of computation.
The site provides expertise both in quantum programming
languages and in the \zxcalculus.
The postdoc at LORIA
will spend half of their time on \ref{wp:frontend}, and divide the remaining time equally between the other WPs.
\end{minipage}
}
\newpage
%%%% Oxford
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 3} & University of Oxford\\
& Department of Computer Science
\end{tabular}
\vspace{1mm}\hrulefill\vspace{1mm}
\refstepcounter{partners}\label{partner:oxford}
\textbf{Expertise:} The now well over 50 members Quantum Group at the Department of Computer Science, founded and led by Abramsky and Coecke has been the world-leading group in the development of high-level computer science methods for quantum computing. It is also the birthplace of \zxcalculus, where most of the completeness result were proven, and where {\tt quantomatic} was mostly developed. Previously they coordinated the FP6 FET Open STREP QICS. The group is part of the NQIT Quantum Technologies Hub and has hosted 8 long-term EPSRC fellowships in the area of Quantum Computing. For a year now the group has an ongoing collaboration with Cambridge Quantum Computing Ltd. The Computer Science Department at Oxford is currently ranked 1st in the world.
% \REM{blah blah blah blah}
% \REM{Expertise of the organisation related to the project
% objectives. For the principal investigators give a brief CV,
% including gender, highlighting research experience; and list up
% to 5 relevant publications, and/or products, services
% (incl. widely-used datasets or software), or other achievements
% relevant to the call content. }
\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 Hadzihasanovic, 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. }
\textbf{Dr Miriam Backens} is a Career Development Fellow at Balliol College, Oxford. They proved completeness of the stabiliser \zxcalculus (1) and of the single-qubit Clifford+T fragment (2), and co-developed the related ZH-calculus as well as proving its completeness (3). \textit{\color{gray} \textbf{Publications:}
(1) ---. The ZX-calculus is complete for stabilizer quantum mechanics. NJP 16, 2014. arXiv:1307.7025.
(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{Dr Niel de Beaudrap} is a post-doctoral researcher in the NQIT project, in which he is Principal Investigator of a Partnership Project on resource-usage in networked quantum architectures and a User Project on emulating quantum computations.
He is a Co-Investigator with Prof.\ Coecke on a project with CQC to optimise quantum circuits using the \zxcalculus, co-developed the connection between \zxcalculus and lattice surgery~(1), and developed the first efficient algorithms to recover annotation systems to re-write MBQC procedures to the unitary circuit model~(2).
\textit{\color{gray}
\textbf{Publications:}
(1) --- and D.~Horsman. The ZX calculus is a language for surface code lattice surgery. arXiv:1704.08670.
(2) ---. Finding flows in the one-way measurement model. PRA~77 (022328), 2008.
}
\textbf{Dr Quanlong Wang} is on an IAA Secondment at Cambridge Quantum Computing Ltd., working on \zxcalculus. Before doing a 2nd PhD at Oxford he was a Lecturer in Mathematics at Beijing University of Aeronautics and Astronautics. He was the 1st to prove universal completeness of universal \zxcalculus. He also established a simple complete set of rules for 2-qubit circuits, which later were proved to be universally complete.
\textit{\color{gray} \textbf{Publications:}
(1) A. Hadzihasanovic, K. F Ng and ---.
Two complete axiomatisations of pure-state qubit quantum computing. LiCS 2018.
(2) B. Coecke and ---. ZX-rules for 2-qubit clifford+T quantum circuits. In RC 2018.
}
% \textbf{Prof.\ Samson Abramsky} is Christopher Strachey Professor of Computing and a Fellow of the Royal Society. He pioneered high-level methods for quantum computing (see (1) above). He received the IEEE LiCS test of time award, is a fellow of the ACM for his pioneering work in computing and was awarded the BCS Lovelace Medal in 2013.
%
% \textbf{Prof.\ Simon Benjamin} is Professor of Quantum Technologies and Associate Director and head of the ``Architectures'' WP of the NQIT Quantum Technologies Hub. He is an expert in design and architecture of quantum hardware.
% %, that is tolerant of the imperfections which first generation quantum technologies will inevitably have.
% \textit{\color{gray} \textbf{Publications:} (1) Architectures and materials for robust and scalable quantum technologies, Nature Comm.~4, 1756. (2) N. H. Nickerson, J. F. Fitzsimons, and ---. Freely scalable quantum technologies using cells of 5-to-50 qubits with very lossy and noisy photonic links. Phys. Rev. X, 4:041041, 2014.}
%
% \textbf{Dr.\ Sam Staton} is Associate Professor and Royal Society University Research Fellow specialised in programming languages, and has expertise in quantum programming languages.
%
% \textbf{Dr.\ Jamie Vicary} is a Senior Research Fellow specialised in graphical reasoning and automation thereof, in particular having produced the Globular software, an online proof assistant for higher-dimensional rewriting (\href{http://globular.science}{\color{blue} http://globular.science}).
%
% \bR \textbf{Dr.\ Dominic Horsman} is a visiting researcher at Oxford and co-inventor of the well-known lattice surgury technique for fault-tolerant computation. He has contributed greatly to applications of \zx-calculus, including the study of non-circuit quantum computational models, error-correction, and lattice surgery. \textit{\color{gray} \textbf{Publications:} (1) Surface code quantum computing by lattice surgery. ---, Fowler, Devitt, Van Meter New Journal of Physics 14 (12), 123011.}
% (2) Horsman and de Beaudrap. The ZX calculus is a language for surface code lattice surgery. QPL 2017, to appear. (3) de Beaudrap. Finding flows in the one-way measurement model. Phys.\,Rev.\,A~77 (022328), 2008.
%(2) ---. Quantum picturalism for topological cluster-state computing. New J. Phys., 13(095011), 2011. (3) N. Chancellor, A. Kissinger, S. Zohren, and ---. Coherent parity check construction for quantum error correction. arXiv:1611.08012, 2016. }
%\vspace{1mm}
\hrulefill\vspace{1mm}
\textbf{Role in Project:}
As the group where \zxcalculus\ originated \cite{Coecke:2009aa}, Oxford will continue the fundamental further development of the calculus. With its established collaboration with CQC it will also play the key role in engagement of the project with industry. A focus of this collaboration is circuit optimisations as well as compiler design, two key components of this proposal. Oxford is also the central institution in the NQIT project, which is the largest national quantum computation hardware project in the United Kingdom.
% The participation of researchers involved with NQIT, and their
% interaction with quantum technologies specialists in Oxford and
% elsewhere in Europe, will bring to the \azx project a wealth of
% expertise in quantum hardware technology projects.
The Oxford postdoc
will split their time mostly between
\newt{\ref{wp:representation}, \ref{wp:theory} and \ref{wp:usefulstuff},
including spending 20\% of their time working closely with
CQC}.
\end{minipage}
}
\newpage
%%%% CQC
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 4} & CQC\\
& Cambridge Quantum Computing Ltd.
\end{tabular}
\refstepcounter{partners}\label{partner:CQC}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:} Founded in 2014, Cambridge Quantum Computing
Ltd (CQC) is a leading independent quantum technology company
combining expertise in quantum information processing, artificial
intelligence, optimisation, and pattern recognition. The company
comprises around 50 people worldwide with the quantum software team
being 10 full-time scientists and software developers.
A major focus for CQC is the development of quantum software, in
particular for quantum chemistry and quantum machine learning. CQC
has developed \tket, a proprietary retargetable compiler for
quantum computers, which allows users to develop software using a
wide range of languages and for execution on multiple quantum
computing devices. The heart of \tket is the circuit optimisation
engine, which is informed the theory of PROPs and incorporates
many ideas derived from the \zxcalculus.
CQC have partnership agreements with IBM, Google, Microsoft,
Oxford Quantum Circuits, the National Physical Laboratory, the
NQIT project, and a variety of other public and private sector
organisations in the quantum technology space. Through these
agreements CQC has access to quantum devices not available to the
general public, and unequalled experience with multiple quantum
computing platforms. In addition, through its chemistry
simulation work, CQC also has knowledge of the kinds of programs
that users will actually want to run.
\textbf{Dr Ross Duncan} is the Head of Quantum Software at CQC
where he leads a team of 10 researchers and software developers.
He invented the \zxcalculus (with Coecke) (1) and started the
Quantomatic project (with Kissinger and L. Dixon) and has pioneered
the application of the \zxcalculus to MBQC (2), quantum error
correcting codes (3), and circuit optimisation (4,5). His current focus is
on compilation for NISQ quantum devices.
He is also a permanent Research Fellow at the University of
Strathclyde, where he was previously a lecturer in Computer
Science before joining CQC. He previously held a mandate Charg\'e
de Recherche at the Universit\'e Libre de Bruxelles and an EPSRC
postdoctoral fellowship. He was the first person to obtain a
doctorate from the Oxford quantum group, in 2006.
\textit{\color{gray} \textbf{Publications:} (1) B. Coecke and ---
. Interacting quantum observables: Categorical algebra and
diagrammatics. NJP 13 (043016), 2011. (2) --- and S.
Perdrix. Rewriting measurement-based quantum computations with
generalised flow. In ICALP 2010, Springer LNCS 6199 (3)
L. Garvie and ---. Verifying the smallest interesting colour
code with quantomatic. In Proc QPL'17 vol 266, 2017. (4)
A. Fagan and --- . Optimising Clifford circuits with
Quantomatic. In Proc QPL'18, EPTCS vol. 287, 2019. (5) ---,
A. Kissinger, S. Pedrix, and J. van de Wetering. Graph-theoretic
simplification of quantum circuits with the
ZX-calculus. arXiv:1902.03178, 2019.}
\textbf{Mr Will Simmons} is a Research Software Developer at CQC.
He obtained a Bachelor's degree in Computer Science from Cambridge
Univeristy and a Masters in the Foundations of Computer Science
from Oxford. At CQC his focus is developing new optimisation
methods for quantum circuits and high performance rewriting
techniques for graphical terms for CQC's \tket compiler.
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Role in Project:}
CQC develop the leading compiler for quantum software and the only
one which supports multiple quantum computers. We provide
expertise in implementation of compilers, integration with
hardware, and a large bank of realistic test examples. Through
its hardware partners, CQC can provide access to multiple quantum
computers via its \tket software. CQC will provide a route to
immediate industrial impact for the project.
\end{minipage}
}
\newpage%\TODOb{It should be prominently indicated that before the start of the project new team member will be hired who will also contribute, possible by list as member "postdoc TBA", "senior postdoc TBS" etc.}
%%% Gdansk
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 5} & University of Gdansk\\
& International Centre for Theory of Quantum Technologies
\end{tabular}
\refstepcounter{partners}\label{partner:gdansk}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:} The International Centre for Theory of Quantum Technologies (ICTQT) is a newly created research institute, funded by the Foundation for Polish Science, and hosted by the University of Gdansk, which is the pioneering and leading center of quantum information research in Poland. The founders of ICTQT are Marek Zukowski as the director, and Pawel Horodecki as a co-applicant, and the Centre's official foreign partner is IQOQI-Vienna of the Austrian Academy of Sciences. ICTQT aims to address the central theoretical problems of quantum technologies, with emphasis on communication methods and quantum computation. The Centre consists of 7 groups, which cover different aspects of quantum resources, quantum computation and quantum cybersecurity. ICTQT hosts leading experts in the field, including M. Horodecki and M. Pawlowski. The Centre harnesses the knowledge and skills of established researchers with strong track records on quantum information theory and the foundations of quantum mechanics, and combines it with the drive and vision of young researchers. Research highlights of the members of ICTQT include the development of (i) quantum entanglement detection and quantification, (ii) quantum security beyond pure entanglement, (iii) device-independent quantum cryptographic protocols (iv) topological self-correcting memories for quantum computing, and (v) contextuality as a resource for one-way communication.
\textbf{Dr Ana Bel\'en Sainz} is shortly to be appointed as Group Leader for the Foundational Underpinnings of Quantum Technologies group at ICTQT, Gdansk. Her team will initially consist of a PhD student (TBA) and a postdoctoral research fellow (TBA), funded by the ICTQT project, who will start in September 2019. She has previously held postdoctoral positions at the University of Bristol (UK) and ICFO (Castellfdefels, Spain). Dr. Sainz is an expert on the nonclassical properties of Nature. Her research has focused on developing an operational understanding of these nonclassical features (see e.g. (1),(3) and (5)), which enables their use as a resource for information processing tasks. Dr. Sainz also has expertise on the development of Resource Theories, which enable the quantification of the nonclassicality (i.e. the power) of these resources. Her research moreover includes the search for an understanding of both the possibilities and limitations of quantum resources (see e.g. (2) and (4)) for technological applications.
\textit{\color{gray} \textbf{Publications:} (1) A. Ac\'in T. Fritz, A. Leverrier and ---. A Combinatorial Approach to Nonlocality and Contextuality. Comm. Math. Phys. 334:533, 2015. (2) T. Fritz, ---, R. Augusiak, J. B. Brask, R. Chaves, A. Leverrier and A. Ac\'in. Local Orthogonality as a multipartite principle for quantum correlations. Nat. Comm. 4:2263, 2013. (3) ---, N. Brunner, D. Cavalcanti, P. Skrzypczyk and T. V\'ertesi. Postquantum steering. Phys. Rev. Lett. 115:190403, 2015. (4) ---, Y. Guryanova, A. Ac\'in and M. Navascu\'es. Almost quantum correlations violate the no-restriction hypothesis. Phys. Rev. Lett. 120:200402, 2018. (5) Matty J. Hoban and ---. A channel-based framework for steering, non-locality and beyond. New J. Phys. 20:053048, 2018.}
% \medskip
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Role in Project:}
ICTQT will develop the foundational aspects of \zxcalculus. The expertise of Dr.~Sainz on operational underpinnings of quantum theory will contribute to the identification of the resources of quantum speedup for computation. The work of ICTQT will be focussed primarily on WP2. The postdoc working on this site will complement the skills of Dr.~Sainz, and spend most of their time building connections between \zxcalculus and traditional approaches to the foundations of quantum resources, as well as the specific tasks outlined in WP2. Dr.~Sainz's team from ICTQT will also contribute to this work package, focusing on tasks T2.3 and T2.4.
\end{minipage}
}
\newpage
%%% Radboud Nijmegen
\fbox{
\begin{minipage}{1.0\linewidth}
\begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
\textbf{Partner 6} & Radboud Universiteit Nijmegen\\
& Institute for Computing and Information Sciences
\end{tabular}
\refstepcounter{partners}\label{partner:radboud}
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Expertise:} Situated within the largest digital security group in the Netherlands (50+ members), the Radboud Quantum Group offers strong expertise in the formal mathematical structures underpinning both quantum theory and classical programming languages. It consists of two full-time academics, one postdoc, and two PhD students. The Quantum Group furthermore maintains active relationships with the security group as a whole, including prominent members of the classical and post-quantum cryptography communities (e.g.~Joan Daemen, co-author of the renowned AES cipher; and Peter Schwabe, whose post-quantum key exchange protocol NewHope was recently trialled by Google\footnote{Nick Stratt. Google is working to safeguard chrome from quantum computers. The Verge, July 2016.}).
\textbf{Dr Aleks Kissinger} is an Assistant Professor of Quantum Structures and Logic in Radboud's Institute for Quantum and Information Sciences (iCIS). For the past 10 years, he has been instrumental in the development of the diagrammatic approach to quantum theory, notably developing the theory of classical and quantum interaction for general process theories~(1), classification of strong complementarity, and the ZW calculus~(2). He also co-authored the canonical textbook for the field~(3). He also leads development on the {\tt Quantomatic}~(4) and {\tt PyZX} tools, which serve as the platform for the software and automated techniques in this proposal.
\textit{\color{gray} \textbf{Publications:} (1) B. Coecke, C. Heunen, and ---. Categories of quantum and classical channels. Quantum Information Processing, 15(12), 2016. (2) B. Coecke and ---. The compositional structure of multipartite quantum entanglement. In Proceedings of ICALP, 2010. Springer LNCS 6199. (3) B. Coecke and ---. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017. (4) Quantomatic: A Proof Assistant for Diagrammatic Reasoning. Proceedings of Conference on Automated Deduction (CADE) 2015. Springer LNCS 9195. \href{http://quantomatic.github.io}{\color{blue} quantomatic.github.io}.}
\medskip
\textbf{Kang Feng Ng} is a postdoc working full-time on quantum circuit optimisation in the \zxcalculus. He is best known for his papers (1), (2) where he showed the \zxcalculus gives a universally complete language for quantum computation. \textit{\color{gray} \textbf{Publications:} (1) --- and Q. Wang. A universal completion of the ZX-calculus. arXiv:1706.09877, 2017. (2) A. Hadzihasanovic, ---, and Q. Wang. Two complete axiomatisations of pure-state qubit quantum computing. In Proceedings of LICS. ACM, 2018.}
\medskip
\textbf{John van de Wetering} is a PhD student supervised by Kissinger and co-developer of the {\tt PyZX} tool (1). He has contributed more broadly to applications of the \zxcalculus to the theory of quantum circuit optimisation (2) and measurement-based quantum compatutation (3). \textit{\color{gray} \textbf{Publications/software:} (1) PyZX: A quantum circuit optimization tool based on the ZX-calculus. \href{http://github.com/Quantomatic/pyzx}{\color{blue} github.com/Quantomatic/pyzx}. (2) R. Duncan, A. Kissinger, S. Pedrix, ---.
Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus. arXiv:1902.03178, 2019 (3) A. Kissinger, ---. Universal MBQC with generalised parity-phase interactions and Pauli measurements. arXiv:1704.06504, 2017}
% \textbf{Prof Bart Jacobs} is a Professor of Software Security and Correctness at Radboud, held an ERC Advanced Grant in Quantum Computation, Logic, and Security, and is a member of the National Cybersecurity Council. He has won several prestigious awards including the 2012 Huibregtsen award for Science and Society, the SURF Security and Privacy Award 2017, and is a recipient of the Dutch order of chivalry: Officer of Orange-Nassau. He has made major contributions to the formal theory of computation, including prominent textbooks on type theory~(1) and coalgebra~(2). He furthermore pioneered a new approach to modelling the logic of probabilistic and quantum systems, initiating the field of Effectus Theory~(3).
% \textit{\color{gray} \textbf{Publications:} (1) ---. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. (2) ---. Introduction to Coalgebra. Towards Mathematics of States and Observations. Cambridge University Press, 2017. (3) ---. New directions in categorical logic, for classical, probabilistic and quantum logic. Logical Methods in Computer Science, Vol. 11, 2015.}
% \medskip
% \REM{Expertise of the organisation related to the project
% objectives. For the principal investigators give a brief CV,
% including gender, highlighting research experience; and list up
% to 5 relevant publications, and/or products, services
% (incl. widely-used datasets or software), or other achievements
% relevant to the call content. }
\vspace{1mm}\hrulefill\vspace{1mm}
\textbf{Role in Project:}
The Radboud site will collaborate and offer guidance on all aspects of the project
dealing with automation and tool development, and will serve as an important point of contact with the extensive quantum hardware groups working within the Netherlands.
% , notably the DiCarlo group in Delft. The \textit{postdoc} working at this site will focus on the development of automated tools and techniques for quantum program transformation and engage with nearby quantum hardware groups to target short- and long-term applications of those techniques.
\end{minipage}
}
\newpage
\subsection{Consortium agreement principles \REM{1/2 page max} }
\label{sec:cons-agre}
\REM{(partner's rights and duties)}
\REM{(IPR management)}
The consortium commits strongly to Open Science. All scientific works
produced in the course the project will be made available to the
general public free of charge and all articles will be published in Open
Access venues. \newt{Evidence of the consortium's commitment to open access is that many members of the consortium are involved in the creation and running of the Diamond Open Access journal Compositionality.\footnote{\url{http://www.compositionality-journal.org}} } We aim at making our software available to the widest community so, \newt{for example, the code of {\tt quantomatic} and {\tt PyZX} is already publicly available.\footnote{At \url{https://quantomatic.github.io} and \url{https://github.com/Quantomatic/pyzx}.}
}
%with one exception, all APIs and source code for the software artefacts
%produced during the project will be freely available to the public,
%under a permissive Open Source license (\eg the BSD
%license\footnote{\url{https://opensource.org/licenses/BSD-3-Clause}}.)
%However, the use of Bull HPC (see \S\ref{sec:sign-facil-large})
%requires proprietary Bull technologies for the
%HPC simulation back-end module (\ref{task:HPC-sim-model}). This
%module will not be open source. However, we will also provide a
%generic reference implementation of this module, which will be
%open source.
\subsection{Significant facilities and large equipment available to
the consortium to perform the project \REM{1/2 page max}}
\label{sec:sign-facil-large}
As a partner company of IBM, Google, Microsoft and other quantum
hardware manufacturers, CQC has access to a wide range of quantum
devices and high performance simulators which are not available to the
general public. CQC will provide access to these devices to
consortium members during the project.
%Bull (Partner 4) will provide high performance computing
%(HPC) facilities which will be accessible by VPN to all project
%participants. The available HPC facilities include:
%\begin{itemize}
%\item One Atos bullion in-memory x86 server, 384 cores and 16 Tbytes RAM
%\item Nvidia P100 GPUs, as required.
%\item Altera Stratix FPGA boards, as required.
%\end{itemize}
%\BREM{TBC: ask Simon B.\ about access to NQIT's computing facilities at Oxford (Niel speculates that this would be available for NQIT related work at the very least)}
% --- The above is commented out instead of removed for the moment, but it appears that this is something we would have to budget for and so cannot be taken for granted. (NdB)
\subsection{Link with ongoing projects \REM{1/2 page max}}
\label{sec:link-with-ongoing}
\begin{itemize}
\item \textbf{Oxford}: We have a very strong
connection to the NQIT project, the United Kingdom's largest quantum
hardware technology project. de Beaudrap has been leading NQIT's software component, and more specific on the the
``Quantum/classical interface and emulation'' workpackage, and is responsible for guiding the development of a compiler for the NQIT architecture. This gives the \dzxc\ project unique access to the state-of-the-art expertise and information regarding the NQIT, and will help to ensure that the activities of the \dzxc project are directed at goals which are of direct practical relevance to practical quantum computational platforms.
% \BREM{Very close collaboration / overlap with NQIT, which is
% interested in co-operating in the development of \azx\ as a
% practical optimising compiler technology that will fits very
% tightly with the planned approach to error-corrected memories}
\item \newt{\textbf{Oxford}: We had a business collaboration and currently have an EPSRC Impact Acceleration Account with CQC, entitled ``Compilation and cost-reduction of quantum computations via ZX-calculus", which already has resulted in the proof-of-concept underpinnings of this project.\footnote{\url{https://www.mpls.ox.ac.uk/internal-research-funding/impact-and-innovation/iaa-projects}}}
\item \textbf{Radboud}: Kissinger holds a US Airforce Office of Scientific
Research (AFOSR) grant on graphical calculus and quantum circuit optimisation, using \zxcalculus,
providing him with the resources to contribute to this project.
\item \textbf{Radboud}: \newt{Kissinger holds a micro-grant from the Unitary Fund,\footnote{\url{http://unitary.fund}} which funds open source software in quantum technology, to extend {\tt PyZX} functionality with circuit routing techniques for near-term quantum hardware.}
\item \textbf{Loria}: Loria is currently working on the PIA-GDN
\emph{Quantex} project, which focuses on \emph{simulation} of
quantum computers rather than real models.
The team at Loria is also involved in the SoftQPro ANR, which deals with the
development of a new HLL related to quantum computing with a HPC
backend. \zxcalculus plays a lesser role in SoftQpro compared to this project.
\item \textbf{CQC}: In April 2019 CQC will begin a new project with the UK National
Physical Laboratory, under the Innovate UK Analysis for Innovators
scheme, which is dedicated to the modelling and analysis of noise in
quantum simulations. Further, there is a funded follow-on project
on the same topic employing 2 PhD students starting in September of
2019. This has direct link to the Task 3.3, and we expect fruitful
interaction between these two projects.
% ERC advanced grant ``Quantum Computation,
% Logic, and Security'' (QCLS) held by Jacobs. This 5-year 2.5M euro
% project will conclude during year 1 of the \azx project. Main
% outcomes: a new mathematical formalism, \emph{effectus theory}, that
% covers Boolean, probabilistic, and quantum computation in a single
% framework and an associated Python tool EfProb for modelling
% probabilistic and quantum systems. The accrued tools and expertise
% will greatly enhance our effectiveness in providing concrete tools
% related to WP3 and WP4.
\end{itemize}
\newpage%\TODOb{This needs to be done urgently}
\subsection{Financial plan (1 page)}
\label{sec:financial-plan}
\REM{The resources to be committed for each project partner have to be
described in the Electronic Submission System by the
coordinator. These resources include: Personnel, Consumables,
Equipment, Travel, Subcontracting, Provisions, Licensing fees,
other. Justify them here. Both the justification and the information
in the system will be communicated to the Evaluation Panel.}
\paragraph{Personnel}
\label{sec:personnel}
This is a large and multifaceted project, which will require
significant work to deliver. A full-time post doc at each contributing academic
site is needed, under supervision of the site lead. In addition, At
all the academic sites there is a large amount of time donated to the
project by senior scientists with relevant expertise. At CQC, our
industrial partner, a Senior Scientist and a Research Software Developer will contribute to the project.
\begin{itemize}
\item \emph{Post-doctoral researchers}: We request 30 months of salary
for post-docs at Oxford, 36+18 months at Gdansk, and 18 months at each of Grenoble and LORIA. The Oxford post-doc will also engage in co-operation with industrial partners at CQC. The post-docs
will be hired as soon as possible by the site leads at each site.
%\item \emph{Coordinator}: We request 10\% contribution the
% Duncan's salary at Strathclyde to cover the time spent managing
% the project. This is reduced from 20\% upon negotiation with
% Stratclyde. (Duncan will contribute an additional 8.4 months of
% time as a researcher, see below.)
\item \emph{Principle investigators and other named staff}: Spread
across the sites, more than 110 person-months of time
will be contributed by the named staff on the project, all of which
is supported by other sources. This means that almost 40\% of the
research effort of the project is funded from elsewhere.
\item \emph{PhD Students}: at LORIA, Titouan Carette will contribute
approx 9 months to the project; this is funded from other sources.
At Grenoble, Richard East will contribute
approx 9 months to the project; this is funded from other sources.
At Gdansk, a PhD student will contribute
approx 12 months to the project; this is funded from other sources. \newt{At Oxford, at least two PhD students will contribute to the project, as well as several MSc students}.
\item \emph{Engineers}: At CQC, a Senior Scientist and a Research Software Developer will contribute, funded from other sources.
\end{itemize}
\paragraph{Workshops}
\label{sec:workshops}
Project workshops serve a key role in intra-project communication,
dissemination, and outreach. We plan one workshop each year, in
Oxford, Nijmegen, and Grenoble. We plan to invite significant figures from the experimental and software industrial communities to supplement the project reach and expertise, which increases the cost beyond
the usual expenses of venue hire and speakers' expenses. We have
budgeted
\euro 15k for each, through the co-ordinating site budget.
\paragraph{Travel and subsistence}
\label{sec:travel-subsistence}
Since many of the personnel have expertise relevant to more than one
work package, we request substantial budget for travel, for quantERA
reporting meetings, for formal project meetings, smaller more frequent
WP meetings, and also to present our work at conferences.
\paragraph{Equipment}
\label{sec:equipment}
\begin{itemize}
\item We request laptop computers for each of the postdocs, and
replacement laptops for some staff. These are necessary
because of the frequent need to travel and work at another site
and/or present work at conferences or workshops.
\end{itemize}
\section{ETHICAL ISSUES \REM{1/2 page}}
\label{sec:ethical-issues}
\REM{Describe any foreseeable ethical issue that may arise during the
course of the research project. Describe all mitigation strategies
employed to reduce ethical risk, and justify the research
methodology with respect to ethical issues.}
No ethical issues foreseeable.
\REM{max 30 references - OK AT THE MOMENT SINCE KEVIN-ROSS ONLY IN COMMENTS}
\bibliographystyle{plain}
\bibliography{quantera}
\end{document} %%% -- uncomment to throw away notes
\newpage
\ROUGH{
\section{NOTES}
There are many proposals for the implementation of a practical quantum
computer, using diverse , and based on various These
implementations have radically different operating and
constraints from each other, and also diverge sharply from the
idealised circuits used to describe quantum algorithms. This
diversity presents an obstacle to the adoption of quantum computing
since each platform will require its software to be written
specifically for it, in terms of its own low-level machine language,
rather than using a powerful high-level languages. At the other end of
the spectrum, programming language designers usually stays at the
logical circuit level when designing their compiler. In consequence,
quantum programmers willing to go for hardware must be machine
specialists, limiting the possible exploitation of quantum computing.
Several quantum programming languages exist which
allow programmers to define algorithms in a high level way, but which
take no account of the characteristics of the underlying hardware. In
this project we will close this gap.
focus
on the front-end part of the compiler (parsing and analysis of
code), and yet be able to offer The chosen intermediate representation will
also make it easy to port the compilation chain to a new quantum
architecture, by concentrating on the translation of the
intermediate representation to the new hardware representation.
We will produce an \emph{intermediate representation} for quantum
software which will be independent of the high-level language and the
target hardware, and which will allow a variety of program
transformations such as optimisation and adding error-correction.
This language will be based on the \zxcalculus \cite{Coecke:2009aa}
, which has already been
used for similar things.
\paragraph{Quipper to ZX}
\label{sec:quipper-zx}
The Quipper language already exists and is pretty good. Thanks to
Selinger and his team there is also a good library of large scale
quantum algorithms written in Quipper. Let's take advantage of this
by writing a new back-end for the Quipper compiler. It can already
generate quantum circuit diagrams, and we know how to translate
circuits to \zx, so this should be easy. This can be used to generate
test cases to support the main activities of the project.
\paragraph{ZX to architecture}
\label{sec:zx-architecture}
The \zxcalculus can represent anything, including many things which
are not physical, or which may have no correspondence something
runnable on a given architecture. In this task we devise criteria for
(i) recognising when a ZX term corresponds to something runnable and
(ii) rewriting the term to something which can be directly translated
into the machine model. We already have two abstract machine models:
circuits and the one-way machine. Our quantum architecture partners
will help develop models which reflect more realistic hardware. Where
possible we'll actually generate ``machine code'' for these machines
(including HPC simulators).
\paragraph{Useful Magic 1: Fault Tolerance}
\label{sec:useful-magic-1}
Given the ZX term corresponding to some algorithm, we produce a
fault-tolerant version based on some error correcting code.
There has already be some work on \zxcalculus and error correcting
codes, so the basics are in place. Harder steps are to prove that the
fault-tolerant version is equivalent to the original, and establish
criteria for what transformations we can do to the fault tolerant
version without breaking the fault tolerance.
\paragraph{Useful Magic 2: optimisation}
\label{sec:useful-magic-1}
Devise tactics which rewrite a given ZX term to minimise various
metrics associated with a given machine model: e.g. T-count for
circuits, classical depth for MBQC etc. Our quantum architecture
people will help come up with suitable metrics for realistic
hardware. The \zxcalculus has some powerful normal form results which
will facilitate this. (But see the point above.)
\paragraph{ZX 2020}
\label{sec:zx-with-t}
The \zxcalculus is known not to be complete in its full generality,
nor for the Clifford + T fragment. Selinger and Bian have recently
given a complete equational presentation for the Clifford + T group.
We extend the \zxcalculus to contain this equational theory and
implement a decision procedure for equality of terms. This will make
the ZX-calculus complete enough for government work.
\paragraph{Programming constructs in ZX}
\label{sec:progr-constr-zx}
The ZX calculus has the !-box, a graphical version of the Kleene
Star. This is useful, but it's not enough to represent everything of
interest in a compact form. We will add new graph patterns to the
language to handle iteration and/or recursion, at least in limited
form. (Compare the two-stage compilation of Quipper -- the graph
patterns would be used to encode ``parameters'' in the Quipper
terminology). TO go along with this we will develop induction
principles so that we can do proofs about ZX-terms using these
constructs.
\paragraph{Quantomatic++}
\label{sec:quantomatic++}
The intention is that the results described above will be realised as
running code rather than papers. The existing Quantomatic tool may
serve as a starting point for this. Relative to the current
quantomatic we require several extensions to support new ZX features,
but also an important improvement in performance to support reasoning
with very large graphs.
}
\end{document}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End: