High-level quantum structured programs as quantum registers compositions

arXiv:2608.03873v1 [quant-ph] 4 Aug 2026

High-level quantum structured programs as quantum registers compositions David Chamizo

Jose Garcia-Alonso

Juan M. Murillo

Quercus Software Engineering Group University of Extremadura Cáceres, Spain davidchs@unex.es

Quercus Software Engineering Group University of Extremadura Cáceres, Spain jgaralo@unex.es

Quercus Software Engineering Group University of Extremadura Cáceres, Spain juanmamu@unex.es

As stated by Zhao [13], quantum programming can be understood as “the process of designing and building executable quantum computer programs to achieve a particular computing result”. At present, building a quantum program is mostly restricted to programming languages that are devised for implementing quantum gates on individual qubits [14]–[20]. As a result, quantum program design is realized at a low level, comparable to classical assembler languages [21], making an intricate computation a complex task and error-prone. In view of this, quantum programs ought to be adjusted to an abstraction level adapted to the dimension of the problems being addressed. This would not only benefit simplification but also verifiability, modularity, scalability and expressive capacity of quantum programs [22]. At the same time, an appropriate abstraction level may prove advantageous in the design and implementation of novel quantum algorithms. Nevertheless, raising the level of abstraction in quantum programming should not aim at merely emulating the abstraction from classical programming, but rather at extending the principles of high-level structured programming into the quantum domain [10], [23], making for a quantum-oriented paradigm [24]. In an effort towards increasing the abstraction level of quantum programming, this work introduces a conceptual I. I NTRODUCTION framework that considers a quantum computation as a structure Quantum computing was conceived through the integration that evolves throughout the computation. To clarify, evolving of quantum mechanics into computational models [1], [2] means modifying the global quantum state by altering, inaiming to create quantum computer programs that enable a dividually or via composition, the distinct components that more efficient computation than any previously known classical conform the structure. This structure is to be composed of one computation [3]–[5]. Currently, research is mainly focused or several quantum registers, understood as ordered sets of on enabling its hardware [6], [7], designing novel quantum qubits. Each register models what we denote as a computational algorithms and error-correcting codes [8], [9], and establish- construct, that is, an entity modeled (e.g., energy levels of a ing the foundations of quantum software engineering [10]. molecule or air flows in a weather model) within available However, while quantum hardware continues to progress at a computation resources. Then, operations are no longer thought remarkable pace [11], [12], quantum software, and specifically at the level of quantum gates acting on individual qubits, but at quantum programming, is not advancing commensurately. As that of quantum register as undivided entities. To illustrate a consequence, the advent of practical quantum computing is this approach, several high-level syntax are formalized as hindered. transformations for composing registers following schemes This works has been partially funded by the EU (Next GenerationEU/PRTR), from previously well-known operations. This formalization is by the Spanish MICIU (PDC2025-165096-C31). It is also supported by project enabled through the definition of an algebraic formalism for ATHENA (PID2024-155693NB-C41, MICIU/AEI/10.13039/501100011033); quantum programming, proposed by Ying et al. [25]. In parand 85% co-funded by the EU, ERDF and the Regional Government of Extremadura. Managing Authority: Spanish Ministry of Finance, Aid GR24099 ticular, a quantum satisfiability modulo theories (SMT) solver and Project IB24190 is formulated relying solely on them: once the transformation

Abstract—Current quantum programs are mainly designed at the level of quantum gates acting on individual qubits; on a large scale and for complex problems this may involve a high cognitive load on the programmer, making the program specification nontrivial and error-prone. In this context, providing quantum programming with higher abstraction mechanisms will assist in making this task more manageable and robust against design errors. In this work, a conceptual framework is addressed following the notion of the whole quantum computation as a structure composed of quantum registers representing each an undivided entity. Thus, computation progresses through semantically well-defined transformations that act on, or entangle, quantum registers, thereby modifying the global state. Ultimately, the program reaches the desired state by following a specific composition strategy. With this in mind, high-level syntax is presented through an algebraic formalism that bridges them with their low-level semantics. Proposed syntax is based on certain well-know operations used on quantum algorithms that apply phase shifts upon logical condition satisfaction or leverage on parallel evaluation. Based solely on the formalized operations, a quantum satisfiability modulo theories (SMT) solver can be designed. At its core, this work contributes to establishing some methodological principles towards realizing a high-level quantum structured programming. Index Terms—Quantum Programming, Quantum Structured Programming, Abstraction, Quantum Software Engineering

©2026 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.

are defined, a quantum program can be designed without however, there is not a suitable framework that properly uses referring to quantum gates. In essence, the proposed approach these to develop a structured programming paradigm taking strives to bring to quantum programming some methodological advantage of the quantum nature of operations. principles of high-level structured decomposition, composition, As such, quantum programs are mainly designed at the and refinement. level of quantum gates sequences to adapt to these languages. Whereas many quantum algorithms are based on evolutions The main contributions of this work are: that can be, to some extent, directly mapped into quantum • Introduction of a conceptual framework that serves as the basis for thinking about quantum computation processes gates sequences [8], [37], this translation is not always at a higher-level than that of individual qubits evolution. straightforward, especially when the scheme is out of the scope of a complete algorithm (e.g., when the goal is to use • Formalization of well-known operations for the conceptual framework using high-level syntax and an algebraic algorithm parts rather than an entire routine). Even though it formalism that bridges them to their low-level semantics. is possible to assemble operations into custom (higher-level) gates acting on sets of qubits following the intended scheme, • The design of a quantum SMT solver program based on the transformations formalized, illustrating their potential they need to be manually specified gate by gate. This process requires programmers to understand the operations behavior capability of advancing quantum program design. and design the program as a sequence of quantum gates The rest of the work is organized as follows. In Section II acting on individual qubits. Given this, specification becomes an overview for the current state of abstraction on quantum nontrivial and error-prone when problems turn increasingly programming is presented. Before outlining the specifics of more complex and grow in scale. At the same time, given such this proposal, Section III provides an explanation about the limitation, expressive capacity and creation of novel algorithms algebraic formalism used and its associated laws. Section IV is hindered. describes in detail the conceptual framework and formalizes the Under the premise that classical programming historical semantics of high-level syntax. Program design for a quantum development achieved success through abstraction increase [38], SMT solver as an application using the previously defined seems reasonable to expect that quantum programming can syntax is shown in Section V. In Section VI, a brief discussion benefit from it as well [39]. Particularly, given the complexity is offered. Lastly, Section VII recapitulates on the work and and counter-intuitive nature of quantum mechanics, abstraction several conclusions are drawn. promises to hasten the adoption process of this technology [40]. Classical programming ceased to be implemented in binary II. A BSTRACTION ON Q UANTUM P ROGRAMMING terms and evolved towards high-level languages based on In general terms, abstraction can be defined as a mechanism abstract data types [26]. Currently, classical programmers that allows the expression of relevant details, leaving irrelevant can model real elements into abstractions inside a program ones hidden [26]. Formally, it is a homomorphic mapping that and specify their interactions (e.g., object-oriented programallows the functioning of a structure to be preserved while ming [41]), completely disengaging algorithmic logic from ignoring its lower-level implementation. Fewer details mean physical implementation. Meanwhile, quantum programming that the barrier to understanding how the process works is lacks a a proper model where quantum information can be lowered. For computational processes, this also may translate used for designing programs in a similar way. Although some into better verifiability, modularity, and scalability [27], [28]. higher abstractions have been formalized in a quantum setting, Current quantum programming is located at an abstraction such as quantum modular arithmetic [42], [43] and circuit level similar to that of assembler languages [21] in classical synthesis [44], [45], a more versatile framework that treats programming. This foundation has been mainly procured quantum information as constructs that establish relations is by leveraging on binary terms1 through the quantum circuit yet to be introduced. Additionally, such abstraction must be paradigm [29], [30] integrated in classical programming aligned with the internal workings of a quantum computer as languages [31]. This advancement enables programmers to to not unintentionally violate its basic principles, leading to operate quantum computers using quantum gates, which inappropriate or not feasible computations [46]. resemble logical gates from classical computing, instead of Hence, this work aims towards establishing a quantumdescending to the level of physical implementation (e.g., pulse oriented structured programming paradigm. This is achieved modulation [32]). This is the paradigm most current quantum by regarding quantum computations as structures that can programming languages work at [14], such as Scaffold [15], be modified via composition and refinement of quantum Quipper [16], Q# [17], Pennylane [18], Qiskit [19], or Cirq [20] registers. However, it is important to note that the underlying among others. Notwithstanding, it is worth mentioning high- implementation of such quantum programming paradigm may level quantum programming languages, namely Silq [33], result in a more complex arrangement than what actual quantum Qrisp [34], [35] or Qmod [36]. These languages are capable computing hardware is able to handle. (That is one of the main of declaring quantum data on a higher level of abstraction, reasons behind the disparity between research progress in both areas.) Yet deferring quantum programming innovation until 1We refer to the computational basis {|0⟩ , |1⟩} when talking about binary terms. However, abstraction achieved through quantum circuits is valid for quantum hardware architectures reach full operational maturity any orthonormal basis of the complex Hilbert space C2 physically realizable. is a methodologically flawed proceeding.

III. A LGEBRAIC F ORMALISM

B. Algebraic laws for quantum circuits

Once quantum circuits are defined, we can continue introducTo properly establish the foundations of this conceptual framework and the semantics of the proposed transformations, ing several laws regarding them. These laws are mainly divided it is appropriate to use an adequate formalism capable of into two categories: quantum if-statement and sequential exhibiting the quantum nature of the operations. The work composition. To better describe these laws, we first introduce a by Ying et al. [25] provides a formalism for treating trans- different notation for quantum if-statements with two possible formations as structured constructs, extending Hoare’s basic outcomes: laws of classical programming [47] to the quantum domain, |ψ0 ⟩ |ψ1 ⟩ C0 ←−−− q −−−→ C1 ≜ qif [q] (|ψ0 ⟩ → C0 □ |ψ1 ⟩ → C1 ) fiq, allowing for expressing low-level semantics as algebra. With (2) this formalism, operations that influence entire registers can with q denoting a single qubit with basis {|ψ0 ⟩ , |ψ1 ⟩}. It is be modeled using high-level statements such as sequential worth noting that this also applies to a quantum register q acting compositions, quantum conditionals, or loops. It is particularly as control whenever only two states from its corresponding interesting due to its capability of verifying recursively defined basis are taken into account. If the quantum if-statement relies quantum circuits and representing lower-level abstractions on more than two branches, this notation is not suitable. when operating on individual qubits [48]. Therefore, it seems 1) Laws of quantum if-statement: Rules regarding a quantum reasonable to argue that it provides appropriate tools for conditional operator can be formalized as follows. When an establishing verifiable programs at a higher level. unitary U changes a basis |ψ0 ⟩ , |ψ1 ⟩ to |φ0 ⟩ , |φ1 ⟩: Although the formalism covers both quantum circuits and |ψ0 ⟩ |ψ1 ⟩ |φ0 ⟩ |φ1 ⟩ programs (i.e., provided with mid-circuit measurements), in this C0 ←−−− q −−−→ C1 ≡ U † [q]; C0 ←−−− q −−−→ C1 ; U [q]. (3) work we will only introduce the former. The reason being that the transformations defined below are all formalized as quantum Quantum conditionals satisfy the idempotence property: circuits, as none of them present mid-circuit measurements. |ψ0 ⟩ |ψ1 ⟩ C ←−−− q −−−→ C ≡ C. (4) However, not all laws regarding quantum circuits are introduced, only those relevant for this work. (Refer to Section 3 and 4 2) Laws of sequential composition: Given a sequence of of [25] for a complete overview.) circuits, its composition can be rewritten as: A. Quantum circuits

U1 [q]; U2 [q] ≡ (U2 U1 )[q], if U2 U1 ∈ U. (5) We consider a set QV of quantum variables. Each quantum Regarding that quantum variables used throughout circuit C variable q ∈ QV represents a quantum system with an associas qv(C), circuit sequences that satisfy qv(C1 ) ∩ qv(C2 ) = ∅ ated Hilbert space denoted by Hq . A sequence q = q1 , . . . , qn obey the commutativity rule: of distinct quantum variables is called a quantum register. That is, a quantum register consists of a quantum system composed C1 ; C2 ≡ C2 ; C1 (6) of subsystems q1 , . . . , qn (typically, these subsystems can be As such, if the composition is established in parallel: thought as individual Nnqubits), where its corresponding Hilbert space is given by i=1 Hqi . Moreover, sequence q 1 , . . . , q N U1 [q]; U2 [r] ≡ U2 [r]; U1 [q] ≡ (U1 ⊗ U2 )[q, r], (7) denotes the concatenation of N registers. Additionally, we if q ∩ r = ∅ and (U1 ⊗ U2 ) ∈ U. have a set U of unitary matrix constants. Each unitary matrix By making use of Eq. (4), the following equivalences for a constant U [{qi }m i=1 ] ∈ U denotes a unitary operation N acting on the subspace spanned by a set of m subsystems m Hqm . sequence involving a quantum conditional can be obtained: Notice that for a given register q composed of n subsystems, C; (C0 ← q → C1 ) = (C; C0 ) ← q → (C; C1 ), (8) if m = n, then U [q] denotes a quantum operation over the (C0 ← q → C1 ); C = (C0 ; C) ← q → (C1 ; C). (9) whole register. In accordance with this basic notation, quantum circuits Likewise, for a sequence comprising quantum conditionals C ∈ QC are defined such that: with the same control conditions, its composition follows: C ::= skip | U [q] | C1 ; . . . ; Cj | qif [q](□di=1 |ψi ⟩ → Ci )fiq. (1) Here, skip denotes an identity operator. U [q] represents an operation U acting on the register q. Meanwhile, C1 ; . . . ; Cj is a sequence of circuits (also presented in this work as seqjl=1 Cl in order to improve readability). Moreover, qif is a quantum if-statement where {|ψi ⟩}di=1 is an orthonormal basis of the Hilbert space associated to control register q, and □di=1 denotes the branching over all possible control states with Ci (i = 1, . . . , d) illustrating different circuits acting on quantum variables outside register q.

|ψ0 ⟩

|ψ1 ⟩

|ψ0 ⟩

|ψ1 ⟩

|ψ0 ⟩

|ψ1 ⟩

(C0 ←−−− q −−−→ C1 ); (D0 ←−−− q −−−→ D1 ) ≡ (C0 ; D0 ) ←−−− q −−−→ (C1 ; D1 ).

(10) IV. C ONCEPTUAL F RAMEWORK In this work, a conceptual framework for enabling a higher level of abstraction for designing quantum programs is proposed. The aim is centered around extending principles from structured programming to the quantum field. First, we start from considering quantum registers as operands that model computational constructs. In essence, a quantum program can be devised as a computable quantum

state that evolves according to the transformations of quantum quantum registers can model computational constructs. That registers, given that these model computational constructs that is, a quantum register is capable of computationally model present quantum traits. These transformations are operations a construct by representing with its basis elements different that act on single quantum registers or that entangle two or states regarding that construct. For instance, basis elements of more of them through composition operations. By performing a a quantum register with D = 4 could each represent one of series (sequences) of semantically meaningful transformations four different water levels in a bottle. In consequence, it is possible operate with a quantum register following a (programming) strategy towards a solution, we are able to modify the global state to obtain the desired result. that acts as a computational construct while hiding details about This directly contributes to the abstraction of the program: by lower-level operations acting on their constituent qubits. That is, realizing operations on sets of quantum registers as undivided the system N dynamics are describe in the complex Hilbert space entities instead of individual qubits, less components are H = j Hqj with unitary operations defined as U : H → H, taking registers as single, undivided entities. Albeit higher instantiated and less details need to be specified. The proposal continues by denoting how a quantum register in abstraction, this conceptual framework is to be engaged for realizing logical evaluations is addressed. With this, it is from two different perspectives: establishing single register possible to formalize a series of transformations that are used transformations dependent on data encoding (i.e., altering a to generalize previously well-know operations among registers. single quantum register based on the entity it models) or These operations are based on quantum phase shifting due ascertaining operations that compose several registers. This to logical constraint satisfaction [3], [49], [50] and parallel work is mainly focused on formalizing composition operations that are not dependent on which computational construct is evaluation [51], [52]. High-level syntax based on these concepts is presented being encoded. Nonetheless, the internal structure of these for increasing the abstraction, however, implementation of transformations would vary depending on the abstract data, these transformations continues to take place at the level prompting distinct single register transformations (e.g., treating of quantum gates on individual qubits. Then, the algebraic a quantum register as representing an integer or a string), even formalism introduced before allows for demarcating how if the overall transformation scheme formalized is left invariant. quantum information is handled and their associated low- B. Quantum registers for logical constraint transformations level semantics. Nevertheless, programmers should continue In order to evaluate complex logical relations in quantum to work with high-level syntax. As such, a suitable quantum registers, it is convenient to structure the Hilbert space programming language ought to be able to translate these associated with each register introducing a subspace dedicated transformations into operations on individual qubits for their to condition evaluation. Each operand register must contain physical implementation. For this reason, we specify both the 2 ancilla qubits that encode information about logical conditions functionality and implementation of the formalized abstractions. placed upon the register. It is important to note that the register and ancillas involved in this operation will be entangled at the A. Quantum registers as operands A quantum register can be described as follows. Let Hq end of the operation, thus uncomputation is relevant. Considering an arbitrary register q composed of m qubits be the complex Hilbert space associated with the quantum whose Hilbert space can be factorized into Hq = Hval ⊗ register q, with dimension D = dim(Hq ). We define a complete H . Here, Hval ∼ = (C2 )⊗m−n with n the number of logical D anc orthonormal set {|ψk ⟩}k=1 that constitutes an arbitrary basis for Hq . The register q is described as the superposition of basis constrains enforced upon the register, contains the superposition of states which yield all register possible values. Meanwhile, elements as: Hanc ∼ = (C2 )⊗n represents ancilla qubits that store information D about the evaluation of certain logical propositions or conditions X q := ck |ψk ⟩ , (11) for each of the superposition states. Then, a valid register q for evaluating n logical relations follows: k=1 where complex coefficients ck ∈ C encode the information 2m−1 embedded into each register. These coefficients can be decomX−1 q := cx |ψx ⟩ ⊗ |f1 (ψx )⟩ ⊗ · · · ⊗ |fn (ψx )⟩ , (12) posed into their probability amplitude and phase components iφk x=0 according to ck = rk e . Term rk = |ck | ∈ [0, 1] represents the probability satisfying the global normalization where the set {|ψx ⟩} constitutes an orthonormal basis that PD amplitude, 2 condition k=1 |ck | = 1; whereas φk ∈ [0, 2π) denotes the encodes data in the subspace Hval , and |fi (ψx )⟩ ∈ {|0⟩ , |1⟩} denotes an ancilla qubit that evaluates the boolean proposition relative phase. Towards realizing a quantum-oriented structured program- fi over the set of values. Note that this quantum register structure is thought for logical ming, quantum registers are considers as operands of transevaluation, and it generates entanglement between ancillas and formations realized through quantum computations (instead of individual qubits). These are able to represent abstract 2 Henceforth, we will use the term ancillas to refer to additional qubits data on a higher level than binary terms following a type- involved throughout computation, and the term auxiliary for those not needed specific encoding. In a sense, this can be extended so that but practical for optimization.

the register. As such, ancillas are temporal (to be uncomputed) resources within this context, and transformations of other nature do not explicitly require appended ancillas. C. Abstraction: PhaseAND(θ)

qubit q. In particular, circuit P hθ generates a global θ-phase shift. Inherently, this phase shift is exclusively extended to the entangled system when controls are activated (i.e., in state |1⟩). However, in order to formalize operations without resorting to auxiliary qubits, we consider one of the involved ancillas as the target while the rest act as controls. Thus, ancillas associated to the set {q i }N i=1 perform a controlled operation acting on one of them, which is ruled out from the control. If all control ancillas are in state |1⟩, a Pθ gate is applied to the target ancilla. That is, a multi-controlled Pθ gate acting on the ancilla qubits of involved registers. Then, high-level syntax from Eq. (13), selecting the last qubit appended as target, can be expressed with the algebraic formalism as:

Within the given structure, the logical conjunction of N conditions is the first operation formalized, namely P haseAN D(θ) (or P h∧,θ for simplicity). As dictated previously, each involved register must encode, at least, one constraint; thus, bi-partitioning every state of the superposition following ancilla evaluation. This transformation objective is to apply a θ-phase shift, to the global system if and only if all conditions encoded on the involved registers are satisfied simultaneously (see Fig. 1). This is a composition operation N  ⊗ni N xi N → Pθ [q N (t)] , where several computational constructs, each subjected to their P h∧,θ [{q i }N i=1 ] ≡ qif [{q i }i=1 ] i=1 □ |ψxi ⟩ |1⟩ (14) own constraints, are arranged into a combined global state that applies phase shift if the logical conjunction of all constraints— where □xj denotes the branching over all possible data states their own and those of others—is satisfied. |ψxj ⟩, ensuring the operation only depends on ancillas and That being said, its high-level syntax follows a quantum ni (except the register related to the target ancilla, where if-statement as: ni = nN − 1). Lastly, the circuit Pθ [q N (t)] indicates the V V application of a Pθ gate strictly on the target ancilla qubit t N ni N P h∧,θ [{q i }N i=1 ] ≡ qif i=1 j=1 fj,q i then P hθ [{q i }i=1 ] else skip fiq, of register q N . (The equivalence between applying the multi(13) controlled circuit P hθ on an auxiliary qubit and that of Eq. (14) with ni the number of logical constraint the i-th register is is proven in Section IV-G.) Of particular note is the possibility subjected to, and fj,qi characterizes each constraint involved. to specify this abstraction when only one constraint on one Also, here P hθ is a circuit that applies a θ-phase shift, and register is specified. This would imply placing a Pθ gate on {q i }N i=1 denoting the set of involved registers. Involved register the ancilla without controls. are entangled after applying the operation, whether or not they Once the transformation P h∧,θ is formalized, we can obtain were entangled beforehand. Moreover, there is no restriction P haseN AN D(θ) (or P h¬(∧),θ ). This can be achieved by to the registers sizes and basis. adding an opposite global phase shift from that of P h∧,θ , i.e, Eq. (13) represents a high-level abstraction intended for applying circuit P h−θ to any qubit of the entangled state: a straightforward understanding, however, this representation needs to be translated into a quantum circuit for its phys- P h¬(∧),θ [{qi }Ni=1 ] ≡ P h∧,−θ [{qi }Ni=1 ]; P hθ [{qi }Ni=1 ] n N ^ ^ ical implementation. Its corresponding realization can be fj,q then skip else P hθ [{q i }N ≡ qif i=1 ] fiq implemented using a single auxiliary qubit. P h∧,θ creates i=1 j=1   an entangled system by performing a multi-controlled circuit n N ^ ^  ≡ qif ¬ fj,q  then P hθ [{q i }N on the auxiliary qubit where ancillas act as controls. Such i=1 ] else skip fiq. i=1 j=1 circuit is P hθ , and said circuit can be obtained through the (15) gate sequence3 X[q]; Pθ [q]; X[q]; Pθ [q] acting on the auxiliary Take into account that these abstractions are equivalent up to a 3Whereas P h represents a circuit that applies a θ-phase shift to the whole global phase factor. Ergo, choosing one or another may yield θ   the same results depending on the program design. state, Pθ denotes the quantum gate: Pθ = 10 e0iθ . i

i

i

i

D. Abstraction: PhaseOR(θ)

Fig. 1. Representation of the P haseAN D(θ) operation functionality on two register with one constraint each. On the right, those states without amplitude contribution are suppressed for simplification. Bars height is an arbitrary depiction of amplitude absolute values while color is related to relative phase.

Following the same methodology, we can formalize the operation P haseOR(θ) (or P h∨,θ ). Analogously as with P h∧,θ , the registers must follow Eq. (12) and after the operation an entangled system is obtained. This operation acts in the same manner as P h∧,θ but evaluates a disjunction instead (see Fig. 2). The associated quantum conditional is not as straightforward as for the conjunction, which only required control and target ancillas in state |1⟩. Here, there are several possible combinations that satisfy the logical relation. For this reason, we infer its structure from that of P h∧,θ . In particular, we exploit the W relation V between disjunction and conjunction such that ¬ ( fj ) ≡ ¬fj . That is, logical N OR is equivalent to logical AN D on negated inputs.

where CΠ0 denotes a circuit that acts on the ancilla conditioned by projector Π0 . Circuit CΠ0 can be achieved by placing a negated multi-controlled operation acting on the ancilla with all value qubits from the register as controls. Correspondingly, a generalization acting on N registers follows: † N N N REF LΠ0 [{q}N i=1 ] ≡ seqi=1 CΠ0,q ; P h¬(∧),π [{q}i=1 ]; seqi=1 CΠ0,qi i

≡ qif

N ^

Π0,qi then skip else P hπ [{q}N i=1 ] fiq,

i=1

Fig. 2. Representation of the P haseOR(θ) operation functionality on two register with one constraint each. On the right, those states without amplitude contribution are suppressed for simplification. Bars height is an arbitrary depiction of amplitude absolute values while color is related to relative phase.

Hence, the abstraction P haseN OR(θ) (or P h¬(∨),θ ) can be constructed from P h∧ in a sequence along the input negations: N N N P h¬(∨),θ [{q i }N i=1 ] ≡ seqi=1 Xq i ; P h∧,θ [{q i }i=1 ]; seqi=1 Xq i ,   n N i __ ≡ qif ¬  fj,qi  then P hθ [{q i }N i=1 ] else skip fiq, i=1 j=1

(16) with seqN X being equal to a parallel sequence, as expressed i=1 i by Eq. (7), of N distinct X circuits. Each Xqi circuit is equivalent to (1mi ⊗ X ni )[q i ], where Pauli-X gates are solely applied on ancillas and mi indicates the number of qubits register q i is composed of. By applying seqN i=1 Xq i again (X is hermitian) after P h∧,θ , the original codification is recovered, following Bennett’s principle [53]. Then, P h∨,θ can be deduced as a sequence composed of P h¬(∨),θ and P h−θ :

(19) taking seqN C as a parallel sequence of N circuits C Π Π 0,q i 0,q i i=1 acting each on its associated register q i , where Π0,qi denotes the corresponding projector for state |0 . . . 0⟩. In consequence, regarding Ck as the circuit that performs state initialization given by operator Uk , the abstraction for reflection across subspace |ψk ⟩ acting on one register follows: REF LΠk [q] ≡ Ck† [q]; REF LΠ0 [q]; Ck [q] ≡ qif Πk then skip else P hπ [q] fiq.

(20)

And its generalization acting on N distinct register can be derived as: † N N N REF LΠki [{q i }N i=1 ] ≡ seqi=1 Cki ; REF LΠ0 [{q i }i=1 ]; seqi=1 Cki

≡ qif

N ^ i=1

Πk,qi then skip else P hπ [{q}N i=1 ] fiq,

(21) where each circuit Cki realizes a distinct operator Uki associated to each register q i . Each circuit Cki will have a different structure depending on how the target state is modeled for distinct computational constructs. N N N P h∨,θ [{q i }i=1 ] ≡ P h¬(∨),−θ [{q i }i=1 ]; P hθ [{q i }i=1 ] This operation can be extended further. Take as an example a ni N _ _ ≡ qif fj,qi then P hθ [q 1 , . . . , q N ] else skip fiq. case where reflection needs to be performed over the orthogonal ⊥ i=1 j=1 subspace |ψk ⟩ . Given the structure of Eq. (21), this can be (17) achieved by modifying the quantum if-statement control with its negation. That is, the middle-sequence component of Eq. (19) E. Abstraction: Reflection Stemming from these logical transformations, it is possible applies P h∧,π instead. Furthermore, consider another instance to formalize a more complex one. This operation represents a where strict inversion is not suitable but an arbitrary phase θ reflection across a certain subspace |ψk ⟩. Mathematically, it can is (e.g., fixed-point quantum search [54], [55]). By adjusting be expressed as 2Πk − 1, with Πk = |ψk ⟩ ⟨ψk | the projector Eq. (21) with a P hθ circuit and Eq. (19) with P h∧,θ , this over subspace spanned by |ψk ⟩. From considering a basis operation can be attained. Reflection is a fundamental part of many algorithms such as change such as Uk Π0 Uk† = Πk , where Π0 = |0 . . . 0⟩ ⟨0 . . . 0|, quantum amplitude amplification [49] or Szegedy quantum † the operation can be rewritten as Uk (2Π0 − 1)Uk . Operator Uk walks [50], both relying on their iterative application. In represents an arbitrary state initialization following Uk |0...0⟩ = fact, it is a concrete case of a phase-shift operator over a |ψk ⟩. The corresponding circuit will vary depending on the certain subspace. If extended, following quantum singular selected subspace. Conversely, 2Π0 − 1 denotes a well-defined value transformation [56], [57], schemes that apply phase-shift operation that can be formalized. It represents a π-phase shift operators could be generalized as polynomial transformations acting on all states except |0 . . . 0⟩. (also used in Hamiltonian simulation [58]). Albeit in its early Notice that this last operation can be obtained by performing stages, this work addresses transformations that may prove P h¬(∧),θ , taking θ = π and constraints that activate one ancilla useful across diverse areas and could benefit from a quantum exclusively for initial state |0 . . . 0⟩ on each involved register. structured programming (e.g., quantum machine learning [59], This initial state is independent of initialization, which is [60], solving quantum linear systems problems [61]). determined by the construction of operator U . A single register reflection is expressed as: F. Abstraction: Synchronization † REF LΠ0 [q] ≡ CΠ0 [q]; P h¬(∧),π [q]; CΠ [q] In parallel to the previously defined transformations, we 0 (18) address a state initialization transformation among registers that ≡ qif Π0 then skip else P hπ [q] fiq,

model the same computational construct. This operation, called Synchronization (or SY N C), stems from Greenberger-HorneZeilinger (GHZ) states [51]. In them, more than two entangled particles exhibit the same behavior.√Mathematically, for a ⊗n ⊗n system of n qubits: (|0⟩ + |1⟩ )/ 2. It is straightforward to acknowledge the reason behind the proposed name. If we establish a GHZ-like state among qubits in the same position over distinct registers, we obtain registers that effectively map the same values in parallel. The register states are not copied, as it is prohibited by the no-cloning theorem [62], but their qubit values are mapped onto other registers:

certain sequences into simpler ones and verify equivalences. Next, we present an example on each of these capabilities. 1) Optimization: Following the rules presented in Section III, sequences can be rewritten and a new sequence that may involve lower implementation costs can be obtained. For instance, a routine composed of sequence (P h∧,θ P h¬(∨),θ′ P h∧,θ′′ )[{q i }N i=1 ], can be optimized. Such optimization, owed to the algebraic characterization, is proven below. First, by illustrating the sequence via conditional notation as presented in Eq. (2): NN

i=1 □

SY N C

PD

k (ck |ψk ⟩) ⊗ |0 . . . 0⟩ ⊗ · · · ⊗ |0 . . . 0⟩ −−−−→

PD

k (ck |ψk ⟩ ⊗ |ψk ⟩ ⊗ · · · ⊗ |ψk ⟩) ,

(22) where {|ψk ⟩}D conform a basis for a complex Hilbert space of k dimension D. Note that this holds if and only if all registers are the same in size, and exactly one of them encodes information in an arbitrary manner while the rest are all initialized in state |0 . . . 0⟩. Based on how GHZ-like states are obtained, we can formalize this initialization abstraction as series of controlled operations with a single control qubit each. Consider that N registers are involved and they are each composed of m qubits. (When coupled with logical abstractions, SY N C subject registers are not intended to include ancillas.) Each controlled operation is executed bit-wise: the i-th qubit of the control register directly targets the j-th qubit of a different register. This operation is iterated over all registers and for all qubits within the control register. Its high-level syntax is: SY N C[{q i }N i=1 ] ≡ q 1 7→ q i for i ∈ [2, N ],

(23)

with i ∈ Z, register q 1 initialized in an arbitrary manner prior to the operation, and q i,j denoting the j-th qubit on register q i . The corresponding algebraic formalism for low-level is:
m seqN i=2 seqj=1 qif q 1,j then X[q i,j ] else skip fiq . (24) As a matter of fact, it is trivial to extend Eq. (23) for the case of uniform superposition initialization of register q 1 . Encoding uniform superposition can be achieved by applying Hadamard gates in every qubit of a register initialized in state |0 . . . 0⟩. As such, it can be obtained as a sequence composed of Hadamard gates on all qubits of register q 1 and SY N C: SY N Cunif [{q i }N i=1 ] ≡

m O

H[q 1 ]; SY N C[{q i }N i=1 ],

(25)

with m the number qubits within register q 1 . G. Sequence optimization and verification Regarding logical transformations, it has been demonstrated that new operations can be formalized based on previously defined ones as reflection has been constructed upon P haseN AN D(π). In a sense, this is possible due to the composability of logical relations. Even so, it seems feasible to further construct more complex abstractions using those formalized beforehand. What is more, the algebraic formalism by Ying et al. [25] not only has the capability of formalizing new transformations but, presumably, is also able to optimize

xi |ψx

⟩|1⟩⊗ni

i Pθ′ [q N (t)] ← [{q i }N −−−−−−−−− −−−−→ (Pθ Pθ′′ )[q N (t)], i=1 ] − (26) with the conditional right side applied when all control ancillas are in state |1⟩, and the left for all ancillas in state |0⟩. Knowing that phase gates are additive (Pθ Pθ′′ = Pθ+θ′′ ):

−1 N Pθ′ [q N ] ← [{q i }N i=1 ] → (Pθ+θ ′′ )[q N ] ≡ (P h¬(∨),θ ′ P h∧,θ+θ ′′ )[{q i }i=1 ],

(27) Assuming arbitrary finely-tuned phase modulation [63], this sequence has one less transformation and, in consequence, lesser implementation costs are achieved. 2) Verification: Likewise, the algebraic framework serves as a tool for verifying equivalences between circuits, that is, their semantics are equivalent. In Section IV-C, it was implied that a multi-controlled circuit P hθ targeting an auxiliary qubit was equivalent to a multi-controlled Pθ gate acting on the ancillas. To illustrate this equivalence we use conditionals definition. From Eq. (2) and for the computational basis, semantics regarding a single qubit conditional follow4 : [[U ′ ← q → U ]] = |0⟩ ⟨0|q ⊗ U ′ + |1⟩ ⟨1|q ⊗ U.

(28)

Assuming a setting with two ancilla qubits for simplicity, a multi-controlled circuit P hθ acting on an auxiliary qubit q3 : q1 → (q2 → (X[q3 ]; Pθ [q3 ]; X[q3 ]; Pθ [q3 ])) ,

(29)

with the equivalent circuit for a controlled Pθ gate being: q1 → Pθ [q2 ],

(30)

with semantics: [[q1 → Pθ [q2 ]]] ≡ |0⟩ ⟨0|q1 ⊗ 1 + |1⟩ ⟨1|q1 ⊗ (|0⟩ ⟨0|q2 + eiθ |1⟩ ⟨1|q2 ).

(31) Arising from the fact that the controlled circuit in Eq. (29) imposes a global θ-phase shift, it is tantamount to operator eiθ 1. Coupled with the conditional definition from Eq. (28), the semantics of Eq. (29) are equivalent to: ≡ |0⟩ ⟨0|q1 ⊗ 1 + |1⟩ ⟨1|q1 ⊗ (|0⟩ ⟨0|q2 ⊗ 1 + |1⟩ ⟨1|q2 ⊗ eiθ 1)   ≡ |0⟩ ⟨0|q1 ⊗ 1 + |1⟩ ⟨1|q1 ⊗ (|0⟩ ⟨0|q2 + eiθ |1⟩ ⟨1|q2 ) ⊗ 1 ≡ [[q1 → Pθ [q2 ]]].

(32) 4 Symbolically, [[syntax]] ≡ semantics.

H. Implementation costs

A. SMT formulation

Although this work is mainly focused on providing a highlevel abstraction framework provided with several formalized operations, it is also important to account for their related implementation costs. For instance, P haseAN D(θ) (and the rest of logical transformations) imply a multi-controlled gate with N − 1 controls. It has been proved that such construction can be simulated in terms of Θ(N 2 ) basic operations [64], and has since been improved to linear-depth [65]. However, this cost can be further reduced by leveraging on auxiliary qubits [66]–[68]. Operations were previously defined so that they would be formally self-contained within the registers without involving external resources. Despite the selected approach for formalization, inclusion of auxiliary qubits may prove beneficial, although such inclusion ought to be program design-independent. In the case of reflection, implementation cost will be tied to the computational construct modeled and the selected subspace. As for synchronization, the sequence of controlled operations grows linearly with the number of registers (distinct control and target operations can be applied in parallel). In this case, using a linear amount of auxiliary qubits with the number of registers allows for reducing the complexity to logarithmic depth by performing fan-out computations [52]. Note that these complexities are presented assuming an allto-all connectivity, and they would need to be adapted for topologies that do not support it. Regarding circuit width, a regime where the number of qubits used should not hinder the implementation as the proposal is intended for large-scale problems. Thereby, size do not pose a problem for as long as it is limited by available quantum resources.

Let x = (x1 , x2 , . . . , xn ) denote a set of variables. A formula F, which is a boolean combination of N clauses, in conjunctive normal form (CNF) is written as:

V. A PPLICATION : Q UANTUM SMT S OLVER

F(x) = f1 (x) ∧ f2 (x) ∧ · · · ∧ fN (x),

(33)

if there exists an assignment x∗ such that F(x∗ ) = True, it is said the formula is satisfiable under x∗ . In this notation, each clause fj is a disjunction of literals: _ fj (x) = ℓj,k , with ℓj,k ∈ {φj,k (x), ¬φj,k (x)}, (34) k

with k the index of each literal in the fj clause and φj,k (x) a predicate (also called atom) of the form φj,k (x) ≡ t1 (x) ▷◁ t2 (x), where t1 (x) and t2 (x) are terms constructed from variables and function symbols and ▷◁ represents predicate symbols. These variables and symbols must be allowed by the respective theory signature Σ, which can be thought of as its alphabet. For instance, in the interpretation for linear integer arithmetic (LIA), predicate symbols satisfy ▷◁ ∈ {=, ̸=, >, <, ≥, ≤}; whereas function symbols are restricted to the set {+, −}5 . Nonetheless, this is not the only manner in which SMT problems are addressed. A boolean combination may not be in a conjunctive normal form, but in a disjunctive normal form (DNF). Here, clauses are connected by conjunctions and each clause is a conjunction of literals. An SMT formula is then a boolean combination of atoms, forming a logical structure that abstracts theory-specific constraints into discrete boolean variables. Thereby, separating the logical structure from the underlying theory semantics. B. Oracles Encoding of information inside registers has been mentioned several times; despite this, no specification on how these encoding are achieved has been given thus far. Mainly, because encoding will depend on the data associated with a construct. Nevertheless, next is the manner in which encoding can be generally expressed for evaluating logical predicates. (This is the other perspective where this conceptual framework is engaged at: single-register transformations dependent on data encoding; still, it will not be further explained beyond oracle introduction in this work.) These encodings are intended for registers that follow the form of Eq. (12). Where, as implied before, an ancilla evaluates a predicate for each value in superposition. Then, oracles are used as the components that enable these data encodings. In quantum computing, an oracle can be defined as a black box that evaluates a certain function f ensuing:

A suitable abstraction is one that, apart from hiding irrelevant details, serves as a useful piece that assists in solving a wide variety of problems. On account of this, the transformations formalized in Section IV are chosen due to their applicability in several algorithms. With this in mind, an example of such applicability is shown; however, take into account that program design using this framework is limited to programs that rely solely on formalized operations. One such a case is Grover’s search algorithm [3]. Following this algorithm’s scheme, a quantum SMT solver can be addressed, based on previous work by Lin et al. [69], using the operations from above. This solver accounts for solving logical formulae where each clause is encoded as a logical constraint restricted by a certain theory signature. In this case, the validation is conducted with clauses that follow relations Of |ψx ⟩ |ψy ⟩ = |ψx ⟩ |ψy ⊕ f (ψx )⟩ , (35) from modular linear integer arithmetic; however, the selection of constructs is not restricted to modulo integers: an SMT which modifies the state amplitudes following f assessment. solver can be understood as a combination of constructs that An oracle for function f acting on register q i can be expressed meet certain criteria. Given this, the algorithm design based using the algebraic formalism as Of [q i ]. on this conceptual framework serves as a structured scheme to any such problem, disregarding the internal data constructs 5 For a more profound understanding of SMT and its formalism, refer may represent. to [70]–[72].

C. Algorithm

subjected to synchronization. Algorithm is conceived following Lin et al. [69], thus synchronization is chosen; however, choosing whether synchronization is advantageous or not should be handled internally by a suitable programming language, not part of the high-level design. Notice that REF LΠ0 can be applied to only one of the registers modeling the same construct, as it would be a redundant operation due to previous † disentanglement brought about by SY N Cunif .

A quantum approach for the SMT problem allows searching the assignments space in superposition, amplifying the amplitudes of those satisfying the constraints while suppressing the rest. In particular, the scheme designed by Lin et al. [69] relies on parallel evaluation of distinct clauses for solving the satisfiability (SAT) problem (where SMT is a generalization of SAT with variables that are not exclusively boolean). In alignment with its design, an extension for SMT that relies on D. Validation the transformations proposed in this work is achieved. A validation of the designed quantum program is performed By employing parallelization a computational construct ex- on Qiskit (v2.3.1) simulation environment [19] by implementing hibiting superposition is simultaneously evaluated for different the corresponding quantum program [73]. Transformations are clauses. This instance is especially relevant when trading-off generalized ad hoc for the specific setting as this programming increased width presents an advantage against concatenating language resorts to individual gate specification. As such, a evaluations of the same register. States satisfying all clauses are more adequate quantum programming language for future marked with a π-phase shift. Then, by performing iterations works should not rely on this low-level implementation. according to Grover’s search [3], it is possible to obtain solution Each register encodes a distinct clause using oracles based states for the problem. Algorithm 1 details the program design on modular arithmetic comparators [74] as described by the for a formula F that may depend on several construct (each respective boolean formula. Integer representation is selected variable denotes a distinct construct) where each construct for simplicity, even so any type of construct following label is subjected to synchronization for evaluating a single clause encoding could be modeled using these same variables. An per register involved. In case evaluation concatenation depth initial test is conducted for a formula that contains a single increase is preferred against width, registers should not be construct (integer values) and is in DNF:

h i h i F(x) = (x > 12) ∧ (x < 17) ∨ (x = 38) ∨ (x > 39) ∧ (x < 43) ∨ (x ≥ 56). (mod 64)

(36) By performing a Grover’s search following the scheme from above, the values that solve the formula, as shown in Fig. 3, are obtained. It is direct to confirm that all values measured correspond to valid solution states for the formula (exact number of Grover’s iterations by design). Its associated circuit is illustrated in Fig. 4. Counts for 1024 shots 80

60

Counts

Algorithm 1 Quantum SMT solver program via Grover’s search for multiple constructs synchronized as an algebraic sequence Require: Formula F with N clauses over m constructs. Let Si ⊆ {1, . . . , N } be the subset of clause indices depending on construct xi . Let q Si denote the corresponding subset of quantum registers. yields a tensor product solution state Ensure: Measurement Nm |ψs ⟩ = i=1 |ψs (xi )⟩ satisfying F. 1: Initialize: 2: q Si ← SY N Cunif [q Si ], ∀ i ∈ {1, . . . , m} 3: Calculate number of iterations k 4: for l = 1 to k do 5: ▷ Parallel clause evaluation 6: for each register j ∈ {1, . . . , N } do 7: q j ← Ofj [q j ] ▷ Evaluate clause fj into q j ancilla 8: end for 9: ▷ Global π-phase shift upon satisfaction of F N 10: {q i }N i=1 ← P h∧,π [{q i }i=1 ] (CNF) 11: (or P h∨,π for DNF) 12: ▷ Uncomputation 13: for each register j ∈ {1, . . . , N } do 14: q j ← Of†j [q j ] ▷ Clear ancillas 15: end for 16: ▷ Amplitude amplification via REFL N 17: {q i }N ← REF L Πki [{q i }i=1 ] i=1 18: ▷ REF LΠ0 on construct representative registers 19: (seqj∈Si Ckj ≡ SY N Cunif [q Si ], ∀i ∈ {1, . . . , m}) 20: end for 21: return Measure one representative register q r (r ∈ Si ) for each i ∈ {1, . . . , m} to obtain |ψs ⟩

40

20

0

13

14

15

16

38

40

41

42

56

57

58

59

60

61

62

63

Measurement Outcome (Integer)

Fig. 3. Histogram representing the results obtained after evaluating Algorithm 1 for the case of Eq. (36) after 1024 shots.

q1 q2

7

Oracle x∈[13,17)

7

Oracle x=38

q4

REF LΠ0

Oracle x=38 † SY N CGHZ

P h∨,π

SY N CGHZ q3

Oracle x∈[13,17)

7

Oracle x∈[40,43)

Oracle x∈[40,43)

7

Oracle x≥56

Oracle x≥56

SY N CGHZ

Fig. 4. Circuit derived from the high-level syntax of Algorithm 1 for the case of Eq. (36).

Counts for 1024 shots

70 60

Counts

50 40 30 20 10 0

201 202 211 212 221 222 231 232 301 302 311 312 321 322 331 332

Measurement Outcome (Integers ordered as x y z)

Fig. 5. Histogram representing the results obtained after evaluating Algorithm 1 for the case of Eq. (37) after 1024 shots.

On the other hand, a second test can be performed on a formula where more than one construct is involved. For instance, formula in CNF: F(x, y, z) = (x ≥ 2) ∧ (y ≥ 0) ∧ (z ≥ 1) ∧ (z < 3), (37) with x, y, and z, all evaluated modulo 4. This formula denotes an instance where several constructs are combined in an structured manner. Fig. 5 plots results obtained following the program design for the proposed formula. VI. D ISCUSSION

and Yue [24], this poses some limitations. Whereas resources like uncomputation are already actively handle by Silq or Qrisp, or entanglement tracking in the case of Twist [78], no actual quantum programming language, to the best of our knowledge, allows the programmer to remain unaware from all these simultaneously. A suitable quantum program design, and subsequent quantum programming language, should handle them in a way where the programmer does not need to resort to designing a quantum program taking them into account. VII. C ONCLUSIONS AND F UTURE W ORK In this work, a conceptual framework where quantum registers act as operands, instead of individual qubits, and operate as single, undivided entities that are treated as computational constructs is introduced. Furthermore, it has succeeded in presenting, through an algebraic formalism, a series of high-level syntax along with their corresponding lowlevel semantics. The formalization of such transformations is fundamental to the abstraction increase and simplification of quantum program design. This lays the groundwork for the construction of a more suitable quantum programming paradigm in which the programmer works at a higher level, instead of being aware of the lower-level implementation. In essence, this work contributes to establishing, at its early stages, some methodological principles towards realizing a high-level quantum structured programming. Additionally, this conceptual framework has enabled the design of a quantum program that sits at an abstraction level where no quantum gates are addressed and relies on previously defined composition operations and data encoding operations that are presented as oracles. Future work will set new transformations that contribute to extending the framework in order to design programs for a wider range of problems. In particular, formalization of a method akin to quantum singular value transformation may allow for the integration of polynomial transformations, which serve as the backbone of many quantum computing areas, into an structured setting. Ultimately, future implementations would benefit from a more appropriate programming language than that used for this work’s validation. Migration towards higher-level programming languages like Silq, Qrisp or Qmod will be considered. Although, a programming language that treats this transformations as primitives would be preferred, taking into account that it is paramount that an adequate programming language relieves the programmer from as many quantum characteristics (e.g., entanglement, uncomputation) as possible to further facilitate the construction of quantum programs.

In this work, we have defined transformations acting on quantum registers using the algebraic formalism introduced by Ying et al. [25]. In comparison, [48] uses this same formalism to generalize lower-level abstractions that act on individual qubits rather than registers. Due to its verification properties, the selected formalism also serves as an appropriate tool for transformation formalization as it enables a future framework where routines are verifiable. As partly demonstrated in Section IV-G, it also provides optimization at a high-level for certain sequences. Hence, obtaining a sequence composed of a simpler structure of operations as a preliminary step prior to translation into the circuit paradigm. However, at this point, this optimization is performed manually as there is no automatization for this process yet. Nonetheless, foundations of a language specification that allows for this direct translation have already been presented [75]. If achieved, then it would be possible to find global restructurings that might otherwise not be feasible using circuit gate-based compilers [76], [77]. Essentially, adopting this approach has allowed us to generalize higher-level abstractions that enable the application of composition operations. Programming languages such as Silq [33], Qrisp [34], [35] or Qmod [36] are especially promising due to their higher-level of data representation but lack a proper framework for handling them in an structured D ISCLOSURE manner. That is where this contribution takes place, at a stage where composition can be achieved among registers, The Zenodo repository cited in Section V was created bringing quantum programming one step closer to high-level with the help of Gemini 3 AI to assist with the structural structured programming. Notwithstanding, this framework organization and management of the documentation. The core serves principally as a method for quantum program design idea, transformations devising and formalization, quantum SMT and, as of now, it is dependent on tracking features of program design, and paper drafting, originate exclusively from quantum mechanics such as entanglement. As stated by Ali our (authors) own work.

R EFERENCES [1] R. P. Feynman, “Simulating physics with computers,” International Journal of Theoretical Physics, vol. 21, no. 6–7, pp. 467–488, 1982. [2] D. Deutsch, “Quantum theory, the Church–Turing principle and the universal quantum computer,” Proceedings of the Royal Society of London. A., vol. 400, no. 1818, pp. 97–117, 1985. [3] L. K. Grover, “A fast quantum mechanical algorithm for database search,” in Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, p. 212–219, 1996. [4] P. W. Shor, “Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer,” SIAM Journal on Computing, vol. 26, no. 5, pp. 1484–1509, 1997. [5] F. Arute et al., “Quantum supremacy using a programmable superconducting processor,” Nature, vol. 574, no. 7779, pp. 505–510, 2019. [6] N. P. De Leon et al., “Materials challenges and opportunities for quantum computing hardware,” Science, vol. 372, no. 6539, 2021. [7] A. Oukaira, “Quantum hardware devices (qhds): Opportunities and challenges,” IEEE Access, vol. 13, pp. 98229–98241, 2025. [8] A. M. Dalzell et al., “Quantum algorithms: A survey of applications and end-to-end complexities,” arXiv preprint arXiv:2310.03011, 2023. [9] T. A. Brun, “Quantum error correction,” Oxford Research Encyclopedia of Physics, 2020. [10] J. M. Murillo et al., “Quantum software engineering: Roadmap and challenges ahead,” ACM Transactions on Software Engineering and Methodology, vol. 34, no. 5, 2025. [11] M. AbuGhanem, “IBM quantum computers: evolution, performance, and future directions,” arXiv preprint arXiv:2410.00916, 2024. [12] Y.-Y. Jiang et al., “Correction to: Advancements in superconducting quantum computing,” National Science Review, vol. 13, no. 2, p. nwaf582, 2026. [13] J. Zhao, “Quantum software engineering: Landscapes and horizons,” arXiv preprint arXiv:2007.07047, 2020. [14] B. Heim et al., “Quantum programming languages,” Nature Reviews Physics, vol. 2, pp. 709–722, 2020. [15] A. J. Abhari et al., “Scaffold: Quantum programming language,” tech. rep., Princeton University, 2012. [16] A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron, “Quipper: a scalable quantum programming language,” ACM SIGPLAN Notices, vol. 48, no. 6, p. 333–342, 2013. [17] K. Svore et al., “Q# enabling scalable quantum computing and development with a high-level dsl,” in Proceedings of the Real World Domain Specific Languages Workshop 2018, no. 7, pp. 1–10, 2018. [18] V. Bergholm et al., “PennyLane: Automatic differentiation of hybrid quantum-classical computations,” arXiv preprint arXiv:1811.04968, 2022. [19] A. Javadi-Abhari et al., “Quantum computing with Qiskit,” arXiv preprint arXiv:2405.08810, 2024. [20] Cirq Developers, “Cirq,” Zenodo, 2025. [21] M. V. Wilkes, D. J. Wheeler, and S. Gill, The preparation of programs for an electronic digital computer. Addison-Wesley Press, 2nd ed., 1957. [22] O. Di Matteo, “The art of abstraction in quantum software,” in 2025 IEEE/ACM International Workshop on Quantum Software Engineering (Q-SE), pp. 25–26, IEEE, 2025. [23] M. Ying, Foundations of quantum programming. Morgan Kaufmann by Elsevier, 2nd ed., 2024. [24] S. Ali and T. Yue, “On the need of quantum-oriented paradigm,” in Proceedings of the 2nd International Workshop on Quantum Programming for Software Engineering, pp. 17–20, 2023. [25] M. Ying, L. Zhou, and G. Barthe, “Laws of quantum programming,” ACM Transactions on Software Engineering and Methodology, vol. 35, no. 7, 2026. [26] B. Liskov and S. Zilles, “Programming with abstract data types,” ACM SIGPLAN Notices, vol. 9, no. 4, pp. 50–59, 1974. [27] E. M. Clarke, O. Grumberg, and D. E. Long, “Model checking and abstraction,” ACM Transactions on Programming Languages and Systems (TOPLAS), vol. 16, no. 5, pp. 1512–1542, 1994. [28] C. Y. Baldwin and K. B. Clark, Design rules, volume 1: The power of modularity. MIT Press, 2000. [29] D. E. Deutsch, “Quantum computational networks,” Proceedings of the Royal Society of London. A., vol. 425, no. 1868, pp. 73–90, 1989. [30] A. Chi-Chih Yao, “Quantum circuit complexity,” in Proceedings of 1993 IEEE 34th Annual Foundations of Computer Science, pp. 352–361, 1993. [31] A. Chakraborty, “QuECT: A new quantum programming paradigm,” arXiv preprint arXiv:1104.0497, 2011.

[32] P. Krantz, M. Kjaergaard, F. Yan, T. P. Orlando, S. Gustavsson, and W. D. Oliver, “A quantum engineer’s guide to superconducting qubits,” Applied Physics Reviews, vol. 6, no. 2, p. 021318, 2019. [33] B. Bichsel, M. Baader, T. Gehr, and M. Vechev, “Silq: A high-level quantum language with safe uncomputation and intuitive semantics,” in Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 286–300, 2020. [34] R. Seidel et al., “Qrisp: A framework for compilable high-level programming of gate-based quantum computers,” arXiv preprint arXiv:2406.14792, 2024. [35] S. Bock, R. Seidel, M. Petrič, N. Tcholtchev, A. Hoffmann, and N. Porges, “Designing a meta-model for the eclipse qrisp edsl for high-level quantum programming,” in Proceedings of the 13th International Conference on Model-Based Software and Systems Engineering - MODELSWARD, vol. 1, pp. 27–39, SciTePress, 2025. [36] M. Vax et al., “Qmod: Expressive high-level quantum modeling,” arXiv preprint arXiv:2502.19368, 2025. [37] R. Cleve, A. Ekert, C. Macchiavello, and M. Mosca, “Quantum algorithms revisited,” Proceedings of the Royal Society of London. A., vol. 454, no. 1969, pp. 339–354, 1998. [38] M. Shaw, D. V. Klein, and T. L. Ross, “Revisiting abstractions for software architecture and tools to support them,” IEEE Transactions on Software Engineering, vol. 51, no. 3, pp. 768–773, 2025. [39] O. Di Matteo, S. Núñez-Corrales, M. Stechły, S. P. Reinhardt, and T. Mattson, “An abstraction hierarchy toward productive quantum programming,” in 2024 IEEE International Conference on Quantum Computing and Engineering (QCE), pp. 979–989, IEEE, 2024. [40] W. C. Shih, “Increasing the level of abstraction as a strategy for accelerating the adoption of complex technologies,” Strategy Science, vol. 6, no. 1, pp. 54–61, 2021. [41] A. P. Black, “Object-oriented programming: Some history, and challenges for the next fifty years,” Information and Computation, vol. 231, pp. 3–20, 2013. [42] V. Vedral, A. Barenco, and A. Ekert, “Quantum networks for elementary arithmetic operations,” Physical Review A, vol. 54, no. 1, p. 147, 1996. [43] T. G. Draper, “Addition on a quantum computer,” arXiv preprint quantph/0008033, 2000. [44] G. Yan et al., “Quantum circuit synthesis and compilation optimization: Overview and prospects,” arXiv preprint arXiv:2407.00736, 2025. [45] T. Goldfriend et al., “Design and synthesis of scalable quantum programs,” arXiv preprint arXiv:2412.07372, 2025. [46] J. Zhao, “When abstraction breaks physics: Rethinking modular design in quantum software,” in 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 3886–3890, 2025. [47] C. Hoare et al., “Laws of programming,” Communications of the ACM, vol. 30, no. 8, pp. 672–686, 1987. [48] M. Ying and Z. Zhang, “Verification of recursively defined quantum circuits,” arXiv preprint arXiv:2404.05934, 2024. [49] G. Brassard, P. Hoyer, M. Mosca, and A. Tapp, “Quantum amplitude amplification and estimation,” arXiv preprint quant-ph/0005055, 2000. [50] M. Szegedy, “Quantum speed-up of markov chain based algorithms,” in 45th Annual IEEE Symposium on Foundations of Computer Science, pp. 32–41, 2004. [51] D. M. Greenberger, M. A. Horne, and A. Zeilinger, “Going beyond Bell’s theorem,” in Kafatos, M. (eds) Bell’s Theorem, Quantum Theory and Conceptions of the Universe. Fundamental Theories of Physics, vol. 37, pp. 69–72, Springer, 1989. [52] C. Moore and M. Nilsson, “Parallel quantum computation and quantum codes,” SIAM Journal on Computing, vol. 31, no. 3, pp. 799–815, 2001. [53] C. H. Bennett, “Logical reversibility of computation,” IBM Journal of Research and Development, vol. 17, no. 6, pp. 525–532, 1973. [54] L. K. Grover, “Fixed-point quantum search,” Physical Review Letters, vol. 95, no. 15, p. 150501, 2005. [55] T. J. Yoder, G. H. Low, and I. L. Chuang, “Fixed-point quantum search with an optimal number of queries,” Physical Review Letters, vol. 113, no. 21, p. 210501, 2014. [56] A. Gilyén, Y. Su, G. H. Low, and N. Wiebe, “Quantum singular value transformation and beyond: exponential improvements for quantum matrix arithmetics,” in Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, pp. 193–204, 2019. [57] J. M. Martyn, Z. M. Rossi, A. K. Tan, and I. L. Chuang, “Grand unification of quantum algorithms,” PRX Quantum, vol. 2, no. 4, p. 040203, 2021. [58] G. H. Low and I. L. Chuang, “Hamiltonian simulation by qubitization,” Quantum, vol. 3, p. 163, 2019.

[59] P. Rebentrost, M. Mohseni, and S. Lloyd, “Quantum support vector machine for big data classification,” Physical Review Letters, vol. 113, p. 130503, 2014. [60] J. Biamonte, P. Wittek, N. Pancotti, P. Rebentrost, N. Wiebe, and S. Lloyd, “Quantum machine learning,” Nature, vol. 549, pp. 195–202, 2017. [61] D. Dervovic, M. Herbster, P. Mountney, S. Severini, N. Usher, and L. Wossnig, “Quantum linear systems algorithms: a primer,” arXiv preprint arXiv:1802.08227, 2018. [62] W. K. Wootters and W. H. Zurek, “A single quantum cannot be cloned,” Nature, vol. 299, pp. 802–803, 1982. [63] D. C. McKay, C. J. Wood, S. Sheldon, J. M. Chow, and J. M. Gambetta, “Efficient Z gates for quantum computing,” Physical Review A, vol. 96, p. 022330, 2017. [64] A. Barenco et al., “Elementary gates for quantum computation,” Physical Review A, vol. 52, p. 3457, 1995. [65] A. J. Da Silva and D. K. Park, “Linear-depth quantum circuits for multiqubit controlled gates,” Physical Review A, vol. 106, p. 042602, 2022. [66] S. Balauca and A. Arusoaie, “Efficient constructions for simulating multi controlled quantum gates,” in International Conference on Computational Science, pp. 179–194, Springer, 2022. [67] J. Nie, W. Zi, and X. Sun, “Quantum circuit for multi-qubit Toffoli gate with optimal resource,” arXiv preprint arXiv:2402.05053, 2024. [68] E. C. Rosa, E. I. Duzzioni, and R. De Santiago, “Optimizing gate decomposition for high-level quantum programming,” Quantum, vol. 9, p. 1659, 2025. [69] S.-W. Lin, T.-F. Wang, Y.-R. Chen, Z. Hou, D. Sanán, and Y. S. Teo, “A parallel and distributed quantum sat solver based on entanglement and

teleportation,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 363–382, Springer, 2024. [70] A. R. Bradley and Z. Manna, The calculus of computation: decision procedures with applications to verification. Springer, 2007. [71] L. De Moura and N. Bjørner, “Satisfiability modulo theories: introduction and applications,” Communications of the ACM, vol. 54, no. 9, pp. 69–77, 2011. [72] C. Barrett and C. Tinelli, “Satisfiability modulo theories,” in Handbook of Model Checking, pp. 305–343, Springer, 2018. [73] D. Chamizo, J. Garcia-Alonso, and J. M. Murillo, “High-level quantum structured programs as quantum registers compositions,” Zenodo, 2026. https://doi.org/10.5281/zenodo.19762069 (Accessed July 2026). [74] J. Sanchez-Rivero, D. Talaván, J. Garcia-Alonso, A. Ruiz-Cortés, and J. M. Murillo, “Automatic generation of efficient oracles: The less-than case,” Journal of Systems and Software, vol. 219, p. 112203, 2025. [75] Z. Zhang and M. Ying, “Quantum register machine: Efficient implementation of quantum recursive programs,” Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, pp. 822–847, 2025. [76] M. Xu et al., “Quartz: superoptimization of quantum circuits,” in Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 625–640, 2022. [77] A. Xu, A. Molavi, L. Pick, S. Tannu, and A. Albarghouthi, “Synthesizing quantum-circuit optimizers,” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 835–859, 2023. [78] C. Yuan, C. McNally, and M. Carbin, “Twist: Sound reasoning for purity and entanglement in quantum programs,” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL, pp. 1–32, 2022.

Related documents

• Model-to-code transformation pipeline : from quantum model to Python / Jan Rohrbach#623868
• PyEncode: An Open-Source Library for Structured Quantum State Preparation#670538
• PyEncode: An Open-Source Library for Structured Quantum State Preparation#668473
• From Pattern Detection to Composition Analysis in Quantum Software#444700
• Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction#1130907