<figure><img src="image_1.png" /></figure>

Latest updates: https://dl.acm.org/doi/10.1145/3756907.3756908

INVITED-TALK

# Counting Qubits and Gates: Resource Analysis in Quantum Programming Languages

<figure><img src="image_2.png" /></figure>

PDF Download
3756907.3756908.pdf
19 December 2025
Total Citations: 0
Total Downloads: 24

Published: 10 September 2025

Citation in BibTeX format

PPDP '25: Proceedings of the 27th
International Symposium on Principles
and Practice of Declarative Programming

September 10 - 11, 2025

Rende, Italy
# Counting Qubits and Gates: Resource Analysis in Quantum Programming Languages

Ugo Dal Lago

Department of Computer Science

University of Bologna

Bologna, Italy

ugo.dallago@unibo.it

## CCS Concepts

* *Theory of computation* → *Program verification; Quantum computation theory; Software and its engineering* → *Context specific languages.*

### ACM Reference Format:

Ugo Dal Lago. 2025. Counting Qubits and Gates: Resource Analysis in Quantum Programming Languages. In *Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming (PPDP '25), September 10–11, 2025, Rende, Italy*. ACM, New York, NY, USA, 3 pages.
https://doi.org/10.1145/3756907.3756908

Quantum computing promises breakthroughs in solving complex problems faster than classical computing, thanks to quantum bits leveraging superposition and entanglement [18, 32]. Various models of quantum computation are being explored, including gate-based systems, quantum annealing [21], and topological quantum computing [22]. But how can such computational power be made available to the programmer in a way that makes the implementation of concrete algorithms and protocols straightforward?

*Quantum Programming.* A widely adopted abstraction is Knill's QRAM model [23], where a classical controller interacts with a quantum storage device, instructing the latter to allocate new qubits, apply unitary operations, and perform measurements. As a consequence, computations can have probabilistic outcomes. Noticeably, quantum operations follow strict quantum mechanical constraints (e.g., no-cloning, no-erasure). This model underpins many quantum programming languages, ranging from low-level [9, 10] to imperative [14] and functional languages [11, 30, 31]. These idioms share a common structure: classical languages are, in some way, augmented with specific instructions that enable interaction with the quantum store (potentially avoiding operations like cloning and erasing), leaving the language core essentially unchanged. However, practical quantum programming often deviates from this model: most current hardware requires quantum circuits to be prepared classically and sent as a *whole* to quantum hardware for execution. Thus, quantum programming is often done via *quantum circuit description languages* such as Qiskit [20], Cirq [33], or Quipper [16, 17], whereas circuits are constructed as data structures, separating circuit *construction* from circuit *execution*.

<figure><img src="image_3.png" /></figure>

This work is licensed under a Creative Commons Attribution 4.0 International License.
PPDP '25, Rende, Italy

© 2025 Copyright held by the owner/author(s).

ACM ISBN 979-8-4007-2085-7/25/09

https://doi.org/10.1145/3756907.3756908

*Dealing with Nosiy Hardware.* It cannot be said that quantum programming follows a single, unified paradigm—though, as in classical computing, certain trends are indeed emerging. Regardless of the approach taken to write quantum programs, there is an additional challenge unique to the quantum domain, which significantly limits its transformative potential. Unlike classical hardware, quantum hardware, both commercially available and experimental, is at the time of writing incapable of reliably executing circuits exceeding minimal width or depth [29]. When these limits are exceeded, errors accumulate to such an extent that they render computation useless. A huge scientific and engineering effort is currently being directed at designing innovative quantum architectures overcoming the aforementioned problem. On the other hand, quantum error correction codes [26] address these problems by creating a sort of middleware layer between the hardware and the applications so as to give the latter the impression of dealing with reliable hardware. In both cases, recent advances has pushed the boundaries [1, 6], offering hope for meaningful breakthroughs.

*Analysing the Complexity of Quantum Programs.* In the meantime, a pressing challenge has emerged: programmers have to be able to work effectively with current quantum architectures, despite their significant limitations. In this context, it is not only crucial to develop suitable programming languages, but also to make it as straightforward as possible for programmers to manage and control hardware resource usage. It is clear that given the high costs of executing programs on quantum hardware architectures, this analysis should be performed *statically*. Furthermore, it should be noted that the problem of estimating the size of a *single* circuit is trivial, while analyzing the size of high-level QRAM programs or circuit family *parametrically* on the (size of the) input represents the real challenge. These needs have spurred research in recent years focused on developing static analysis techniques capable of estimating the resource requirements of quantum programs.

*This Talk.* I will present an overview of the just described research area. I will start with an introduction to quantum computing and quantum programming languages. I will then explore some approaches to the resource analysis of quantum programs—without attempting to provide an exhaustive survey.

## 1 Resource Estimation in Circuit Description Languages

As already mentioned, quantum circuit description languages (QCDLs in the following) are domain-specific programming languages—or libraries for general-purpose idioms—used to build and manipulate quantum circuits. They provide abstractions for qubits, quantum
gates, and operations on them, enabling the implementation of quantum algorithms as quantum circuit families. These languages support both low-level gate definitions and high-level algorithmic constructs, facilitating the development of quantum software at various levels of abstraction.

Quipper is a QCDL hosted in Haskell, in which quantum circuits can be manipulated like any other data structure, but circuit building is also viewed as a form of computational effect. Ultimately, this allows for flexibility, with the ability to seamlessly switch between circuits and functions. Recently, the author, in a joint work with Andrea Colledan, proposed a type-based static analysis technique for Quipper programs allowing the derivation of upper bounds on the size of the circuits produced [7, 8]. Noticeably, the methodology is flexible, in that it is not restricted to a specific circuit metric but can handle any metric satisfying certain mild requirements, including, but not limited to, *circuit width*, *circuit depth*, and *gate count*. The methodology is not only sound from a theoretical point of view but has been implemented in a tool, called QuRA.

## 2 Quantum Expectation Transformers

Expectation analysis methodologies extend predicate transformer semantics [13]—like weakest preconditions—to probabilistic programs by mapping post-expectations, namely real-valued functions representing expected outcomes, back to pre-expectations. This allows reasoning about the *expected value* of program variables rather than the mere *logical truth* of the underlying assertions. These methods have been proved to be effective in the verification of quantitative properties of probabilistic programs, including expected cost, reachability, and resource usage (see, e.g., [4, 28]).

Given that measurement operations can have a probabilistic outcome, quantum programs in the QRAM model behave not too dissimilarly from probabilistic programs, and for many verification problems it can be shown that the intrinsic difficulty, while very high, remains the same [2]. It is thus natural to imagine generalizations of the expectation-based approach to QRAM programs. The challenges, in this context, are those of appropriately formalizing the notion of cost and to adapt classical definitions to the presence of quantum data, which have both been addressed by recent work [3, 27].

## 3 Implicit Computational Complexity

In implicit computational complexity (ICC in the following), one looks for characterizations of computational complexity classes without explicitly referencing resource bounds nor machines models. Instead, ICC relies on logical systems, programming language restrictions, or subrecursive schemes to ensure that programs remain within relatively small complexity classes such as P or PSPACE, at the same time being able to represent all problems in the class [5, 15, 24, 25]. This way, ICC naturally suggests machine-independent, syntax-driven methods for controlling the use of computational resources, often suggesting verification methodologies.

For some time now, attempts have been made to adapt classical ICC techniques so that the captured complexity class is quantum. This is the case with the work by the author with Masini and Zorzi [12] on a λ-calculus designed around the principles of Lafont's

Soft Linear Logic [24] but equipped with specific constructs for accessing quantum registers, in the spirit of the QRAM model. Yamakami, instead, worked on characterizing quantum polynomial time [34] and polylogarithmic time [35], through function algebras in the style of primitive recursive functions. Finally, recent work on a characterization of FBQP by an imperative programming language with quantum control is also noteworthy [19].

## References

[1] 2025. Quantum error correction below the surface code threshold. *Nature* 638, 8052 (2025), 920–926.

[2] Martin Avanzini, Georg Moser, Romain Péchoux, and Simon Perdrix. 2024. On the Hardness of Analyzing Quantum Programs Quantitatively. In *Proc. of ESOP 2024 (Lecture Notes in Computer Science, Vol. 14577)*, Stephanie Weirich (Ed.). Springer, 31–58.

[3] Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, and Vladimir Zamdzhiev. 2022. Quantum Expectation Transformers for Cost Analysis. In *Proc. of LICS 2022*. ACM, 10:1–10:13.

[4] Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Math-eja. 2021. Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning. *Proc. ACM Program. Lang.* 5, POPL (2021), 1–30.

[5] Stephen Bellantoni and Stephen Cook. 1992. A New Recursion-Theoretic Characterization of the Poltime Functions. *Computational Complexity* 2 (1992), 97–110.

[6] Dolev Bluvstein, Simon J Evered, Alexandra A Geim, Sophie H Li, Hengyun Zhou, Tom Manovitz, Sepehr Ebadi, Madelyn Cain, Marcin Kalinowski, Dominik Hangleiter, et al. 2024. Logical quantum processor based on reconfigurable atom arrays. *Nature* 626, 7997 (2024), 58–65.

[7] Andrea Colledan and Ugo Dal Lago. 2024. Circuit Width Estimation via Effect Typing and Linear Dependency. In *Proc. of ESOP 2024 (Lecture Notes in Computer Science, Vol. 14577)*, Stephanie Weirich (Ed.). Springer, 3–30.

[8] Andrea Colledan and Ugo Dal Lago. 2025. Flexible Type-Based Resource Estimation in Quantum Circuit Description Languages. *Proc. ACM Program. Lang.* 9, POPL (2025), 1386–1416.

[9] Andrew Cross, Ali Javadi-Abhari, Thomas Alexander, Niel De Beaudrap, Lev S. Bishop, Steven Heidel, Colm A. Ryan, Prasahnt Sivarajah, John Smolin, Jay M. Gambetta, and Blake R. Johnson. 2022. OpenQASM 3: A Broader and Deeper Quantum Assembly Language. *ACM Transactions on Quantum Computing* 3, 3 (Sept. 2022), 1–50. doi:10.1145/3505636

[10] Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. 2017. Open Quantum Assembly Language. arXiv:1707.03429 [quant-ph] https://arxiv.org/abs/1707.03429

[11] Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. 2009. On a measurement-free quantum lambda calculus with classical control. *Math. Struct. Comput. Sci.* 19, 2 (2009), 297–335. doi:10.1017/S096012950800741X

[12] Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. 2010. Quantum implicit computational complexity. *Theor. Comput. Sci.* 411, 2 (2010), 377–409. doi:10.1016/j.tcs.2009.07.045

[13] Edsger W Dijkstra. 1975. Guarded commands, nondeterminacy and formal derivation of programs. *Commun. ACM* 18, 8 (1975), 453–457.

[14] Yuan Feng and Mingsheng Ying. 2021. Quantum Hoare logic with classical variables. *ACM Transactions on Quantum Computing* 2, 4 (2021), 1–43.

[15] Jean-Yves Girard. 1998. Light Linear Logic. *Information and Computation* 143(2) (1998), 175–204.

[16] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoit Valiron. 2013. *An Introduction to Quantum Programming in Quipper*. Springer Berlin Heidelberg, 110–124. doi:10.1007/978-3-642-38986-3_10

[17] Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoit Valiron. 2013. Quipper: a scalable quantum programming language. *ACM SIGPLAN Notices* 48, 6 (June 2013), 333–342. doi:10.1145/2499370.2462177

[18] Lov K Grover. 1996. A fast quantum mechanical algorithm for database search. In *Proc. of STOC 1996*, 212–219.

[19] Emmanuel Hainry, Romain Péchoux, and Mário Silva. 2023. A Programming Language Characterizing Quantum Polynomial Time. In *Proc. of FoSSaCS 2023 (Lecture Notes in Computer Science, Vol. 13992)*, Orna Kupferman and Pawel Sobocinski (Eds.). Springer, 156–175.

[20] Ali Javadi-Abhari, Matthew Treinish, Kevin Krsulich, Christopher J. Wood, Jake Lishman, Julien Gacon, Simon Martiel, Paul D. Nation, Lev S. Bishop, Andrew W. Cross, Blake R. Johnson, and Jay M. Gambetta. 2024. Quantum computing with Qiskit. doi:10.48550/arXiv.2405.08810 arXiv:2405.08810 [quant-ph]

[21] M. W. Johnson, M. H. S. Amin, S. Gildert, T. Lanting, F. Hamze, N. Dickson, R. Harris, A. J. Berkley, J. Johansson, P. Bunyk, E. M. Chapple, C. Enderud, J. P. Hilton, K. Karimi, E. Ladizinsky, N. Ladizinsky, T. Oh, I. Perminov, C. Rich, M. C. Thom, E. Tolkacheva, C. J. S. Truncik, S. Uchaikin, J. Wang, B. Wilson, and G.
[21] Rose. 2011. Quantum annealing with manufactured spins. *Nature* 473, 7346 (2011), 194–198. doi:10.1038/nature10012

[22] A.Yu. Kitaev. 2003. Fault-tolerant quantum computation by anyons. *Annals of Physics* 303, 1 (2003), 2–30. doi:10.1016/S0003-4916(02)00018-0

[23] E Knill. 1996. Conventions for quantum pseudocode. *Technical report* (6 1996). doi:10.2172/366453

[24] Yves Lafont. 2004. Soft linear logic and polynomial time. *Theor. Comput. Sci.* 318, 1–2 (2004), 163–180.

[25] Daniel Leivant. 1993. Stratified Functional Programs and Computational Complexity. In *Proc. of POPL 1993*. 325–333.

[26] Daniel A Lidar and Todd A Brun. 2013. *Quantum error correction*. Cambridge university press.

[27] Junyi Liu, Li Zhou, Gilles Barthe, and Mingsheng Ying. 2025. Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. *J. ACM* 72, 3 (2025), 20:1–20:51.

[28] Annabelle McIver and Carroll Morgan. 2005. *Abstraction, refinement and proof for probabilistic systems*. Springer.

[29] John Preskill. 2018. Quantum computing in the NISQ era and beyond. *Quantum* 2 (2018), 79.

[30] Peter Selinger and Benoît Valiron. 2006. A lambda calculus for quantum computation with classical control. *Math. Struct. Comput. Sci.* 16, 3 (2006), 527–552.

[31] Peter Selinger and Benoît Valiron. 2008. On a fully abstract model for a quantum linear functional language. *Electronic Notes in Theoretical Computer Science* 210 (2008), 123–137.

[32] Peter W Shor. 1999. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. *SIAM review* 41, 2 (1999), 303–332.

[33] Google AI Quantum Team. 2018. Cirq Programming Language. https://quantumai.google/cirq.

[34] Tomoyuki Yamakami. 2020. A Schematic Definition of quantum Polynomial Time Computability. *J. Symb. Log.* 85, 4 (2020), 1546–1587.

[35] Tomoyuki Yamakami. 2024. Elementary quantum recursion schemes that capture quantum polylogarithmic-time computability of quantum functions. *Math. Struct. Comput. Sci.* 34, 7 (2024), 710–745.