diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 7c627a8392dcd501cf92bac04df5d58855cc60bd..8d12b5c9731f849860e72830e5e374efee5a404c 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -712,18 +712,6 @@ First, we will identify re-writing processes among the automated theorem proving
This will allow us to identify candidate subroutines that require nonclassical resources to be carried out.
Such subroutines then will be used to develop procedures for characterising if a \zx-represented algorithm demonstrates speed-up.
-\KILL{\begin{color}{red!70!black}
-\texttt{[Delete the following once it has been properly incorporated into the WP description in \S3.2]}
-
-Deliverables:
-\begin{itemize}
- \item M12: Preliminary assessment of the comparative study of the axiomatizations of paradigms of quantum computation.
- \item M15: \zx representation and explanation of the result that promotes magic states as a resource of quantum computation in the state injection paradigm.
- \item M18: Preliminary assessment of nonclassicality of re-writing processes.
- \item M24: A \zx formulation of contextuality (Kochen--Specker and/or generalised Spekken's type).
-\end{itemize}
-\end{color}}
-
\subsubsection{Machine-independent optimisation}
\label{sec:repr-reas-azx}
@@ -1309,7 +1297,7 @@ Devise test-suite of concrete instances of circuits and
%%%
\begin{WP}{Representation, reasoning, and resources in \zx}{1M}{36M}{wp:backends}
\WPleaderPOL
-\WPeffort{{12}}{{12}}{{14}}{{4}}{{30}}{{6}}
+\WPeffort{{12}}{{12}}{{14}}{{4}}{{42}}{{6}}
\begin{WPaim}
%We build the theoretical foundations for \zx as an intermediate representation. This includes extending the capabilities of \zx to represent mixed states, qudit states, and control flows. We use \zx axiomatisations and automated theorem provers to extract out post-classical computing resources, which will be used both for further optimisation work, and for characterisation of quantum algorithmic speed-up.
We build the theoretical foundations for \zx as an intermediate representation. This includes extending the capabilities of \zx to represent qudit states with a fixed $d$, arbitrary finite-dimensional quantum states, and control flows. We explore the structure of W-type tensors with interaction with \zx generators of GHZ-type. We use \zx axiomatisations and automated theorem provers to extract out post-classical computing resources, which will be used both for further optimisation work, and for characterisation of quantum algorithmic speed-up.
@@ -1445,12 +1433,12 @@ Perdrix, Valiron, Carette.}
%%%
%%%%%%%WP 4
%%%
-\begin{WP}{Machine-dependent optimisation}{1M}{36M}{wp:usefulstuff}
+\begin{WP}{Machine-dependent optimisation}{13M}{36M}{wp:usefulstuff}
\WPleaderGREN
\WPeffort{12}{9}{12}{6}{6}{0}
\begin{WPaim}
We import machine-dependent specifications to \zx terms, and use this to optimise algorithms further for specific hardware constraints. We focus on the silicon spin qubits developing in Grenoble, the ion traps developed in Oxford, and the superconducting devices accessible through CQC and partnership with IBM. This is the culmination of all previous work packages, and feeds back into them. The final result will be \ldots.
-Also machine-dependent error correction here?
+Also machine-dependent error correction?
\end{WPaim}
\begin{WPtasks}
\WPtask[\label{task:qdot-model}]{Grenoble silicon spin qubits (M13--M36 Responsible: \partnerref{partner:grenoble};
@@ -1468,6 +1456,7 @@ Also machine-dependent error correction here?
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: \partnerref{partner:loria}; Involved: \partnerref{partner:grenoble},\partnerref{partner:oxford},\partnerref{partner:gdansk})}{%
Develop algorithms which, given a collection of constraints
@@ -1493,9 +1482,10 @@ Also machine-dependent error correction here?
\WPdeliverable{M30}{General purpose layout engine}
\WPdeliverable{M36}{Optimising \dzxc, suitable for compiling to Grenoble and/or Oxford architecture}
\WPdeliverable[\label{del:backendapi}]{M36}{API for back-end
- modules, including specification language for architectures.}
+ modules, including specification language for architectures.}
\end{WPdeliverables}
\end{WP}
+\TODOb{Should D4.5 be the same as D1.6?}
\REM{\emph{Leader:} Kissinger.
\emph{Others:} Abramsky, de Beaudrap, Duncan, Jeandel, Perdrix,
@@ -1562,13 +1552,13 @@ Staton, Carette.}
& \ref{wp:usefulstuff}
& \ref{wp:admin}
& \textbf{TOTAL} \\\hline
-1. Grenoble & 12 & 12 & 12 & 12 & 3 & 51 \\\hline
+1. Grenoble & 12 & 2 & 12 & 12 & 3 & 41 \\\hline
2. LORIA & 20 & 12 & 9 & 9 & 3 & 53 \\\hline
3. Oxford & 32 & 14 & 30 & 12 & 2 & 90 \\\hline
4. CQC & 12 & 4 & 12 & 6 & 1 & 28 \\\hline
-5. Gdansk & 12& 30 & 12 & 6 & 4 & 71 \\\hline
+5. Gdansk & 12& 42 & 12 & 6 & 4 & 76 \\\hline
6. Nijmegen & 3 & 6 & 12 & 0 & 2 & 23 \\\hline
-\textbf{TOTAL}& 91 & 78 & 87 & 45 & 11 & 317 \\\hline
+\textbf{TOTAL}& 91 & 80 & 87 & 45 & 11 & 317 \\\hline
\end{tabular}
\end{center}}
@@ -1655,19 +1645,24 @@ reduce risk and improve communication across the consortium.
\textbf{Title} \\\hline
%
\ms \label{ms:qasmqasm}&
-9 &
+12 &
+\ref{wp:frontend},\ref{wp:backends}, &
+Deep-\zx based circuit optimiser software that outperforms all other procedures.\\\hline
+%
+\ms \label{ms:qasmqasm}&
+14 &
\ref{wp:frontend},\ref{wp:backends}, &
-Minimal QASM$\rightarrow$QASM circuit optimiser\\\hline
+Compiler module for qudit and mixed state \\\hline
%
\ms \label{ms:quippermbqc}&
18&
All&
-Quipper$\to$MBQC compilation pipeline\\\hline
+\zx $\to$MBQC and circuit compilation pipeline\\\hline
%
\ms \label{ms:simbackend}&
24&
All&
-Simulator back-end with parametric \azx support\\\hline
+ \\\hline
%
\ms \label{ms:delftbackend}&
30&
@@ -1677,7 +1672,7 @@ All&
\ms \label{ms:nqitbackend}&
36&
All&
-Integrate NQIT back end\\\hline
+Complete deep-\zx compiler stack with open APIs. \\\hline
\end{tabular}}
\end{center}