SHORTPROP.tex

% !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 \REM{Same as long proposal}}

\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


\section*{Relevance to the topic addressed in the call \REM{Same as long proposal}}
\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, same as long proposal)}}
\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 for easy and customisable cross-compilation; no such tools exist for quantum devices.
  Optimisation, in particular around error correction overheads, will be vital for running post-classical protocols on near-term hardware. Classically, this is an element of an integrated compiler.
  As quantum technologies will continue to be scarce and valuable, identifying truly quantum resources, currently limited to 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 \newt{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-diagram3.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, 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.
  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]}}
  
\newt{The tensor network structure means that the \zxcalculus represents initial states, unitary operations, measurements and discarding in one unified notation.
It also makes the notation vastly more 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}.
An example of such a transformation is the following:}

\includegraphics[width=\textwidth]{figures/circuit-fig}

Members of our consortium have demonstrated how to use 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 \newt{outperform
  other methods of circuit optimisation,  in the sense that certain
  circuit metric (such as total size, tree-width, or number of
  non-Clifford subterms such as T-gates) can be minimised.}  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 specifically address the theme of \emph{Quantum Computation}.
  Our goal is to develop tools to facilitate running quantum programs
on any available quantum device.
This will 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.}
}

\BREM{
\begin{itemize}
  \item Need to emphasise unique features in light of \liquid, which also claims compilation to hardware, circuit rewriting/optimisation, and error correction
  \item \textbf{novel feature:} flexibility, via intermediate language
  \item \textbf{novel feature:} formal basis (ZX-calculus, categorical semantics)
  \item \textbf{novel feature:} multiple paradigms. Notably MBQC (both team members' expertise, and in methodology) and \textbf{lattice surgery} (high-level description of logical operations on error-corrected memories)
  \item \textbf{foundational nature:} 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.
\end{itemize}
}


\paragraph{Novelty:}
\label{sec:novelty}

  Using the \zxcalculus to manage resources in quantum hardware is a totally new application of the \zxcalculus, and a totally new way to realise computations on 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.
  This provides us with great flexibility with respect to time-space trade-offs, and will help to achieve optimal implementations on diverse architectures.
Furthermore, our system allows transformations of tensor networks which cannot be expressed as equations between circuits \newt{as illustrated in the figure on the previous page}.
  In addition to these benefits, the \zxcalculus is a sound and complete formal system for transforming quantum procedures, so that each program transformation which our compiler system would realise will be provably correct, and indeed comes with a proof of its correctness.
  At the same time, the way that the \zxcalculus represents quantum procedures 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.


\REM{This project rests on more than a decade of investigations into the
categorical structure of quantum mechanics. This project therefore has a uniquely
strong theoretical foundation, and provides us with
insights unavailable to other approaches.% Repeated later
}
\REM{more}
\REM{}

\REM{Formal proofs of everything.  Formal basis (ZX-calculus, categorical semantics)}

\REM{Pure symbolic manipulation; no dimension explosion!  (\liquid
  handles up to 30 qubits -- aka 3 error corrected qubits!}


\REM{
However, as the RISC revolution in CPU design showed in the 1980s, there is no reason for
instruction sets to be optimised for human comprehension once
good compilers are available. \azx would provide a more
flexible, powerful,  interface between quantum computers and the outside world.
}

\REM{
From a formal perspective, \azx could be
regarded as a formal semantics for quantum programming
languages. However, unlike other existing semantics such as the
category CPM %~\cite{cpm}
or the language of superoperators, this model
is purely algebraic, with a graph-like representation which does not involve exponentially-sized matrices. Finally, unlike
existing semantics, we believe that it is extendable to express
computations parametric on the size of the input (such as
\emph{e.g.}~parametric families of circuits).
}

\REM{Is the following foundational ?
Although not part of this proposal, the \azx approach could
open the door to using quantum simulators for some general quantum
computation  tasks.}


\paragraph{Ambition:}
\label{sec:ambition}

  Our goal is to develop technology for a ``deep compiler'' for quantum computing systems: 
  \begin{itemize}
  \item
    one which allows for the modular design of the quantum software stack, allowing programmers to write at a high level for any hardware and any quantum error correcting technology; but 
  \item
    such that the result is a tightly integrated piece of software upon compilation, and well-tailored to the specific resources, architecture, control systems, and hardware of a specific platform.
  \end{itemize}
  %\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.

\REM{
Our central aim is to define, in \azx, (i)~a~formal tool to express formally verified code transformation and
optimisation, (ii)~a~strictly more expressive superset of the existing semantics of programming languages, and (iii)~use this as an intermediate representation to provide a scalable solution for quantum software development, which is fully independent of the hardware. To our knowledge this is the first attempt of this kind: in view of the changing landscape of backends, defining a hardware-independent IR will be challenging.
}

\BREM{(The following has been moved here from the description of \ref{task:NQIT-model} to put it more approximately where it can be of use) --- 
For NQIT, 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 be red/green copies
and products. This will certainly make the ambition here much more
achievable. 
Annotations for dealing with byproduct operations in real-time or
otherwise, particularly for magic states, is an early task to be dealt
with. It is possible that work on \azx\ might inform the way in which
NQIT networks its encoded memories together, if the problem of
resource management can be fruitfully solved with particular layouts
of logical qubits. 
}

\REM{More here}

\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.}

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.
The deep quantum compilation technology which we develop
will allow the computer to do the heavy lifting of managing resources and mapping operations onto the quantum hardware, allowing both the developers of hardware and software to focus their attentions elsewhere.
This will facilitate the development of new architectures and technologies for quantum computing.
A key example, exploited in our collaboration with NQIT, is that lattice surgery operations on surface codes do not fit into the gate model, but have natural and simple representations in the \zxcalculus \cite{BH-2017}.


\REM{
While the \zxcalculus is
restricted to qubits, the structures it uses are totally generic
\cite{Duncan2016Interacting-Fro}, permitting \azx to handle qudits or codewords in a uniform manner.
}

\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.
}

Our proposed quantum compiler technology, which we call the \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: it provides 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.

% \REM{Can do useful stuff at this level!  Some optimisation; ECC
% simple generic optimisations.  e.g.
%   \begin{itemize}
%   \item reduce T-count / gate count
%   \item coalesce Cliffords
%   \item Circuits: minimise depth
%   \item MBQC : minimise rounds
%   \end{itemize}
% }


% specifying how the tensor
% network may be realised.  This consists



The annotations of the second layer provide the basis of \emph{augmented
  rewrites}: program transformations which are 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
would generalise this concept to 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-tolerant (\ref{task:ECC}).
This would enable the \dzxc system
to 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}).
%%For example, in
% Other
%examples of annotations might include paths in the graph corresponding
%to the trajectories of physical qubits, or subgraphs corresponding to
%the primitive hardware operations and the time required to execute
%them.  For
%%hybrid architectures like NQIT, the annotations will also
%%indicate the differing behaviour of the subsystems.
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.%
%
%  (have I implemented
% the correct process?) and  layer (is the implementation
% possible/efficient/robust?).  This separation
%
%

Concrete tensor networks have a fixed finite size, whereas algorithms
are described in parametric fashion, \eg varying according the
input size.
To accommodate this, the \dzxc system would 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.
% --- The following commented out as I'm not sure what it means or if it contributes to the meaning of the proposal:
% As this information is typically erased by the circuit generation phase
% \cite{Alexander-S.-Green:2013fk,Cross2017Open-Quantum-As} of
% compilation, we effectively move the boundary between \azx and the HLL
% above the circuit-level.
This is possibly the most challenging part
of the project (\ref{task:betterboxes}); however, we have experience of
similar constructs from the \texttt{quantomatic}
project~\cite{KZ:2015:aa, Kissinger2015Quantomatic:-A-}.
\REM{[apropos to refer to PyZX here?]}

We will 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.

\BREM{
\begin{itemize}
  % \item methodology centres around common language: AZX
  % \item (\textbf{idea:} what about IZX, \textit{implemented} ZX?
  %   i.e. something more active/evocative than \textit{annotations})
  % \item this has two layers (1) the ZX-graph layer, a  technique for representing quantum processes, and (2) annotations which describe parameters as well as how process is implemented within a computational model
  % \item (1) already done (cf. ten years of research!)
  % \item (2) is guided in two ways: \textit{top-down} (capturing language features of Quipper) and \textit{bottom-up} (capturing hardware requirements)
  \item a common language synchronises the project across sites, implementation details (e.g. platform, language, etc.), and goals (optimisation, EC, simulation)
  \item development focuses around simple, modular tools, mitigating \textbf{risk} and increasing \textbf{agility} of the project as a whole
  \item 
\end{itemize}
}

\REM{
The front-end is responsible for translating a high-level programming
language to the IR.  We will adapt the existing \emph{Quipper}
compiler \cite{Alexander-S.-Green:2013fk} for this purpose. % We will
% develop static analysis techniques like abstract interpretation
% \cite{Perdrix2008} or implicit computational complexity
% \cite{DALLAGO2010377} to optimise various resources.  Such
% optimisations may be performed at the high-level or passed to the IR
% as annotations.
The front-end will later be adapted to generate the
parametric IR (see \ref{task:betterboxes}.)
}

\REM{These modules will be used to implement sophisticated
quantum algorithms which will serve as robust benchmarks
for the other WPs.   
idea of separating program compile time from circuit compile time
(following the {\em Quipper} and {\liquid} architecture).

  other objectives. Some program parameters and control flow features
  of the programming language will be translated into the \azx\
  representation.
}

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 (\ref{wp:representation}); optimisation strategies independent of implementations (\ref{wp:theory}); using annotated \zx to compile and optimise for specific quantum devices.(\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}

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 \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 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{(1 page -- this is shorter than long proposal)}}
\label{sec:impact-2-pages}

\subsection{Expected impacts}
\label{sec:expected-impacts}
%% maybe turn \subsections into \paragraphs to save space?

\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.

The project will \textbf{develop a deeper fundamental and practical understanding} of systems for quantum information processing.
We will develop a deep quantum compiler that can take input in a variety of high-level quantum programming languages, automatically add error correction, optimise the process, and output machine instructions adapted for different devices.
Creating the system necessarily will produce foundational insights into the operation and capability of quantum devices including using the \zxcalculus to identify and certify resources required for quantum speedup.
The \dzxc system will model noise, error rates, and connectivity of the target platforms and take steps to minimise decoherence, \textbf{enhancing the robustness and scalability} of quantum information technologies.

As the basis of a retargetable compiler, the \dzxc system will make it easy to support new quantum devices and thereby \textbf{identify new opportunities and applications} fostered through quantum technologies.
By providing open APIs, we will make the \dzxc system available to all academic and industrial users, thus \textbf{transferring these technologies} from laboratories to industries.
The intelligent compilation chain will make quantum programming available to non-specialists, \textbf{enlarging the community involved} in tackling the new challenges of quantum computation.
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.
This \textbf{enhances interdisciplinarity} and \textbf{crosses traditional boundaries} between disciplines.

With our newly-founded member group at the University of Gdansk, we have a \textbf{partner from the widening countries} for bi-directional knowledge exchange.
The project also involves several other research groups that have been founded in the past few years and links to QuEnG and NQIT, thus \textbf{building leading innovation capacity}.
Additionally, the team includes as PIs and Co-Is multiple \textbf{excellent young researchers}.
Our industrial partner, CQC, is an \textbf{ambitious high-tech SME} with a team leader who has expertise in technology transfer from academia to industry.


\subsection{Dissemination, exploitation of results, communication}
\label{sec:diss-expl-results}

\REM{Provide a plan for disseminating and exploiting the project results beyond the project itself.  
Results include any data produced in the framework of the project. If applicable, describe how data curation and distribution can be ensured beyond the project duration. 

Describe the proposed communication measures for promoting the project and its findings during the period of the project. Measures should be with clear objectives. They should be tailored to the needs of different target audiences, including groups beyond the project’s own community. 
Where relevant, include measures for public/societal engagement on issues related to the project.}

\paragraph{Dissemination.\!\!}
\label{sec:dissemination}
The primary means of dissemination will be by publishing our results
in leading journals and conferences.
We will target specialist quantum information venues such as \emph{Quantum Information and Computation} (QIC) or \emph{Quantum Information Processing} (QIP), mainstream computer science venues such as \emph{International Conference on Computer-Aided Design} (ICCAD) or \emph{Logic in Computer Science} (LiCS), and physics journals such as \emph{Physical Review Letters} (PRL) or \emph{New Journal of Physics} (NJP).
We support open access publishing and will aim in particular to publish in diamond open access journals \emph{Quantum} and our own \emph{Compositionality}, as well as 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 and beyond.

\paragraph{Exploitation of results.\!\!}
Through CQC, our research will be integrated with the leading quantum
software compiler system, \tket.
As \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.
The integration with the QuEnG and NQIT projects, through key members (Horsman and de Beaudrap), gives a direct pipeline to technological implementation.
%Furthermore, we will provide a programming framework for the networked quantum computer developed as part of the NQIT project, of which one of our researchers (de Beaudrap) is a key member.
We seek close collaboration with architectures teams, and will show results at the meetings including the UK Quantum Technologies annual showcase.

% \newt{Finally, we commit to produce public APIs (see
% \ref{del:frontendapi}, \ref{del:backendapi} and \ref{del:backendapiBIS})
% for the \dzxc system 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.  To further advance this aim, 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, such as \emph{Communications of the ACM} and \emph{La Recherche}.



\newpage
\section{IMPLEMENTATION \REM{(2 pages total -- shorter than long proposal)}}
\label{sec:impl-2-pages} 

\subsection{Work plan} \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).
}

\TODOb{Put some more here from actual WP descriptions.}
The work plan has four major scientific work packages (WPs),
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[{\bf WP 1}] is focussed on 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 for benchmarking.
\item[{\bf WP 2}] 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[{\bf WP 3}] 
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[{\bf WP 4}]
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.  
Our work plan consists of a balance of short tasks with concrete software deliverables and longer term, more ambitious and open-ended tasks which can offer significant, but less predictable, step-changes in the state of the art.

The early tasks of {\bf WP 1} 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 {\bf WP 2} build on a significant existing body of results and techniques for the \zxcalculus and quantum information theory.
Similarly, several tasks of {\bf WP 3} are based on known results and techniques for the \zxcalculus and rewrite theory in general. Hence, they can begin immediately.  The more challenging machine models of {\bf WP 4} are scheduled to begin in parallel with the more challenging theoretical tasks in {\bf WP 3}, 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, developing representations for recursion and control, and expressing topological and causal constraints.
Throughout the project, we will check the performance of our methods against competitors and benchmark our software using the open test-suite we will develop.

%{\bR 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.\e}

%\newpage

\def\partnerref#1{{\hypersetup{hidelinks}\ref{#1}}}
  


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\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}
\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 work packages will be done