<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">
\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{diagrams}  
\input{figures/cnot.tex}

\begin{document}

\newcommand\projtitle{Compilation and optimisation for near-term quantum computing using the ZX calculus}
\newcommand\projacro{Co-Op ZX} 

\title{QuantERA Full Proposal}   
\author{}
\date{} 
\maketitle 

\begin{center}
  {\Huge \projacro }\\
  {\LARGE \projtitle } 
\end{center}

\newpage
\textit{Title page will be replaced with file Front-Page\\
\oldt{Text from previous proposal in blue}}
 
 
\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.}  

Recent investment in quantum technologies has paid off, and quantum computers are now here. Current and near-term quantum computers, known as noisy intermediate-scale quantum (NISQ) devices,  have few qubits, short coherence times, and non-trivial gate error. In this regime, quantum software support -- in particular focussed towards compilation and optimisation -- is vital to the efficient use of scarce, noisy, hardware resources, and the development of implementable protocols that go beyond what is feasible classically.

These NISQ computers are not so much single devices, but instead patchworks of components (including classical) which vary greatly between implementations such as silicon qubits, superconducting circuits, or ion traps. Programming such devices currently requires intimate knowledge of the hardware, which is a significant barrier to the realisation of usable, scalable quantum computers, as programs must be rewritten for every new device. High-level software descriptions of quantum algorithms must be translated to low-level control instructions for quantum hardware. However, whereas classical computers have had a roughly static concept of ``low-level instructions'' for decades, the analogous notion for quantum hardware is constantly changing and evolving to cope with the rapid progress in quantum technology. We face a situation where the ever-multiplying range of quantum computers has minimal software support.

This project develops the \zx calculus of observables as a flexible intermediate language for quantum computation, and a core element in compilation for immediate use with NISQ devices. This intermediate language will be versatile enough to target a wide variety of hardware implementations, and simple enough to support any programming language. This project builds on recent significant formal and practical advances in completeness and optimisation of the \zx calculus. The former 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, enrich (with annotations), and standardise the \zx 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. 

%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, along with well-established figures at all levels in the project, 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}", both at the
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}". More generally, 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.
}

\REM{ OLDTEXT The project clearly has ``\emph{potential to initiate or foster new
  lines of quantum technologies through collaborations exploring
  advanced multidisciplinary science and/or cutting-edge engineering}'',
which is the overall objective of QuantERA.  We specifically
address the \emph{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}, both at the
intermediate and machine level.  The ability to compile multiple
high-level languages will promote the \emph{development of novel
  quantum algorithms}.  More generally, this project is an enabling
technology that multiplies the impact of all the target
outcomes of QuantERA, and prepares the stage for the Quantum
Technology Flagship.
}



\newpage
\section{EXCELLENCE \REM{(6 pages)}}
\label{sec:overview}

\newt{Very recent revisions for the new proposal are in violet}

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

\newt{%
  We propose to develop a flexible intermediate representation for quantum software, to enable formally verifiable transformations of circuits.
  This will form the basis of a re-targetable optimising compiler for  any practical quantum computer architecture based on quantum circuits.
}
\\
\textit{\bfseries\ttfamily\color{red!70!black} FIGURE NEEDS RE-DRAWING}
\vspace{-2mm}

\vspace{-1mm} 
\cgraph[0.65]{arch-diagram.pdf}\vspace{-5mm}

\paragraph{Context:}
\label{sec:context}

High-level programming languages (HLLs) increase programmer productivity and software reliability --- provided that the HLL compiler can generate machine code which runs well on the intended hardware platform. 
Quantum algorithm designers have the choice of several powerful quantum programming languages~\cite{Alexander-S.-Green:2013fk, Paykin2017a, Steiger2016ProjectQ:-An-Op, export:209634}.
\newt{%
  However, these languages do not describe how to realise programs on specific hardware platforms, of which there are several, using different technologies (ion traps, superconducting circuits, optics) and architectural concepts (networked vs.\ hybrid, ancilla driven, measurement based)~\cite{PhysRevX.4.041041,Raussendorf-2001,KendonAncilla}.
  Even at such a time as quantum hardware technology matures, we cannot be assured that exactly one platform will predominate for all quantum information processing applications.
}
For classical programs, modern compiler toolchains such as LLVM\footnote{%
  The LLVM Compiler Infrastructure, \url{http://llvm.org}}
decouple the HLL from the machine by using an \emph{intermediate representation} (IR), which is independent of both.
By translating to and from the IR, any HLL may be used on any platform.
A quantum IR accommodating dissimilar architectures is needed to support software on rapidly shifting hardware.

\paragraph{Targeted breakthrough:}
\label{sec:targ-breakthr}

\newt{%
  We will define a versatile and universal intermediate representation language,
}
called \azx, which is platform-agnostic but which facilitates program
transformations appropriate to specific hardware. 
Specifically, \azx will provide the following (see \S\ref{sec:impl-2-pages} for more detail):
\begin{itemize}
\item
  \newt{An easily-specified and easily-generated universal language for quantum transformations.}
\item
  Automated IR transformations for error correction, resource optimisation, and execution layout.
\item
  A complete compilation pipeline from HLL to hardware for (i)~superconducting transmon qubits \oldt{(QuTech)~\cite{Versluis2016Scalable-quantu} and (ii)~optically-coupled ion traps (NQIT)~\cite{PhysRevX.4.041041}}.
\end{itemize}
\newt{%
  The theory, algorithms, and software architecture behind this will be flexible and extensible.
  This will permit programming languages and architectures not explicitly included in the project scope to be supported.}
This will greatly improve the software ecosystem for quantum computers: by supporting \azx, future quantum devices may 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}

\newt{%
  The closest extant thing to a quantum IR is QASM~\cite{Cross2017Open-Quantum-As}, a circuit description language.
  QASM is the input language for IBM's quantum computing platforms, including the \emph{IBM Quantum Experience}\footnote{%
    This is a publicly accessible 5-qubit device; \url{http://research.ibm.com/quantum/}.}.
    QASM is an output option for ProjectQ \cite{Hner2016A-Software-Meth};
    the ProjectQ team describe a compilation process for quantum software involving possibly multiple IRs, but do not describe a specific one.
}
State-of-the-art quantum programming languages such as Quipper~\cite{Alexander-S.-Green:2013fk}
\newt{and Q\#~\cite{qsharp}}
support multiple targets; in practice the choice
is between a circuit description or a classical simulation.
%(\liquid in particular is tightly integrated with its simulator).  
Neither language exposes an IR.

\newt{%
  Our proposed IR is built on the \zxcalculus~\cite{Coecke:2009aa}, a graphical tensor notation developed by members of this consortium during a decade of work on the mathematical foundations of quantum computing \cite{AbrCoe:CatSemQuant:2004,
%Coecke:2009db, CDKW-lics:2012qy, 
 Coecke2017Picturing-Quant}.}
The \zxcalculus can be viewed in two distinct ways:
\newt{%
  either as a formal axiomatic theory which encodes the properties of complementary observables in categorical algebra; or 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.  
\newt{%
  Recently, members of our consortium developed versions of the \zxcalculus which were complete for Clifford+T computations~\cite{Jeandel2017A-Complete-Axio,NW-2018} and for  quantum computations including CNOTs and arbitrary single-qubit gates~\cite{NW-2017,JPV-2018}.
  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 can easily describe computations in both the circuit and measurement-based models of quantum
computation (MBQC)~\cite{Raussendorf-2001}.
% a proven track record in
%quantum computation, in particular treating error correction
%\cite{Horsman:2011lr,Chancellor2016Coherent-Parity}, and translating between
%architectures \cite{Duncan:2010aa}.
Due to its great flexibility and expressive power, the \zxcalculus 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}.
\newt{Its graphical representation is especially well-suited to describe systems having a natural have graph structure.
Examples include 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.}
Here is an example of such a transformation:\vspace{-1mm}
\\
\textit{\bfseries\ttfamily\color{red!70!black} CONSIDER USING DIFFERENT FIGURE}
\vspace{-2mm}%
   % (see Figure~\ref{fig:zx-mbqc-cnot}).
  \[
    \cnoti[0.7] \rTo^* 
    \cnotii[0.6] \rTo^*
    \cnotiii[0.6] \rTo^*  
    \cnotiv[0.6] \rTo^* 
    %\cnotv[0.6] \rTo^* 
    \cnotvi[0.7]
  \]~\\[-4mm]%
\newt{
  Furthermore, members of our consortium have also incorporated these formal reasoning techniques into 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 perform circuit optimisation.
\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}.  The
goal of \azx is to make it easy to run 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}

\azx is a totally new way of representing computation. 
Tensor networks specify \emph{what} the program should do, augmented with separate instructions for \emph{how} the hardware should do it.
Unlike sequences of gates, these tensor networks have no preordained causal structure beyond the global input and output.
This gives the \azx system great flexibility with respect to time-space trade-offs, and will help to achieve optimal implementations on diverse architectures.
\newt{Furthermore, our system allows} transformations of tensor networks which cannot be expressed as equations between circuits.
\oldt{Key examples include powerful normal-form theorems for Frobenius and Hopf algebras.}
\textsf{\bfseries\color{red!70!black} [I think that we need a better selling point here --- N]}

% to reduce its terms to minimal forms.  This flexibility has been
% exploited in the \zxcalculus to convert between the circuit model and
% the MBQC model via intermediate steps not expressible in either model
% \cite{Duncan:2010aa,Duncan:2012uq}.

\newt{%
  Another novel and essential element of our project is that the basis of the \azx, the \zxcalculus, is a formal equational theory: this implies that our program transformations are provably correct, and indeed will come with proofs of their correctness.
}
This symbolic approach also avoids \newt{the immediate dimensional explosion} of explicit matrices.

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

\newt{%
  Our goal is to develop a vertically integrated system to construct a program's implementation, from its specification in a high-level language, and the characteristics of the target machine, for two different quantum computing architectures (\ref{task:delft-model}, \ref{task:NQIT-model}).
  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.}

\newt{%
  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 \azx system 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.
} 

\oldt{Our proposed \azx language 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 power of \azx comes from 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.

% (for ``\emph{annotated} \textsc{zx}'') % rwd - taking this because
% the previous sentence gives 3 possibilities for A... and Z and X
% don't stand for anything either!
\azx will retain the mature and effective formal tensor language of
the \zxcalculus at its heart, ensuring semantic soundness, logical
completeness \cite{Jeandel2017A-Complete-Axio,NW-2017}, and allowing
techniques from earlier work (cf.~\texttt{quantomatic}
\cite{Kissinger2015Quantomatic:-A-}) %, as well as new techniques developed as part of this project,
to be applied to \azx terms.  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




\oldt{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}.
We propose to 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, we would develop 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}).
We may then attempt to re-write procedures, to minimise the number of operations subject to the constraints described by those annotations.
We may further elaborate such a system of annotations by a description of 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:backends}), 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 we introduce a second class of
annotations to represent limited forms of iteration and recursion, yielding \emph{parametric} \azx terms.  While the hardware-derived
annotations are inferred in a bottom-up fashion, the parametric
structure is produced top-down, based on the original HLL program.  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-}.


Early in the project, we will implement translations from existing
quantum programming languages~(\ref{task:trans1}).  These will provide
 examples and test cases, and allow comparative
evaluation.} % of the \azx system.  %We will adapt an existing compiler to generate parameterised \azx terms (\ref{task:trans2}).

% Due to the fact that there exist ZX-based software, additional features were added to the language e.g.~`bang-boxes' which are formal incarnations of the ``..." occurring in the above equations. 


% \REM{Summarise WPs in light of this setup}

% \REM{Interrelations of goals and separation of concerns}

% \REM{Risk assessment: which are easy, which are hard?  Dependencies.}

\REM{WHY this is a good idea.}





%\TODOb{Nowhere it is explained what the A in AZX means.}
\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:backends}); optimisation strategies independent of implementations (\ref{wp:theory}); using enriched \zx to compile and optimise for specific quantum devices.(\ref{wp:usefulstuff}).

\subsubsection{A quantum compiler stack}
\label{sec:progr-lang-supp}

\oldt{In the quantum setting, several powerful high-level languages
(HLLs) such as Quipper~\cite{Alexander-S.-Green:2013fk} and \liquid
\cite{export:209634} have been proposed.  As in the case of their
classical counterparts, these HLLs are not designed to be run directly
on quantum hardware, rather their compilers typically output quantum
circuit descriptions.
Rather than designing a new programming language, we propose a quantum
IR, \azx.  Unlike the languages mentioned above, \azx is not intended
to be written by humans\footnote{This said, the \zxcalculus has proved
  a very useful notation for mathematical proofs.}, instead it will 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 \azx.

Since most existing quantum HLLs can output circuit descriptions, and
since circuits can easily be represented in the \zxcalculus, we first
design a simple front end for the circuit language
QASM~\cite{Cross2017Open-Quantum-As} in 
\ref{task:transQASM}.  This will allow \azx terms to be produced from
virtually any extant quantum HLL, albeit rather naively.
Later, we will perform concrete front-end experiments using more
sophisticated existing HLLs, for example \emph{Quipper},
\liquid, or ProjectQ \cite{Steiger2016ProjectQ:-An-Op} during the
long running task~\ref{task:transHLL}.  

This work package consists of a back-and-forth interaction between
HLLs and \azx, which is why many of its tasks span the entire lifetime
of the project. HLL development influences \azx by providing the
control structures and other constructs that must be represented at
\azx level. Conversely, \azx developments will influence HLL, as we
analyse how information and requirements from the back-end flow upward
in a meaningful way, and how this can be translated into compilation
flags and assertions/hints to the compiler within HLL programs. 

The open database of tests developed in \ref{task:testBench} will
serve as a measuring tool for the quality of the output. The database
will also be made available to the community for rating and testing
future compilers or optimisation techniques.  To encourage interaction
from other research groups, and to support other languages, both our
interface and the \azx language will be made
public.

Proposed and existing quantum devices differ along a variety of axes.
At the most abstract level, the quantum circuit model and the
1-way model \cite{Raussendorf-2001} have different execution
concepts and primitive operations, despite their computational
equivalence.  More realistic models might suffer from 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.\REM{noise,fidelitY} In a hybrid architecture like NQIT, these
properties will vary across the subsystems, with concomitant
implications for the execution of the desired program.

Since the overall goal of the project is to produce a
\emph{retargetable} compiler, able to generate executables for
multiple architectures, these differing characteristics must be taken
into account.  The ability to synthesise hardware-appropriate
implementations from abstract descriptions is one of the major novel
contributions of this project. 
%
Towards this objective, in \ref{wp:backends} we model the performance
characteristics and architectural constraints of various idealised and
realistic machines, and develop language features of \azx to express
these properties.  The goal is two-fold: to facilitate
\emph{code-generation} for a given machine from an \azx term; and to
expose information needed by the \emph{optimiser}.}



\subsubsection{Representation, reasoning, and resources}
\label{sec:machines-models}

\REM{stuff about WP 2 here}

\oldt{
A key research challenge of this work package consists in the
management of the {\em classical computation} and {\em classical
  information} within quantum algorithms: What computation should
occur at the \azx-generation phase, and which classical parameters are
passed on to the \azx terms? To help answer this question we will
design a test suite (\ref{task:testBench}) to compare possible
solutions.


Due to its novelty, we adopt an exploratory approach.  Initially, and
in parallel, we study the circuit model (\ref{task:circuit-model}) and
the 1-way model (\ref{task:mbqc-model}) because these models are well
understood, stable, and have been extensively treated in the
\zxcalculus literature.  We will use these examples to develop
prototypical \azx constructs expressing the relevant properties.  This
consists in three tightly related tasks: decomposing the tensor
network into atomic operations; characterising runnability with
respect to the model by predicates in monadic second order logic; and
transforming the tensor network into an equivalent runnable version.
This experience will inform the later work in \ref{wp:theory} and
\ref{wp:usefulstuff}.

While in the early stages of the project, 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 task
\ref{task:betterboxes}, we will extend \azx 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.
}


\subsubsection{Machine-independent optimisation}
\label{sec:repr-reas-azx}

\oldt{The formal mechanisms for transforming the \azx diagrams produced by
HLL compilers into optimised, physically implementable computations
are the theoretical core of this proposal, and developing effective
techniques for working with \azx diagrams are a prerequisite for our success.

Recent breakthroughs in the theory of the \zx-calculus
\cite{Jeandel2017A-Complete-Axio,NW-2017}, have shown that whenever two
\zxcalculus diagrams describe the same linear operator, then one can be
transformed into the other using just a finite set of local,
diagrammatic transformations.

However, completeness of the \zxcalculus is just the beginning of the
story for \azx. 
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
task~\ref{task:algorithms}, we will employ theoretical and automated
techniques drawn from rewrite theory to search for better
presentations of the Clifford+T \zx-calculus and develop strategies
for effectively simplifying \zx-diagrams. These include Knuth-Bendix
completion and theory synthesis.
In task~\ref{task:axioms}, we will extend the
\zx-calculus in two dimensions. 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. 

Finally, we will construct a theoretical framework which mediates the
abstract rewrite theory of \zx-diagrams and real-world constraints
coming from quantum hardware. In task \ref{task:annotate1}, we will
extend the language of \azx 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.  We will then
develop the formal tools for rewriting \zx-diagrams in ways that
respect those constraints.  Similarly, 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.}



\subsubsection{Machine-dependent optimisation}
\label{sec:comp-quant-softw}

\oldt{
In the second phase we switch attention to real computers.  The first
target is a classical simulator running on HPC hardware provided by
our industrial partner Bull.  This will leverage existing expertise in
simulation, combined with new techniques for symbolic evaluation of
\azx terms.  \ROUGH{Finally we study two concrete quantum computers
  based on different technologies: superconducting circuits (Delft)
  and optically linked ion traps (NQIT).}  In both cases we will
interact strongly with the experimental groups working on these
models, who are either members of our consortium (S. Benjamin and
N. de Beaudrap for NQIT) or our advisory board (L. DiCarlo in Delft).
Since these architectures are dissimilar, tackling both is an ideal
demonstration of our approach.  The completion of this phase will
allow quantum programs represented as \azx terms to be run on real
hardware.

  An \azx term produced by the compiler front-end is, by design, an
abstract tensor network, perhaps annotated with some useful
information, but generally without any preconception of how it should
be executed on any particular machine.  Translating such
abstractly-described procedures to code that can run on realistic
machines is a key objective for the project.  WP4 is responsible for
developing the tools to do so.  This work package represents the most
technically involved and multi-disciplinary component of the \azx
project, requires the integration of the theoretical work of
\ref{wp:theory} and generalisation from the specific machines
considered in \ref{wp:backends}, and will result in software forming
the basis of a general-purpose quantum compiler.

We identify three main tasks: to add suitable error protection to the
program; to optimise the program according to whichever resources are
most appropriate for the given machine; and to layout the program for
execution.  Although we treat them separately, in practice these tasks
will interact in non-trivial ways, and their order need not be fixed.

Error correction should be performed automatically.  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'' \azx terms to
error corrected / fault-tolerant versions of the same program;
additional annotations will be added to ensure that other program
transformations 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.  Second,  optimisations which take into
account the resource models of a specific machine, expressed through
annotations, cf.~\ref{task:annotate2}.  This might be applied before
or after layout, depending on the circumstances.  Layout will be handled
in a similar way to this second kind of optimisation, generalising
from \ref{task:delft-model} and \ref{task:NQIT-model}.

Although we will provide specific modules for the tasks described above, the
\azx system is intended to extensible, so we will also 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}). 

The tasks to be performed within WP4 may be broadly described in terms of how the \azx compiler 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: (i)~an initial round of generic, hardware-independent optimisations; (ii)~application of some choice of strategy for error correction; (iii)~translation to a specialised annotation system which represents the parameters and constraints of a specific hardware implementation; and finally (iv)~another round of optimisation within the constraints imposed by the error correction and hardware models.
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 \azx compiler to arbitrary hardware systems and allowing \azx to act as a general-purpose quantum compiler.

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

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



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 WP2, 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 translation to the machine language of the target architecture) is a final round of optimisation, this time applied to \zx terms within 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} \BREM{[and \ref{task:annotate2}?]} 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 make possible a reduction in the resources used in any particular hardware platform without requiring the use of bespoke techniques for each target architecture.

Annotation systems representing the hardware implementation are to be provided by the development environment, using a standardised interface.
By providing public documentation for this interface~(\ref{task:backendapi}), we enable third-party developers to extend the functionality of the \azx compiler to arbitrary platforms, thus ensuring the suitability of the \azx compiler as part of a general-purpose quantum software development platform.}


\subsection{Interdisciplinary nature}
\label{sec:interd-nature}

\oldt{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 \&amp; 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.  Just
as \azx itself is an intermediary, 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{(3 pages)}}
\label{sec:impact-2-pages}

\subsection{Expected impacts}
\label{sec:expected-impacts}

\oldt{
\azx significantly advances the state-of-the-art across four of the
five expected impacts.% the fifth is out of project scope.

\paragraph{Develop a deeper fundamental and practical
  understanding of systems and protocols for manipulating and
  exploiting quantum information ---\!\!}

This project will take practical insights into the workings of diverse quantum technologies, along with fundamental techniques in quantum information processing, and embody them as software in the \azx toolchain. By embodying this expertise in software, practitioners can employ push-button optimisations and fault-tolerant transformations of programs without a deep understanding of the underlying theoretical techniques, effectively making these techniques available to a broader audience.

The \azx language will connect both high-level (algorithmic) and low-level (physical) representations, enabling the specifics of individual devices to be translated into constraints on the design of protocols. For instance, causal and topological structure is a crucial restriction on what can be processed in networked computing, and incorporating this into \azx will allow novel and efficient protocol design.
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 \azx). 
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 ---\!\!}
  
\azx will provide a robust and scalable intermediate representation
for quantum programs, which will help minimise the resource
requirements in quantum technologies. \azx is also a practical tool to manage and track the resources required to
realise operations on different hardware platforms.
The annotation layer of \azx can model environmental noise and error
rates of the target platform, allowing the compiler to make provisions to minimise
decoherence as the program runs.  In particular, the annotation layer of \azx can be used for
fine-grained resource management for lower levels of error correction
as well as idealised quantum memories, allowing integration of
compilation and protection of coherence. 
\azx will enhance the development of error correction that is tailored to specific devices.
Individual noise models and error propagation will be encoded in the language through the annotations,
which can then be used for optimisation of error correction procedures. Using \azx as a design tool, specific error correction protocols can be developed for different devices, customised to the different noise models. These models will be flexible as the devices get larger, ensuring scalability of robust devices. Networked scalability can be optimised for, as well as different topologies, by encoding timing and spacial constraints in the language. 
As \azx will be a common representation, hybrid devices can also be optimised for. Error correction or mitigation strategies can be developed across multiple devices acting in tandem.
Modelling error correction in \azx will thus enable the design of new error correction procedures, optimisation of existing ones, and give a mutually-intelligible language for error correction theorists and device technologists.

\paragraph{Identify new opportunities and applications fostered
  through quantum technologies, and the possible ways to transfer
  these technologies from laboratories to industries ---\!\!}

%doing cool stuff with cool stuff

The retargetable \azx system will make it easy to support new quantum
devices, thus making the latest developments
in quantum technology available to all academic and industrial users,
and maximising the return on investment in quantum computing.  Our
consortium includes an industrial partner (Bull) to help ensure
the industrial relevance of our work. 
We also have further industrial figures on the advisory panel.
With \azx as a common intermediate language, high-level quantum languages and
protocols can be designed without needing to know the underlying hardware. 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 specified fully in \azx
and then integrated into a large or hybrid device.
This will accelerate the widespread commercial and academic development and exploitation of quantum technology.  

}

% and programming languages
% will become more easily transferred 

% accelerating the widespread exploitation of
% quantum technology.  

% to different hardware platforms,



% and accessible to both academia and industry.  

  \oldt{
\paragraph{Enhance interdisciplinarity in crossing traditional
  boundaries between disciplines in order to enlarge the community
  involved in tackling these new challenges ---\!\!}

%The inherently interdisciplinary nature of this project will bring a larger community to bear solving problems during the lifetime of the project. The development of the \azx language and compiler stacks themselves will also open up further challenges as the project progresses (and beyond) that are accessible to broader communities. 
\azx will connect the entire range of knowledge involved in building quantum technologies, from experimental and theoretical Physics, through to quantum computing theory, and on to formal methods of Computer Science. All of these are needed to develop the language and its applications. Developing \azx is a fundamentally interdisciplinary task, and the resultant language will itself be a common method of communication between different disciplines. This opens the prospect of an acceleration in the development of quantum algorithms in a way which can then be easily ported to many different hardware platforms. % that will enable them all to co-ordinate in the further development of quantum technologies.
For example, algorithm and protocol designers will not need to interface directly with quantum technologies: the \azx layer does all the compilation and optimisation necessary. This will allow the
integration of quantum computing into mainstream Computer Science, and so the easy importing of tools (for example, techniques for optimisation or verification) that have been developed over many years. 
By aiding the development of intuitively accessible programming languages, \azx will also make quantum technologies accessible to a broader range of users and developers. End-users outside quantum physics and computer science will be able to build protocols for use in their own field that do not require them to understand the physical action of the hardware.

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 overcome these limitations within the project and in the wider community.}



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

\paragraph{Dissemination.\!\!}
\label{sec:dissemination}

\oldt{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), \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), and the recently
  established open access journal \emph{Quantum}.
\end{itemize}
The consortium members have a strong record of publishing in these
leading venues.  Other venues will targeted opportunistically in order
to achieve the most timely publication of our results.

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

\oldt{We propose several direct and indirect routes to exploitation of our
results.  Firstly, our consortium includes an industrial partner
(Bull) and members of the NQIT project (Abramsky, Benjamin, de
Beaudrap).  With Bull, our work will be incorporated into state of the
art products for simulation of quantum systems.  With NQIT, we will
provide a programming framework for the networked quantum computer
developed as part of that project.  As part of this we will present
the project results at the semi-annual NQIT Industry Forum events and
the UK Quantum Technologies annual showcase.  To further this aim, our
postdoc in Oxford will spend 10--20\% of their time working closely
with the NQIT project.  In both cases, our work can be exploited
directly by end-users.

In addition, we have also recruited a board of advisers (see below)
including the European leaders in scalable quantum devices.  These
experts will participate in our annual workshops to help define
requirements and ensure that our work can be used by their projects.
The DiCarlo group (Delft) and Rigetti have shown particular interest
in exploiting our work to assist with supporting the superconducting
quantum devices they are developing.

Finally, we commit to produce public APIs (see
\ref{del:frontendapi} and \ref{del:backendapi})
for the \azx 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 \azx 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 open access publishing and open source software, 
\oldt{
To communicate of our work to a wider audience, and to take advantage
of wide public interest in quantum technology, we will perform a
variety of outreach activities.  Firstly, we will adopt ``open
lab-book'' research, publishing work-in-progress on a project wiki,
and articles aimed at a general audience on a project
blog.\footnote{The success of \emph{Graphical linear algebra}
  (\href{http://graphicallinearalgebra.net}{\color{blue} graphicallinearalgebra.net}, 217K visitors since 2015) demonstrates there is a clear audience for such works.}
To allow end-users to experiment with \azx, Bull will
provide an HPC simulator with a publicly accessible front end, which
will also be incorporated into the project website.

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}.
\item French: \emph{La Recherche}, \emph{Pour la Science}, and
  \emph{Interstices}.
\item Dutch: \emph{Kijk Magazine}, \emph{Quest}, and the dutch edition
  of the \emph{New Scientist}.
\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 Board:\!\!}
\label{sec:advsiory-board}

\oldt{
In order to ensure the maximum impact, and to complement the expertise
present in the consortium, we have recruited a board of
advisors who will consult with the project.  The board includes
several leading European researchers working on scalable quantum
devices; their input will help ensure that our software stack is able
to support real devices, and they form a ready base of
users for the final products.  The board comprises:
\begin{itemize}
\item Leonardo DiCarlo (QuTech\,/\,Delft), 
\item Jonathan Pritchard (Strathclyde),
\item Peter Selinger (Dalhousie), 
\item Andreas Wallraff (ETH Z\"urich), 
\item Philip Walther (Vienna), 
\item Will Zeng (Rigetti Quantum Computing).  
\end{itemize}
Letters of support from the board members are attached at the end of
this document.}


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

\oldt{The work plan has four major scientific work packages, each focusing
on a different \emph{theme} within the project.  The work packages
will proceed in parallel, and all will have at least some activities
throughout the length of the project.  (There is also a fifth
work package grouping administrative and organisational activities.)
\begin{description}
\item[\ref{wp:frontend}] is focussed on translating from HLLs into
  \azx, reflecting higher level programming constructs into \azx, and
  building a test suite of programs.
\item[\ref{wp:backends}] is about modelling the properties of
  different machines in \azx, and translating \azx to hardware.
\item[\ref{wp:theory}] develops the theory behind \azx and algorithms
  to realise the logical ideas.
\item[\ref{wp:usefulstuff}] 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}

\oldt{
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
\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:transQASM} and \ref{task:HPC-sim-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.

Except for \ref{task:transQASM}, the 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.

The early tasks of \ref{wp:frontend} and \ref{wp:backends} are quite
practical and don't require much preparation to begin. They will provide
useful experience for the later tasks.

The first two tasks of \ref{wp:theory} build on a significant existing body of results and techniques for the \zx-calculus and rewrite theory in general. Hence, they can begin straight away. 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:annotate1} and \ref{task:annotate2}.

The more challenging machine models of \ref{task:delft-model} and
\ref{task:NQIT-model} are scheduled to begin in parallel with the more challenging theoretical tasks in WP3, anticipating a great deal of back-and-forth interaction between these two aspects of the project.

%  delayed until sufficient theory has been
% developed to attempt them.

\ref{wp:usefulstuff} requires integrating and generalising many of the
ideas of \ref{wp:backends} and \ref{wp:theory}, so it is mostly
scheduled toward the end of the project.

\begin{figure}[h]
  \centering
  \input{pertchart.tex}
  
  \caption{Dependencies and interactions between tasks}
\label{fig:pert}
\end{figure}

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
\subsection{Work Packages \REM{1page per WP}}
\label{sec:work-packages}

\begin{WP}{A quantum compiler stack}{1M}{36M}{wp:frontend}
\WPleaderLOR
\WPeffort{0}{0}{0}{0}{0}{0}
\begin{WPaim}
This WP develops elements of \zx as in intermediate compiler language. 
This includes interfaces between \zx and up to known high-level quantum languages (HLL), and down to the device level of the target technologies.
In the first instance we make contact 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:circuit-model}]{Idealised quantum circuits
    (M1--M9; Responsible 2; Involved: 1,3,4)}{%
    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--M12; Responsible 3; Involved: 1,2)}{%
    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: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, this task will also make it possible to test
%    the {\azx} framework on real, possibly very large instances of
%    programs. This task will progressively incorporate new features
%    of the \azx language as they are developed,
%    especially in concert with \ref{task:betterboxes}.
%    %
%  }
  %
  \WPtask[\label{task:trans1}]{Open API for AZX terms (M1--M36;
    responsible 3; involved 2,4,5)}{%
    Develop an open API for the description of \azx terms. While
    largly 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 \azx as they
    become available. This task is tightly linked with
    \ref{task:betterboxes}.
    %
  }
  %

  \WPtask[\label{task:testBench}]{Open test-suite (M3--M36;
    responsible 3; involved 2,4,5) }{%
    Devise a 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:backendapi}]{Back-end API (M24--M36 Responsible: 5; Involved: 1,2,3,4)}{%
      Open specification of an API for back-end modules, facilitating third-party  development of specifications of target architectures, providing the \azx 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 \azx API}
  % 
  \WPdeliverable{M12}{Preliminary benchtests of circuits and algorithms}
  %
  \WPdeliverable{M15}{Module for generation of 1WQC code from \azx terms}
  %
  \WPdeliverable{M30}{Advanced front-end for Quipper and one other
    HLL -- updated API}
  %
  \WPdeliverable[\label{del:frontendapi}]{M36}{Finalized API, test-suite and front-ends}
    \WPdeliverable[\label{del:backendapi}]{M36}{API for back-end
    modules, including specification language for architectures.}    
\end{WPdeliverables}
\end{WP}


\newpage

%%%
%%%%%%%WP 2
%%%
\begin{WP}{Representation, reasoning, and resources in \zx}{1M}{36M}{wp:backends}
\WPleaderPOL
\WPeffort{0}{0}{0}{0}{0}{0}
\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.
\end{WPaim}
\begin{WPtasks} 
    \WPtask[\label{task:axioms}]{Beyond qubits and stabilisers 
      (M1--M12; Responsible: 2; Involved: 1,3,5)}{%
    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.
    % and exploit the translation from \textsc{zx}-    to \textsc{zw}-calculus.
    }
  \WPtask[\label{task:betterboxes}]{Control in \zx
    (M1--M18; Responsible: 1; Involved: 2,3,5)}{%
    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. 
    }
      \WPtask[\label{task:resources}]{Resources and axioms
    (M1--M18; Responsible: 1; Involved: 2,3,5)}{%
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
    (M1--M18; Responsible: 1; Involved: 2,3,5)}{%
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{M12}{Deliverable.} 
  \WPdeliverable{M15}{Deliverable.} 
  \WPdeliverable{M24}{Deliverable.} 
    \WPdeliverable{M36}{Deliverable.} 
\end{WPdeliverables}
\end{WP}


\newpage

%%%
%%%%%%%WP 3
%%%
\begin{WP}{Machine-independent optimisation}{M1}{M36}{wp:theory}
  \WPleaderOXF
  \WPeffort{0}{0}{0}{0}{0}{0}
  \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 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--M24; Responsible: 5; Involved: 1,2,3)}{%
      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. Implement these strategies in
      software and give bounds on computational complexity.  
    }

    \WPtask[\label{task:annotate1}]{Topological and causal constraints 
      (M13--M24; Responsible: 2; Involved: 1,3,5)}{%
      Extend \azx 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: 2; Involved: 1,3,5)}{%
      Extend \azx 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 
      (M12--M24; Responsible: 3;   Involved: 1,4,5)}{% 
      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--M24; Responsible: 5; Involved: 1,2)}{%
        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{M24}{A library of general-purpose techniques and
      algorithms for simplifying \zx terms} 
        \WPdeliverable{M24}{Algorithms and heuristics for optimising \zx
    terms, including minimisation of T gate count}
  \WPdeliverable{M24}{Routines for adding error-correction to \zx
    programs}
    \WPdeliverable{M24}{An extended \zx language which expresses
      topological and quantitative properties, with associated
      reasoning techniques}
  \end{WPdeliverables}
\end{WP}

\REM{\emph{Leader:} Coecke.
\emph{Others:} de Beaudrap, Duncan, Jacobs, Jeandel, Kissinger,
Perdrix, Valiron, Vilmart.}

% 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}{1M}{36M}{wp:usefulstuff}
  \WPleaderGREN
  \WPeffort{0}{0}{0}{0}{0}{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 quantum dot devices 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 \ldots.
Also machine-dependent error correction here?
  \end{WPaim}
  \begin{WPtasks}
\WPtask[\label{task:Si-model}]{Grenoble quantum dots (M13--M36  Responsible: 2;
  Involved: 1,5)}{
  We will model the quantum dot device 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
  and 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:delft-model}]{Oxford ion traps (M13--M30  Responsible: 5;
  Involved: 1,2)}{
  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:runnable}]{Formatting for target systems 
    (M15--M30; Responsible: 2; Involved: 1,3,5)}{%
    Develop algorithms which, given a collection of constraints
    representing a machine model
    (c.f.~\ref{task:annotate1}, \ref{task:annotate2}), re-writes \azx 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:opt-machine}]{Model-guided optimisation 
      (M21--M36; Responsible: 5; Involved: 1,2,3)}{%
      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{M24}{Deliverable}
  \WPdeliverable{M24}{Deliverable}
  \WPdeliverable{M30}{General purpose layout engine}
  \WPdeliverable{M36}{Optimising compiler for \azx, suitable for compiling to Grenoble and/or Oxford architecture}    
  \WPdeliverable[\label{del:backendapi}]{M36}{API for back-end
    modules, including specification language for architectures.}    
  \end{WPdeliverables}
\end{WP}

\REM{\emph{Leader:} Kissinger.
\emph{Others:} Abramsky, de Beaudrap, Duncan, Jeandel, Perdrix,
Staton, Vilmart.}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% WP admin and comms
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{WP}{Administation and Communications}{M1}{M36}{wp:admin}
  \WPleaderGREN
  \WPeffort{3}{3}{2}{1}{2}{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 1; involved 2,3,4,5)}{Global administration and
      project coordination.}
    \WPtask[\label{task:website}]{Creation and maintenance of project
      website (M1--M36; responsible 1; involved 2,3,4,5)}{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 2; involved 1)}{Project workshop to define
      state of the art, establish plans for the next year.}
    \WPtask[\label{task:wkshoptwo}]{Midpoint meeting (M17--M18;
      responsible 5; involved 1)}{Project workshop to disseminate
      initial results, evaluate progress and determine next steps.}
    \WPtask[\label{task:wkshopthree}]{Final meeting and school (M33--M36;
      responsible 3; involved 1,5)}{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}

\begin{center}
  \begin{tabular}{|p{0.2\textwidth}|c|c|c|c|c|c|}
    \hline
    \textbf{Partner} 
    &amp; \ref{wp:frontend} 
    &amp; \ref{wp:backends} 
    &amp; \ref{wp:theory}
    &amp; \ref{wp:usefulstuff} 
    &amp; \ref{wp:admin} 
    &amp; \textbf{TOTAL} \\\hline
1. Grenoble &amp;  0 &amp; 11 &amp; 19 &amp; 15 &amp; 3  &amp; 48 \\\hline
2. LORIA      &amp;  7 &amp; 27 &amp; 28 &amp; 22 &amp; 3  &amp; 87 \\\hline
3. Oxford       &amp; 32 &amp; 12 &amp; 20 &amp; 18 &amp; 2  &amp; 84 \\\hline
4. CQC        &amp;  5 &amp; 18 &amp;  0 &amp;  5 &amp; 1  &amp; 29 \\\hline
5. Gdansk    &amp;  3 &amp; 12 &amp; 13 &amp; 21 &amp; 2  &amp; 51 \\\hline
6. Nijmegen    &amp;  3 &amp; 12 &amp; 13 &amp; 21 &amp; 2  &amp; 51 \\\hline
\textbf{TOTAL} &amp; 47 &amp; 83 &amp; 83 &amp; 75 &amp; 11 &amp; 299   \\\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 R. Duncan at the Strathclyde 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: 
C. Allouche (Bull), B. Coecke (Oxford), R. Duncan (Strathclyde),
E. Jeandel (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}}: B. Valiron (LORIA), 
\textbf{\ref{wp:backends}}: S. Abramsky (Oxford),
\textbf{\ref{wp:theory}}: B. Coecke (Oxford),
\textbf{\ref{wp:usefulstuff}}: A. Kissinger (Nijmegen),
\textbf{\ref{wp:admin}}: R. Duncan (Strathclyde).

\paragraph{Software Integration}
\label{sec:software-integration}

Responsibility for the overall software architecture and integration
of components will be shared between C.~Allouche (Bull), A.~Kissinger
(Nijmegen),  and
B.~Valiron (LRI), who make the technical decisions regarding
interfacing of modules and global design.

\paragraph{Monitoring and 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, we have recruited a
board of external advisors who are both experts and potential
end-users of the project.  The advisory board consists of:  
Leonardo DiCarlo (QuTech\,/\,Delft University of Technology), 
Jonathan Pritchard (University of Strathclyde),
Peter Selinger (Dalhousie University), 
Andreas Wallraff (ETH Z\"urich), 
Philip Walther (University of Vienna), and 
Will Zeng (Rigetti Computing). 
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.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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|}
    \textbf{Milestone} &amp;
    \textbf{Delivery Month} &amp;
    \textbf{WP involved} &amp;
    \textbf{Title} \\\hline
%
\ms \label{ms:qasmqasm}&amp;
9 &amp;
\ref{wp:frontend},\ref{wp:backends},  &amp;
Minimal QASM$\rightarrow$QASM circuit optimiser\\\hline
%
\ms \label{ms:quippermbqc}&amp;
18&amp;
All&amp;
Quipper$\to$MBQC compilation pipeline\\\hline
%
\ms \label{ms:simbackend}&amp;
24&amp;
All&amp;
Simulator back-end with parametric \azx support\\\hline
%
\ms \label{ms:delftbackend}&amp;
30&amp;
All&amp;
 Integrate Delft back-end\\\hline
%
\ms \label{ms:nqitbackend}&amp;
36&amp;
All&amp;
Integrate NQIT back end\\\hline
  \end{tabular}}
\end{center}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\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 may (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.
\ref{wp:backends} 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.



\begin{center}
  \begin{tabular}{|p{0.25\textwidth}|c|c|p{0.4\textwidth}|}
    \textbf{Description of risk} 
    &amp; \textbf{Likelihood}
    &amp; \textbf{WPs involved}
    &amp; \textbf{Proposed mitigation measures}\\\hline
%    
Can't hire suitable post-docs&amp;
Low&amp;
All&amp;
We have already identified several suitable candidates for each role.
\\\hline
%    
NQIT or Delft machine info unavailable or not detailed enough&amp;
Low&amp;
\ref{wp:backends}&amp;
(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&amp;
High&amp;
All&amp;
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&amp;
Medium&amp;
All&amp;
(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 developers in the  consortium (Allouche,
Kissinger, Valiron) to act as ``integration triumvirate'' 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.  
%}

The members  of the consortium are chosen to provide the best
combination of skills to deliver this project, having been the pioneers of the fields that provide the foundations for this project, namely the invention of  \zxcalculus\ and its further development, and also having developed applications of \zxcalculus to quantum technologies.  Many members also have a long history of collaboration.   They also contributed greatly to community building.  Several members are part of are part of the NQIT Quantum Technologies Hub.\footnote{nqit.ox.ac.uk} We now provide details on each of these.

Expertise on the
theoretical aspects underpinning the project is provided by the project leader Duncan and
Oxford site leader Coecke who jointly invented the \zxcalculus\  \cite{Coecke:2009aa}. Kissinger,
Perdrix,  Horsman and De Beaudrap and many of their students are experts in its further development  and
use, for example in translation between different computational models \cite{Duncan:2010aa, Horsman:2011lr}, error-correction \cite{Chancellor2016Coherent-Parity} and lattice surgery \cite{BH-2017}.   Abramsky and Coecke are pioneers of high-level methods for
quantum computing more generally. Duncan, Kissinger and Vicary have pioneered automation of diagrammatic reasoning ({\tt quantomatic} and {\tt Globular} respectively), which also will play a key role in this project.  

We  include pioneers in quantum
programming languages (Valiron) and important contributors to the
theory of MBQC (Perdrix, de Beaudrap, Benjamin, and Duncan) and
quantum circuits (Jeandel).  The consortium includes experts in
classical simulation (Allouche), quantum error correction (Horsman, Benjamin), and in quantum architecture (Benjamin,
de Beaudrap), whose expertise is bolstered by the members of our
world-leading advisory board.  

We include experienced co-ordinators of
large multi-site projects (Abramsky, Benjamin, Coecke, Jacobs), and in particular, Benjamin and Coecke have led large-scale project in quantum computing.

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 (Benjamin, 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.

\REM{From cyril to address industrial/commericial}
Bull brings expertise in high performance simulation as well as
industrial guidances in software. \REM{more}

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}

\newpage

\subsection{Description of the consortium \REM{(1 page each)}}
\label{sec:descr-cons}

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


%%%% Strathclyde
\fbox{
  \begin{minipage}{1.0\linewidth}
    \begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
      \textbf{Partner 1} &amp; University of Strathclyde\\
      Project Coordinator &amp; Department of Computer and Information
      Sciences
    \end{tabular}
    \vspace{1mm}\hrulefill\vspace{1mm}

    \textbf{Expertise:} Strathclyde University is one of the UK's
    leading technological universities, and is a member of all four of
    the UK's Quantum Technology hubs, collecting world leading
    expertise in all areas of quantum information.  In the Computer
    and Information Science department, the Mathematically Structured
    Programming group contains internationally recognised leaders in
    the areas of programming language design and implementation (Conor
    McBride, Robert Atkey) and in categorical semantics (Neil Ghani,
    Clemens Kupke).  In the Physics department, which was ranked No.~1
    in the UK in REF 2014, the Optics Division contains numerous
    leading academics and researchers across all areas of theoretical
    and experimental quantum technology, including Andrew Daley, John
    Jeffers, Stefan Kuhr, Daniel Oi, Marco Piani, Jonathan Pritchard,
    and Luca Tagliacozzo.  This unique range of expertise across all
    areas of project the makes Strathclyde an ideal site to host an
    interdisciplinary project like \azx.

    \textbf{\dr Ross Duncan} is Lecturer in Computer and Information
    Sciences, having previously held personal research awards as
    Charg\'e de Recherche (Universit\'e Libre de Bruxelles) and
    \textsc{epsrc} Postdoctoral Fellow (University of Oxford).  He is
    the co-inventor of the \zxcalculus (with B. Coecke)
    (1), and made key contributions to its theory
    (2,3) and its
    application to quantum computation
    (4).  He initiated the %Duncan:2012uq
    \texttt{Quantomatic}
    project\footnote{\url{http://quantomatic.github.io}} and pioneered
    its use for the formal verification of quantum error correcting
    codes (5). He has % Duncan:2013lr,
    organised many major events, most recently \emph{Quantum Physics
      and Logic 2016}, and is co-organiser of the workshop series
    \emph{Quantum Information Scotland}, and \emph{Categories Logic
      and Physics}.
\textit{\color{gray} \textbf{Publications:} (1) B. Coecke and ---. Interacting quantum observables: Categorical algebra and
diagrammatics. New J. Phys, 13(043016), 2011. (2) --- and K. Dunne. Interacting Frobenius algebras are Hopf. In LiCS 2016, ACM Transactions, 2016. (3) Bob Coecke, ---, Aleks Kissinger, and Quanlong Wang. Strong complementarity
and non-locality in categorical quantum mechanics. LiCS 2012. IEEE Computer Society Press, 2012. (4) --- and Simon Perdrix. Rewriting measurement-based quantum computations with generalised flow. In ICALP 2010, Springer LNCS 6199. (5) Liam Garvie and ---. Verifying the smallest interesting colour code with quantomatic. In Proceedings of QPL 2017, to appear.}

    \vspace{1mm}\hrulefill\vspace{1mm}

    \textbf{Role in Project:}

    As the coordinating site, Strathclyde will handle the overall
    management of the project.  With expertise in the \zxcalculus, and
    graphical rewriting generally, Duncan 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
    Strathclyde will focus on \ref{wp:theory} (15 months), 
    \ref{wp:usefulstuff} (12 months) and \ref{wp:backends} (9 months).
  \end{minipage}
}

\newpage
%%%% Oxford
\fbox{
  \begin{minipage}{1.0\linewidth}
    \begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
      \textbf{Partner 2} &amp; University of Oxford\\
       &amp; Department of Computer Science
    \end{tabular}
    \vspace{1mm}\hrulefill\vspace{1mm}

    \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 where 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. The Computer Science Department at Oxford is currently ranked within the world top 3.  
        
%    \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} pioneered categorical and diagrammatic methods for quantum computing (1), and \zxcalculus\  in particular (with Duncan) (2). He is/has supervised approx.~40 PhD students, which include Ng and Wang  who recently proved universal completeness of the \zx-calculus \cite{NW-2017}, and included Backens who proved stabiliser completeness \cite{1367-2630-16-9-093021}. He co-authored \em Picturing Quantum Processes \em (3), which presents diagrammatic methods for quantum computing to a broader audience.
    \textit{\color{gray} \textbf{Publications:} (1) Samson Abramsky and ---. A categorical semantics of quantum protocols. In LICS 2004. IEEE Computer Society, 2004. (2) Bob Coecke and Ross Duncan. Interacting quantum observables: Categorical algebra and
diagrammatics. New J. Phys, 13(043016), 2011. (3) --- and A. Kissinger. Picturing Quantum Processes: A First Course in Quantum Theory and Diagrammatic Reasoning. Cambridge University Press, 2017.}
          
    \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}).

    \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.} \textbf{Dr.\ Niel de Beaudrap} is a post-doctoral researcher involved in the NQIT project. He developed the first efficient algorithms to recover annotation systems to re-write MBQC procedures to the unitary circuit model. \textit{\color{gray} \textbf{Publications:} (1)~---\,. Finding flows in the one-way measurement model. Phys.\,Rev.\,A~77 (022328), 2008.}
% (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.      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 equally between
      \ref{wp:backends}, \ref{wp:theory}, and \ref{wp:usefulstuff},
      including spending 10--20\% of their time working closely with
      the NQIT project.
  \end{minipage}
}


\newpage
%%%% LORIA + LRI
\fbox{
  \begin{minipage}{1.0\linewidth}
    \begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
      \textbf{Partner 3} &amp; Universit\'e de Lorraine / CNRS / INRIA\\ 
       &amp; LORIA (UMR 7503) \\
       &amp; LRI (UMR 8623) ({\small Universit\'e Paris-Sud / CNRS })
    \end{tabular}
    \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 Carte, 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{Emmanuel Jeandel} is Professor at Universit\'e de
    Lorraine, leader of the Inria project team Carte. 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. arXiv:1705.11151, 2017.}

    %\medskip
    
    \textbf{Simon Perdrix} is researcher at CNRS (CR1), 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{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{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 16:60, 2017
    (3) ---, N. J. Ross, P. Selinger, D. S. Alexander and Jonathan M. Smith. Programming the Quantum Future. Communications of the ACM, Vol. 58 No. 8, 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.


    
    
    \vspace{1mm}\hrulefill\vspace{1mm}

    \textbf{Role in Project:} LORIA will develop the front-end compilation of HLLs into \azx 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 \azx taking into account the different models of computation.
    The site provies 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
%%%% Bull
\fbox{
  \begin{minipage}{1.0\linewidth}
    \begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
      \textbf{Partner 4} &amp; Bull\\
       &amp; ATOS Quantum Lab
    \end{tabular}
    \vspace{1mm}\hrulefill\vspace{1mm}

    \textbf{Expertise:}
    Bull SAS, part of ATOS group, is the European industrial leader in
    HPC and Big Data. It has extensive expertise of machine learning,
    in particular in the context of high performance computing. It has
    also a strong expertise in Quantum Computing, with a dedicated
    team of 10 FTE, with activities relevant to the project : quantum
    software,  optimization of quantum circuits, high performance
    simulation of quantum algorithms, theoretical physics. 

    \textbf{Cyril Allouche, PhD}, is the director of Quantum Computing R\&amp;D of
    Atos. An industrial member of the High Level Steering Committee of
    the Quantum Flagship, he had strongly contributed to the
    definition of Pillar 3, "compute". Relevant product is the "Atos
    Quantum Learning Machine", first commercial product dedicated to
    quantum programming and high performance simulation of quantum
    algorithms

    \vspace{1mm}\hrulefill\vspace{1mm}

    \textbf{Role in Project:}

    With their expertise in high-performance computing Bull, will
    focus on the HPC simulation of \azx terms
    (~\ref{task:HPC-sim-model}) however they will also contribute to
    the front end (\ref{wp:frontend}) and compilation techniques
    (\ref{wp:usefulstuff}).  With expertise in building large scale
    software Bull will also contribute the definition of the APIs that
    the \azx toolchain will use.
  \end{minipage}
}

\newpage
%%% Radboud Nijmegen
\fbox{
  \begin{minipage}{1.0\linewidth}
    \begin{tabular}{p{0.4\linewidth}|p{0.6\linewidth}}
      \textbf{Partner 5} &amp; Radboud Universiteit Nijmegen\\
       &amp; Institute for Computing and Information Sciences
    \end{tabular}
    \vspace{1mm}\hrulefill\vspace{1mm}

    \textbf{Expertise:} Situated within the largest digital security group in the Netherlands (51 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 six 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). Since 2006, he has also lead development on the Quantomatic tool~(4), which serves 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{Prof Bart Jacobs} is a Professor of Software Security and Correctness at Radboud, the holder of an ERC Advanced Grant in Quantum Computation, Logic, and Security, and 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 coordinate all aspects of the project
    dealing with automation and tool development, focussed primarily in WP4. It will furthermore contribute strongly to WPs 2 and 3, and in the case of WP2, 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.  All articles will be published in Open
Access venues.

We aim at making our software available to the widest community so, 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}

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.  Benjamin is the leader of the NQIT
  ``Architectures'' work-package, and is an Associate Director of the
  NQIT project as a whole.  Abramsky and de~Beaudrap work on the
  ``Quantum/classical interface and emulation'' workpackage of NQIT,
  and are responsible for guiding the development of a compiler for
  the NQIT architecture.  This gives the \azx\ project unique access
  to the expertise and information regarding the NQIT, and will help
  to ensure that the activities of the \azx 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 \textbf{Oxford}: we have a connection with the \pounds2M Quantum
  Causal Structures JTF grant (with Coecke as PI), which includes the
  study of causal aspect of quantum computing.
\item \textbf{Oxford}: ongoing work on quantum and
  probabilistic programming languages, funded through a Royal Society
  University Research Fellowship (Principled Foundations of
  Programming Languages, Staton), an EPSRC Project (EP/N007387/1:
  Quantum Computation as a Programming Language, Staton) and a grant
  from the Korean Government (Staton). That ongoing work is currently
  on the theoretical side of quantum programming languages and their
  semantics, and this proposal adds a new direction because it bridges
  the gap towards practice.
\item \textbf{Strathclyde:} the Carnegie Trust awarded a PhD
  Scholarship to Mr Joseph Collins for the project ``Infinite
  Dimensional Categorical Quantum Mechanics''.  This contributes to
  the later parts of \ref{task:axioms}.
\item \textbf{Radboud}: 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
\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 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 Bull, our
industrial partner, several engineers will contribute to the project.

\begin{itemize}
\item \emph{Post-doctoral researchers}: We request 36 months of salary
  for post-docs at Strathclyde, Oxford, LORIA, and Nijmegen.  They
  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 four academic 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, Renaud Vilmart will contribute
  approx 9 months to the project; this is funded from other sources.
\item \emph{Engineers}: At Bull, we request 29 person-months for
  research engineers, familiar with Bull's HPC systems, and
  experienced in making commercial software products.  They will be
  essential in achieving our planned impacts.
\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 Nancy respectively.  Our entire advisory board
will be invited to these workshops, which increases the cost beyond
the usual expenses of venue hire and speakers' expenses.  We have
budgeted \euro 6.5k for the first one\footnote{Included in the
  Oxford site's consuambles budget.} (which is planned to be smaller) and
\euro 12k for the second and third.

\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 25\% of the cost of new server blades to upgrade our
  dedicated HPC facility.  This facility will be available to the
  entire project via VPN, and will be used across several tasks, most
  crucially for \ref{task:HPC-sim-model}.
\item We also request laptop computers for each of the postdocs, and
  replacement laptops for some staff at LORIA.  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}

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

\newpage
\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}
</pre></body></html>