Sized types for low-level quantum metaprogramming. (English) Zbl 07118470

Thomsen, Michael Kirkedal (ed.) et al., Reversible computation. 11th international conference, RC 2019, Lausanne, Switzerland, June 24–25, 2019, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11497, 87-107 (2019).
Summary: One of the most fundamental aspects of quantum circuit design is the concept of families of circuits parametrized by an instance size. As in classical programming, metaprogramming allows the programmer to write entire families of circuits simultaneously, an ability which is of particular importance in the context of quantum computing as algorithms frequently use arithmetic over non-standard word lengths. In this work, we introduce metaQASM, a typed extension of the openQASM language supporting the metaprogramming of circuit families. Our language and type system, built around a lightweight implementation of sized types, supports subtyping over register sizes and is moreover type-safe. In particular, we prove that our system is strongly normalizing, and as such any well-typed metaQASM program can be statically unrolled into a finite circuit.
For the entire collection see [Zbl 1420.68014].


68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
81P68 Quantum computation
Full Text: DOI arXiv


[1] Aharonov, D., Jones, V., Landau, Z.: A polynomial quantum algorithm for approximating the jones polynomial. In: Proceedings of the Thirty-Eighth Annual ACM Symposium on Theory of Computing, STOC, pp. 427-436 (2006). https://doi.org/10.1145/1132516.1132579 · Zbl 1301.68129
[2] Altenkirch, T., Grattage, J.: A functional quantum programming language. In: 20th Annual IEEE Symposium on Logic in Computer Science, LICS, pp. 249-258 (2005). https://doi.org/10.1109/LICS.2005.1
[3] Amy, M.: Feynman. https://github.com/meamy/feynman
[4] Amy, M., Roetteler, M., Svore, K.M.: Verified compilation of space-efficient reversible circuits. In: Proceedings of the 29th International Conference on Computer Aided Verification, CAV, pp. 3-21 (2017). https://doi.org/10.1007/978-3-319-63390-9_1
[5] Bello, L., et al.: Qiskit. https://github.com/Qiskit/qiskit-terra
[6] Cross, A.W., Bishop, L.S., Smolin, J.A., Gambetta, J.M.: Open quantum assembly language. arXiv preprint (2017). http://arxiv.org/abs/1707.03429
[7] Fu, P.: Private communication (2018)
[8] Gay, S.J.: Quantum programming languages: survey and bibliography. Math. Struct. Comput. Sci. 16(4), 581-600 (2006). https://doi.org/10.1017/S0960129506005378 · Zbl 1122.68021
[9] Gheorghiu, V.: Quantum++: a modern C++ quantum computing library. PLoS ONE 13(12), 1-27 (2018). https://doi.org/10.1371/journal.pone.0208073
[10] Green, A.S., Lumsdaine, P.L.F., Ross, N.J., Selinger, P., Valiron, B.: An introduction to quantum programming in Quipper. In: Dueck, G.W., Miller, D.M. (eds.) RC 2013. LNCS, vol. 7948, pp. 110-124. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38986-3_10 · Zbl 1406.68013
[11] Green, A.S., Lumsdaine, P.L., Ross, N.J., Selinger, P., Valiron, B.: Quipper: a scalable quantum programming language. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, pp. 333-342 (2013). https://doi.org/10.1145/2491956.2462177 · Zbl 1406.68013
[12] Grover, L.K.: A fast quantum mechanical algorithm for database search. In: Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, STOC, pp. 212-219 (1996). https://doi.org/10.1145/237814.237866 · Zbl 0922.68044
[13] Häner, T., Steiger, D.S.: 0.5 petabyte simulation of a 45-qubit quantum circuit. In: Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC, pp. 33:1-33:10 (2017). https://doi.org/10.1145/3126908.3126947
[14] Häner, T., Steiger, D.S., Svore, K., Troyer, M.: A software methodology for compiling quantum programs. Quantum Sci. Technol. 3(2), 020501 (2018). https://doi.org/10.1088/2058-9565/aaa5cc
[15] Heyfron, L.E., Campbell, E.T.: An efficient quantum compiler that reduces T count. Quantum Sci. Technol. 4(1), 015004 (2018). https://doi.org/10.1088/2058-9565/aad604
[16] JavadiAbhari, A., et al.: ScaffCC: scalable compilation and analysis of quantum programs. Parallel Comput. 45(C), 2-17 (2015). https://doi.org/10.1016/j.parco.2014.12.001
[17] Khammassi, N., Ashraf, I., Fu, X., Almudever, C.G., Bertels, K.: QX: a high-performance quantum computer simulation platform. In: Proceedings of the 20th Design, Automation Test in Europe Conference Exhibition, DATE, pp. 464-469 (2017). https://doi.org/10.23919/DATE.2017.7927034
[18] Khammassi, N., Guerreschi, G., Ashraf, I., Hogaboam, J.W., Almudever, C.G., Bertels, K.: cQASM v1.0: towards a common quantum assembly language. arXiv preprint (2018). http://arxiv.org/abs/1805.09607
[19] Killoran, N., Izaac, J., Quesada, N., Bergholm, V., Amy, M., Weedbrook, C.: Strawberry fields: a software platform for photonic quantum computing. Quantum 3, 129 (2019). https://doi.org/10.22331/q-2019-03-11-129
[20] Kissinger, A., van de Wetering, J.: PyZX: large scale automated diagrammatic reasoning. arXiv preprint (2019). http://arxiv.org/abs/1904.04735
[21] Kliuchnikov, V., Maslov, D., Mosca, M.: Fast and efficient exact synthesis of single-qubit unitaries generated by clifford and T gates. Quantum Inf. Comput. 13(7-8), 607-630 (2013). https://doi.org/10.26421/QIC13.7-8
[22] Liu, S., et al.: \(Q|SI\rangle \): a quantum programming environment. arXiv preprint (2017). http://arxiv.org/abs/1710.09500
[23] Lloyd, S.: Universal quantum simulators. Science 273(5278), 1073-1078 (1996). https://doi.org/10.1126/science.273.5278.1073 · Zbl 1226.81059
[24] Martonosi, M., Roetteler, M.: Next steps in quantum computing: computer science’s role. Computing Community Consortium (CCC) workshop report (2019). http://arxiv.org/abs/1903.10541
[25] Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge Series on Information and the Natural Sciences. Cambridge University Press, Cambridge (2000) · Zbl 1049.81015
[26] Ömer, B.: Quantum programming in QCL. Master’s thesis, Technical University of Vienna (2000). http://tph.tuwien.ac.at/ oemer/qcl.html
[27] Paykin, J., Rand, R., Zdancewic, S.: QWIRE: a core language for quantum circuits. In: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL, pp. 846-858 (2017). https://doi.org/10.1145/3009837.3009894 · Zbl 1380.68087
[28] Preskill, J.: Quantum computing in the NISQ era and beyond. Quantum 2, 79 (2018). https://doi.org/10.22331/q-2018-08-06-79
[29] Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings of the 35th Annual Symposium on Foundations of Computer Science, SFCS, pp. 124-134 (1994). https://doi.org/10.1109/SFCS.1994.365700
[30] Smith, R.S., Curtis, M.J., Zeng, W.J.: A practical quantum instruction set architecture. arXiv preprint (2016). http://arxiv.org/abs/1608.03355
[31] Soeken, M.: RevKit. https://msoeken.github.io/revkit.html
[32] Steiger, D.S., Häner, T., Troyer, M.: ProjectQ: an open source software framework for quantum computing. Quantum 2, 49 (2018). https://doi.org/10.22331/q-2018-01-31-49
[33] Svore, K., et al.: \(Q\#\): enabling scalable quantum computing and development with a high-level DSL. In: Proceedings of the 3rd ACM International Workshop on Real World Domain Specific Languages, RWDSL, pp. 7:1-7:10 (2018). https://doi.org/10.1145/3183895.3183901
[34] Xi, H.: Dependent types for program termination verification. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, LICS, pp. 231-242 (2001). https://doi.org/10.1109/LICS.2001.932500
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.