From eda67c5a0c2aa0400b9cf5e5127b7d63d65720fc Mon Sep 17 00:00:00 2001
From: Ross Duncan <ross.duncan@strath.ac.uk>
Date: Fri, 15 Feb 2019 13:12:56 +0000
Subject: [PATCH] added sentence about tket

---
 NEWPROPOSAL/FULLPROP.tex | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/NEWPROPOSAL/FULLPROP.tex b/NEWPROPOSAL/FULLPROP.tex
index 9b419f9..10b491f 100644
--- a/NEWPROPOSAL/FULLPROP.tex
+++ b/NEWPROPOSAL/FULLPROP.tex
@@ -254,7 +254,19 @@ An example of such a transformation is the following:}
     %\cnotv[0.6] \rTo^* 
     \cnotvi[0.7]
   \]~\\[-4mm]%
-Members of our consortium have demonstrated how to use these formal reasoning techniques in software, including the interactive theorem prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which was used to formally verify quantum communication protocols and error correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr}) and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early demonstration of the capacity of the \zxcalculus to \newt{outperform other methods of circuit optimisation,  in the sense that certain circuit metric (such as total size, tree-width, or number of non-Clifford subterms such as T-gates) can be minimised.}
+Members of our consortium have demonstrated how to use these formal
+reasoning techniques in software, including the interactive theorem
+prover {\tt quantomatic} \cite{Kissinger2015Quantomatic:-A-} (which
+was used to formally verify quantum communication protocols and error
+correcting codes \cite{Chancellor2016Coherent-Parity,Duncan:2013lr})
+and {\tt PyZX}~\cite{DKPdW-2019}, which provides an early
+demonstration of the capacity of the \zxcalculus to \newt{outperform
+  other methods of circuit optimisation,  in the sense that certain
+  circuit metric (such as total size, tree-width, or number of
+  non-Clifford subterms such as T-gates) can be minimised.}  Our
+industry partner CQC develops \tket, a retargetable quantum compiler
+which, using \zx-based optimisations, outperforms all existing
+compilers for quantum software.
 \TODO{citations if there is space, otherwise maybe kill the second half of this sentence.}
 %%% cutting because repeated later
 % It is strictly more powerful than the stabiliser
-- 
GitLab