Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Towards quantum program calculation

Ana Neri

Published Jan 1, 2018• 1 citation
OpenAlex

Abstract

Based on the similarity between the categorial derivation of classical programs from their specification and the category theory approach to quantum physics, this dissertation aims at extending the laws of classical program algebra to quantum programming. In this context, the principles of the algebra of classical programs are applied to quantum programming, in order to verify the feasibility of creating correct-by-construction quantum circuits that can run on quantum devices available in the IBM Q Experience. The reversibility restrictions of quantum circuits are ensured by minimal complements. Moreover, measurements are postponed to the end of recursive computations called “quantamorphisms” to avoid the collapse of quantum states. Quantamorphisms are classical catamorphisms extended to ensure quantum reversibility. The derived quantamorphisms implement quantum cycles (vulg. for-loops) and quantum folds on lists. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. The examples of the calculated quantum programs are simulated in Haskell, Quipper and QISKit and run on the quantum computers of the IBM Q Experience. The main conclusions of this work are that, while all the simulations produced correspond to the predicted results, running these programs on real quantum devices results in a significant amount of errors. As quantum devices are constantly evolving, it is likely that in the near future these devices will increase their reliability, allowing programs to run more accurately. The extension of the quantamorphism concept to more general input structures, such as finite trees, remains a challenge that is left for future work. Also relevant will be the study of conditional quantum control without measurements, which will extend the scope of quantamorphisms as quantum circuit specifications.

Related papers

Compiling Quantamorphisms for the IBM Q Experience

Ana Neri, Rui Soares Barbosa, José N. Oliveira

Based on the connection between the categorical derivation of classical programs from specifications and a category-theoretic approach to quantum information, this paper contributes to extending the laws of classical program algebra to quantum programming. This aims at buildingcorrect-by-constructionquantum circuits to be deployed on quantum devices such as those available through the IBM Q Experience. Reversibility is ensured by minimal complements. Such complementation is extended inductively to encompass catamorphisms on lists (vulgo folds), giving rise to the corresponding recursion scheme in reversible computation. The same idea is then applied to the setting of quantum programming, where computation is expressed by unitary transformations. This yields the notion of ‘quantamorphism’, a structural form of quantum recursion implementing cycles and folds on lists with quantum control flow. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. Such calculated quantum programs prepared in Haskell are pushed through Quipper and the Qiskit interface to IBM Q quantum devices. The generated quantum circuits – often quite large – exhibit the predicted behaviour. However, running them on real quantum devices naturally incurs a significant amount of errors. As quantum technology is rapidly evolving, an increase in reliability is likely in the future, allowing for our programs to run more accurately.

arXiv:2010.10510•IEEE Transactions on Software Engineering•Oct 5, 2021•4 citations

On a Categorically Sound Quantum Programming Language for Circuit Description

Francisco Franklin Sousa Rios

This thesis contains contributions to the mathematical foundations of quantum programming languages. The likely arrival of scalable quantum computers in the not-so-distant future has resulted in a flurry of activity in the development of quantum programming languages. As in classical computing, the transition from a description of a quantum algorithm found in the literature to a hardware-specific set of instructions run on a quantum device is a complex process, prone to errors. This issue is exacerbated in the quantum setting not only by the complexity of quantum algorithms but also by the fragility of quantum information, which renders ineffective some of the classical techniques used to debug programs. In this thesis, we contribute to the solution of some of these issues. We introduce Proto-Quipper-M, a new quantum programming language designed to serve as a testbed for the research and development of sound mathematical semantics and reasoning techniques for quantum programs. We first present Proto-Quipper-M as a formalization of a fragment of Quipper, a high-level functional programming language for describing families of quantum circuits. In particular, we define Proto-Quipper-M as a simply-typed lambda calculus with a special type for quantum circuits and a strong type system designed to enforce linearity on quantum data, and thus prevent violations of the no-cloning property of quantum information. We endow Proto-Quipper-M with computational meaning via a big-step operational semantics and prove that the language is type-safe by showing that it enjoys the type-preservation and error-freeness properties. We also give Proto-Quipper-M a denotational semantics in a suitable class of monoidal categories and show that these categories give rise to linear-non-linear models in the sense of Benton, and thus models of intuitionistic linear logic. Finally, we crystallize the connection between the syntax and the semantics of the language by proving the soundness theorem for Proto-Quipper-M.

•Aug 31, 2021•0 citations

Quantum Orchestras: a Concrete Semantics for Recursive Hybrid Programs

Alex Rice, Dominik Leichtle, Kim Worrall +1 more

Many production quantum programming languages represent hybrid quantum computations by extending a classical base language with a quantum effect, where qubits are addressed by reference, and quantum operations are understood to mutate some external quantum state. However, the semantics of this view of quantum computation remains underdeveloped, especially when the language allows mid-circuit measurements and non-termination. In this work, we provide a general method for building denotational semantics for such languages, by defining the quantum orchestra monad, which precisely captures this style of quantum effect. The monad has a concrete presentation, being based on the formalism of quantum instruments, a common tool in quantum information theory for capturing the action of a quantum process along with its classical outcomes. It acts on the category DCPO, and so enables the interpretation of divergent hybrid programs. The quantum orchestra monad serves as a natural extension of both the classical state monad and the probabilistic powerdomain monad. We investigate some of the subtleties present when trying to naïvely extend these definitions to the quantum non-commutative case.

cs.PLCross-listedarXiv:2607.09605•Jul 13, 2026•0 citations

Structural Verification of Quantum Circuits: A Haskell Implementation via Hoare Logic

Alex Bastianini

As quantum hardware remains limited by qubit count and noise, the efficiency and correctness of quantum programs cannot yet be efficiently checked by execution or classical simulation alone. This thesis develops a Hoare logic for reasoning about the structural properties of quantum circuits produced by Proto-Qiskit, a Qiskit inspired programming language. We define derivation rules that treat commands that modify circuits as assignments, allowing properties such as gate count, circuit width, and depth to be specified and verified. These results are implemented in a Haskell tool that parses annotated Proto-Qiskit programs and proves their validity by generating verification conditions using weakest precondition calculus, with the support of an SMT solver. The tool is demonstrated on parametric example programs, including a quantum Fourier transform circuit, highlighting both its capabilities and its current limitations. Furthermore, we informally discuss the implementation of an optimization-aware extension of the logic based on a quantum state assertion language. This allows triviality conditions to be checked during verification so that redundant gates can be identified and removed while proving the correctness of the resulting optimized circuit. We discuss the issues this extension introduces for automated verification.

•Jul 15, 2026•0 citations

On the Automation of Encoding Processes in the Quantum IO Monad

James Barratt

It is now clear that the use of resilient encoding schemes will be required for any quantum computing device to be realised. However, quantum programmers of the future will not wish to be tied up in the particulars of such encoding schemes. Quantum programming languages and libraries are already being developed, one of which is the Quantum IO Monad. QIO, as it is often abbreviated to, provides an interface to define and simulate quantum computations via a library of functions written in Haskell, a purely functional programming language. A solution is presented that takes an arbitrary QIO program and returns an equivalent program incorporating some specified quantum error correction techniques.

arXiv:1210.0611•Electronic Proceedings in Theoretical Computer Science•Oct 1, 2012•1 citation

Laws of Quantum Programming

Mingsheng Ying, Li Zhou, Gilles Barthe

In this article, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.’s basic laws of classical programming to the quantum setting. These laws characterise the algebraic properties of quantum programs, such as the distributivity of sequential composition over (quantum) \({\mathbf{if}}\) -statements and the unfolding of nested (quantum) \({\mathbf{if}}\) -statements. At the same time, we clarify some subtle differences between certain laws of classical programming and their quantum counterparts. Additionally, we derive a fixpoint characterisation of quantum \({\mathbf{while}}\) -loops and a loop-based realisation of tail recursion in quantum programming. Furthermore, we establish two normal form theorems: one for quantum circuits and one for finite quantum programs. The theory in which these laws are established is formalised in the Coq proof assistant, and all of these laws are mechanically verified. As an application case of our laws, we present a formal derivation of the principle of deferred measurements in dynamic quantum circuits. We expect that these laws can be utilised in correctness-preserving transformation, compilation and automatic code optimisation in quantum programming. In particular, because these laws are formally verified in Coq, they can be confidently applied in quantum programme development.

arXiv:2412.19463•ACM Transactions on Software Engineering and Methodology•Sep 18, 2025•0 citations
Based on the similarity between the categorial derivation of classical programs from their specification and the category theory approach to quantum physics, this dissertation aims at extending the laws of classical program algebra to quantum programming. In this context, the principles of the algebra of classical programs are applied to quantum programming, in order to verify the feasibility of creating correct-by-construction quantum circuits that can run on quantum devices available in the IBM Q Experience. The reversibility restrictions of quantum circuits are ensured by minimal complements. Moreover, measurements are postponed to the end of recursive computations called “quantamorphisms” to avoid the collapse of quantum states. Quantamorphisms are classical catamorphisms extended to ensure quantum reversibility. The derived quantamorphisms implement quantum cycles (vulg. for-loops) and quantum folds on lists. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. The examples of the calculated quantum programs are simulated in Haskell, Quipper and QISKit and run on the quantum computers of the IBM Q Experience. The main conclusions of this work are that, while all the simulations produced correspond to the predicted results, running these programs on real quantum devices results in a significant amount of errors. As quantum devices are constantly evolving, it is likely that in the near future these devices will increase their reliability, allowing programs to run more accurately. The extension of the quantamorphism concept to more general input structures, such as finite trees, remains a challenge that is left for future work. Also relevant will be the study of conditional quantum control without measurements, which will extend the scope of quantamorphisms as quantum circuit specifications.
Based on the connection between the categorical derivation of classical programs from specifications and a category-theoretic approach to quantum information, this paper contributes to extending the laws of classical program algebra to quantum programming. This aims at buildingcorrect-by-constructionquantum circuits to be deployed on quantum devices such as those available through the IBM Q Experience. Reversibility is ensured by minimal complements. Such complementation is extended inductively to encompass catamorphisms on lists (vulgo folds), giving rise to the corresponding recursion scheme in reversible computation. The same idea is then applied to the setting of quantum programming, where computation is expressed by unitary transformations. This yields the notion of ‘quantamorphism’, a structural form of quantum recursion implementing cycles and folds on lists with quantum control flow. By Kleisli correspondence, quantamorphisms can be written as monadic functional programs with quantum parameters. This enables the use of Haskell, a monadic functional programming language, to perform the experimental work. Such calculated quantum programs prepared in Haskell are pushed through Quipper and the Qiskit interface to IBM Q quantum devices. The generated quantum circuits – often quite large – exhibit the predicted behaviour. However, running them on real quantum devices naturally incurs a significant amount of errors. As quantum technology is rapidly evolving, an increase in reliability is likely in the future, allowing for our programs to run more accurately.
This thesis contains contributions to the mathematical foundations of quantum programming languages. The likely arrival of scalable quantum computers in the not-so-distant future has resulted in a flurry of activity in the development of quantum programming languages. As in classical computing, the transition from a description of a quantum algorithm found in the literature to a hardware-specific set of instructions run on a quantum device is a complex process, prone to errors. This issue is exacerbated in the quantum setting not only by the complexity of quantum algorithms but also by the fragility of quantum information, which renders ineffective some of the classical techniques used to debug programs. In this thesis, we contribute to the solution of some of these issues. We introduce Proto-Quipper-M, a new quantum programming language designed to serve as a testbed for the research and development of sound mathematical semantics and reasoning techniques for quantum programs. We first present Proto-Quipper-M as a formalization of a fragment of Quipper, a high-level functional programming language for describing families of quantum circuits. In particular, we define Proto-Quipper-M as a simply-typed lambda calculus with a special type for quantum circuits and a strong type system designed to enforce linearity on quantum data, and thus prevent violations of the no-cloning property of quantum information. We endow Proto-Quipper-M with computational meaning via a big-step operational semantics and prove that the language is type-safe by showing that it enjoys the type-preservation and error-freeness properties. We also give Proto-Quipper-M a denotational semantics in a suitable class of monoidal categories and show that these categories give rise to linear-non-linear models in the sense of Benton, and thus models of intuitionistic linear logic. Finally, we crystallize the connection between the syntax and the semantics of the language by proving the soundness theorem for Proto-Quipper-M.
Many production quantum programming languages represent hybrid quantum computations by extending a classical base language with a quantum effect, where qubits are addressed by reference, and quantum operations are understood to mutate some external quantum state. However, the semantics of this view of quantum computation remains underdeveloped, especially when the language allows mid-circuit measurements and non-termination. In this work, we provide a general method for building denotational semantics for such languages, by defining the quantum orchestra monad, which precisely captures this style of quantum effect. The monad has a concrete presentation, being based on the formalism of quantum instruments, a common tool in quantum information theory for capturing the action of a quantum process along with its classical outcomes. It acts on the category DCPO, and so enables the interpretation of divergent hybrid programs. The quantum orchestra monad serves as a natural extension of both the classical state monad and the probabilistic powerdomain monad. We investigate some of the subtleties present when trying to naïvely extend these definitions to the quantum non-commutative case.
As quantum hardware remains limited by qubit count and noise, the efficiency and correctness of quantum programs cannot yet be efficiently checked by execution or classical simulation alone. This thesis develops a Hoare logic for reasoning about the structural properties of quantum circuits produced by Proto-Qiskit, a Qiskit inspired programming language. We define derivation rules that treat commands that modify circuits as assignments, allowing properties such as gate count, circuit width, and depth to be specified and verified. These results are implemented in a Haskell tool that parses annotated Proto-Qiskit programs and proves their validity by generating verification conditions using weakest precondition calculus, with the support of an SMT solver. The tool is demonstrated on parametric example programs, including a quantum Fourier transform circuit, highlighting both its capabilities and its current limitations. Furthermore, we informally discuss the implementation of an optimization-aware extension of the logic based on a quantum state assertion language. This allows triviality conditions to be checked during verification so that redundant gates can be identified and removed while proving the correctness of the resulting optimized circuit. We discuss the issues this extension introduces for automated verification.
It is now clear that the use of resilient encoding schemes will be required for any quantum computing device to be realised. However, quantum programmers of the future will not wish to be tied up in the particulars of such encoding schemes. Quantum programming languages and libraries are already being developed, one of which is the Quantum IO Monad. QIO, as it is often abbreviated to, provides an interface to define and simulate quantum computations via a library of functions written in Haskell, a purely functional programming language. A solution is presented that takes an arbitrary QIO program and returns an equivalent program incorporating some specified quantum error correction techniques.
In this article, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.’s basic laws of classical programming to the quantum setting. These laws characterise the algebraic properties of quantum programs, such as the distributivity of sequential composition over (quantum) if{\mathbf{if}}if -statements and the unfolding of nested (quantum) if{\mathbf{if}}if -statements. At the same time, we clarify some subtle differences between certain laws of classical programming and their quantum counterparts. Additionally, we derive a fixpoint characterisation of quantum while{\mathbf{while}}while -loops and a loop-based realisation of tail recursion in quantum programming. Furthermore, we establish two normal form theorems: one for quantum circuits and one for finite quantum programs. The theory in which these laws are established is formalised in the Coq proof assistant, and all of these laws are mechanically verified. As an application case of our laws, we present a formal derivation of the principle of deferred measurements in dynamic quantum circuits. We expect that these laws can be utilised in correctness-preserving transformation, compilation and automatic code optimisation in quantum programming. In particular, because these laws are formally verified in Coq, they can be confidently applied in quantum programme development.