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