Document Open Access Logo

Resource-Aware Quantum Programming with General Recursion and Quantum Control

Authors Kostia Chardonnet , Emmanuel Hainry , Romain Péchoux , Thomas Vinet

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.12.pdf
  • Filesize: 0.84 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Lambda calculus
  • Theory of computation → Quantum complexity theory
Keywords
  • Hybrid Quantum Programs
  • Resource Analysis

Metrics

Abstract

This paper introduces the hybrid quantum language with general recursion {{Hyrql}}, driven towards resource-analysis. By design, {{Hyrql}} does not require the specification of an initial set of quantum gates. Hence, it is well amenable towards a generic cost analysis, unlike languages that use different sets of quantum gates, which yield quantum circuits of distinct complexity.
Regarding resource-analysis, we show how to relate the runtime of an expressive fragment of {{Hyrql}} programs with the size of the corresponding quantum circuits. We also manage to capture the class of functions computable in quantum polynomial time, which, by Yao’s Theorem, corresponds to families of circuits of polynomial size. Consequently, this result paves the way for the use of termination and runtime-analysis techniques designed for classical programs to guarantee bounds on the size of quantum circuits.

Cite As Get BibTex

Kostia Chardonnet, Emmanuel Hainry, Romain Péchoux, and Thomas Vinet. Resource-Aware Quantum Programming with General Recursion and Quantum Control. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 12:1-12:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.12

Author Details

Kostia Chardonnet
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
Emmanuel Hainry
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
Romain Péchoux
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France
Thomas Vinet
  • Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

Funding

This work is supported by the Plan France 2030 through the PEPR integrated project EPiQ (ANR-22-PETQ-0007) and the HQI platform (ANR-22-PNCQ-0002); by the European Union through the MSCA Staff Exchanges project QCOMICAL (Grant Agreement ID: 101182520); and by the Maison du Quantique MaQuEst.

References

  1. Alastair A. Abbott, Julian Wechs, Dominic Horsman, Mehdi Mhalla, and Cyril Branciard. Communication through coherent control of quantum channels. Quantum, 4:333, September 2020. URL: https://doi.org/10.22331/q-2020-09-24-333.
  2. Thorsten Altenkirch and Jonathan Grattage. A functional quantum programming language. In Logic in Computer Science, LICS'05, pages 249-258. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/lics.2005.1.
  3. Mateus Araújo, Fabio Costa, and Časlav Brukner. Computational advantage from quantum-controlled ordering of gates. Phys. Rev. Lett., 113:250402, December 2014. URL: https://doi.org/10.1103/PhysRevLett.113.250402.
  4. Thomas Arts and Jürgen Giesl. Termination of term rewriting using dependency pairs. Theoretical Computer Science, 236(1):133-178, 2000. URL: https://doi.org/10.1016/S0304-3975(99)00207-8.
  5. Martin Avanzini and Georg Moser. Dependency pairs and polynomial path orders. In International Conference on Rewriting Techniques and Applications, RTA'09, pages 48-62. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02348-4_4.
  6. Martin Avanzini, Georg Moser, Romain Péchoux, Simon Perdrix, and Vladimir Zamdzhiev. Quantum expectation transformers for cost analysis. In Christel Baier and Dana Fisman, editors, LICS '22: Symposium on Logic in Computer Science, pages 10:1-10:13. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533332.
  7. Patrick Baillot and Ugo Dal Lago. Higher-order interpretations and program complexity. Information and Computation, 248:56-81, 2016. URL: https://doi.org/10.1016/j.ic.2015.12.008.
  8. Henk Barendregt. The lambda calculus: its syntax and semantics. Studies in logic and the foundations of Mathematics, 1984. URL: https://doi.org/10.1016/c2009-0-14341-6.
  9. Kathleen Barsse, Romain Péchoux, and Simon Perdrix. A quantum programming language for coherent control, 2025. URL: https://doi.org/10.48550/arXiv.2507.10466.
  10. Ethan Bernstein and Umesh Vazirani. Quantum Complexity Theory. SIAM Journal on Computing, 26(5):1411-1473, October 1997. URL: https://doi.org/10.1137/S0097539796300921.
  11. Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin 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, PLDI ’20, pages 286-300. ACM, June 2020. URL: https://doi.org/10.1145/3385412.3386007.
  12. Guillaume Bonfante, Jean-Yves Marion, and Jean-Yves Moyen. Quasi-interpretations a way to control resources. Theoretical Computer Science, 412(25):2776-2796, June 2011. URL: https://doi.org/10.1016/j.tcs.2011.02.007.
  13. Kostia Chardonnet, Louis Lemonnier, and Benoît Valiron. Semantics for a Turing-Complete Reversible Programming Language with Inductive Types. In Jakob Rehof, editor, Formal Structures for Computation and Deduction (FSCD 2024), volume 299 of LIPIcs, pages 19:1-19:19, 2024. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.19.
  14. Kostia Chardonnet, Alexis Saurin, and Benoît Valiron. A Curry-Howard Correspondence for Linear, Reversible Computation. LIPIcs, Volume 252, CSL 2023, 252:13:1-13:18, 2023. URL: https://doi.org/10.4230/LIPIcs.CSL.2023.13.
  15. Giulio Chiribella, Giacomo Mauro D'Ariano, Paolo Perinotti, and Benoit Valiron. Quantum computations without definite causal structure. Phys. Rev. A, 88:022318, August 2013. URL: https://doi.org/10.1103/PhysRevA.88.022318.
  16. Andrea Colledan and Ugo Dal Lago. Flexible type-based resource estimation in quantum circuit description languages. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704883.
  17. Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open quantum assembly language, 2017. URL: https://arxiv.org/abs/1707.03429.
  18. Andrew W. 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. OpenQASM 3: A broader and deeper quantum assembly language. ACM Transactions on Quantum Computing, 3(3):1-50, September 2022. URL: https://doi.org/10.1145/3505636.
  19. Ugo Dal Lago, Andrea Masini, and Margherita Zorzi. Quantum implicit computational complexity. Theor. Comput. Sci., 411(2):377-409, 2010. URL: https://doi.org/10.1016/J.TCS.2009.07.045.
  20. Kinnari Dave, Louis Lemonnier, Romain Péchoux, and Vladimir Zamdzhiev. Combining quantum and classical control: syntax, semantics and adequacy. In Foundations of Software Science and Computation Structures, FoSSaCS 2025, pages 155-175, Berlin, Heidelberg, 2025. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-90897-2_8.
  21. Nachum Dershowitz. Orderings for term-rewriting systems. Theoretical computer science, 17(3):279-301, 1982. URL: https://doi.org/10.1016/0304-3975(82)90026-3.
  22. Nachum Dershowitz. Termination of rewriting. J. Symb. Comput., 3(1-2):69-115, February 1987. URL: https://doi.org/10.1016/S0747-7171(87)80022-6.
  23. Alejandro Díaz-Caro and Octavio Malherbe. Quantum control in the unitary sphere: Lambda-s1 and its categorical model. Log. Methods Comput. Sci., 18(3), 2022. URL: https://doi.org/10.46298/LMCS-18(3:32)2022.
  24. Jörg Endrullis, Herman Geuvers, and Hans Zantema. Degrees of Undecidability in Term Rewriting, pages 255-270. Springer Berlin Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-04027-6_20.
  25. Yuan Feng and Mingsheng Ying. Quantum Hoare logic with classical variables. ACM Transactions on Quantum Computing, 2(4):1-43, 2021. URL: https://doi.org/10.1145/3456877.
  26. Florent Ferrari, Emmanuel Hainry, Romain Péchoux, and Mário Silva. Quantum programming in polylogarithmic time. In Mathematical Foundations of Computer Science, MFCS 2025, volume 345 of LIPIcs, pages 47:1-47:17, 2025. URL: https://doi.org/10.4230/LIPIcs.MFCS.2025.47.
  27. Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: a scalable quantum programming language. In ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, pages 333-342. ACM, June 2013. URL: https://doi.org/10.1145/2491956.2462177.
  28. Emmanuel Hainry, Romain Péchoux, and Mário Silva. A programming language characterizing quantum polynomial time. In Foundations of Software Science and Computation Structures, Fossacs 2023, pages 156-175. Springer, April 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_8.
  29. Emmanuel Hainry, Romain Péchoux, and Mário Silva. Branch sequentialization in quantum polytime. In Maribel Fernández, editor, Formal Structures for Computation and Deduction, FSCD 2025, volume 337 of LIPIcs, pages 22:1-22:22, 2025. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.22.
  30. Vesa Halava, Tero Harju, Mika Hirvensalo, and Juhani Karhumäki. Skolem’s problem - on the border between decidability and undecidability. Technical Report 683, Turku Center for Computer Science, 2005. URL: https://tucs.fi/publications/view/?pub_id=tHaHaHiKa05a.
  31. Emanuel Knill. Conventions for quantum pseudocode. Technical report, Los Alamos National Lab., 1996. URL: https://arxiv.org/abs/2211.02559.
  32. Hlér Kristjánsson, Tatsuki Odake, Satoshi Yoshida, Philip Taranto, Jessica Bavaresco, Marco Túlio Quintino, and Mio Murao. Exponential separation in quantum query complexity of the quantum switch with respect to simulations with standard quantum circuits, 2024. URL: https://arxiv.org/abs/2409.18420.
  33. Yves Lafont. Soft linear logic and polynomial time. Theor. Comput. Sci., 318(1-2):163-180, 2004. URL: https://doi.org/10.1016/J.TCS.2003.10.018.
  34. Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program termination. In Symposium on Principles of Programming Languages, POPL 2001, pages 81-92, New York, NY, USA, January 2001. ACM. URL: https://doi.org/10.1145/373243.360210.
  35. Louis Lemonnier. The Semantics of Effects : Centrality, Quantum Control and Reversible Recursion. PhD thesis, Université Paris-Saclay, June 2024. URL: https://doi.org/10.70675/0db41738z16f8z447fz8352z236e657df8ee.
  36. Jean-Yves Marion and Romain Péchoux. Sup-interpretations, a semantic method for static analysis of program resources. ACM Trans. Comput. Logic, 10(4), August 2009. URL: https://doi.org/10.1145/1555746.1555751.
  37. Georg Moser. Proof Theory at Work: Complexity Analysis of Term Rewrite Systems. Cumulative habilitation thesis, University of Innsbruck, 2009. URL: https://arxiv.org/abs/0907.5527.
  38. André Nies. Computability and Randomness. Oxford University Press, January 2009. URL: https://doi.org/10.1093/acprof:oso/9780199230761.001.0001.
  39. Romain Péchoux. Complexité implicite : bilan et perspectives. Accreditation to supervise research, Université de Lorraine, October 2020. URL: https://hal.univ-lorraine.fr/tel-02978986.
  40. Lorenzo M. Procopio, Amir Moqanaki, Mateus Araújo, Fabio Costa, Irati Alonso Calafell, Emma G. Dowd, Deny R. Hamel, Lee A. Rozema, Časlav Brukner, and Philip Walther. Experimental superposition of orders of quantum gates. Nature Communications, 6(1), August 2015. URL: https://doi.org/10.1038/ncomms8913.
  41. Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. From symmetric pattern-matching to quantum control. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures, pages 348-364, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-89366-2_19.
  42. Peter Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527-586, August 2004. URL: https://doi.org/10.1017/s0960129504004256.
  43. Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. In Paweł Urzyczyn, editor, Typed Lambda Calculi and Applications, TLCA 2005, pages 354-368. Springer Berlin Heidelberg, 2005. URL: https://doi.org/10.1007/11417170_26.
  44. Peter Selinger and Benoît Valiron. Semantic techniques in quantum computation. In Simon Gay and Ian Mackie, editors, Quantum lambda calculus, pages 135-172. Cambridge University Press, 2009. URL: https://doi.org/10.1017/cbo9781139193313.005.
  45. Peter W. Shor. Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer. SIAM Journal on Computing, 26(5):1484-1509, 1997. URL: https://doi.org/10.1137/S0097539795293172.
  46. Márcio M. Taddei, Jaime Cariñe, Daniel Martínez, Tania García, Nayda Guerrero, Alastair A. Abbott, Mateus Araújo, Cyril Branciard, Esteban S. Gómez, Stephen P. Walborn, Leandro Aolita, and Gustavo Lima. Computational advantage from the quantum superposition of multiple temporal orders of photonic gates. PRX Quantum, 2:010320, February 2021. URL: https://doi.org/10.1103/PRXQuantum.2.010320.
  47. Peter van Emde Boas. Machine Models and Simulations, pages 1-66. Handbook of Theoretical Computer Science. Elsevier, 1990. URL: https://doi.org/10.1016/b978-0-444-88071-0.50006-0.
  48. Finn Voichick, Liyi Li, Robert Rand, and Michael Hicks. Qunity: A unified language for quantum and classical computing. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571225.
  49. Toshiyuki Yamada. Confluence and Termination of Simply Typed Term Rewriting Systems. In Aart Middeldorp, editor, Rewriting Techniques and Applications, pages 338-352, Berlin, Heidelberg, 2001. Springer. URL: https://doi.org/10.1007/3-540-45127-7_25.
  50. Tomoyuki Yamakami. A Schematic Definition of Quantum Polynomial Time Computability. The Journal of Symbolic Logic, 85(4):1546-1587, December 2020. URL: https://doi.org/10.1017/jsl.2020.45.
  51. Mingsheng Ying. Foundations of quantum programming. Elsevier, 2024. URL: https://doi.org/10.1016/C2014-0-02660-3.
  52. Mingsheng Ying and Zhicheng Zhang. Verification of recursively defined quantum circuits, 2024. URL: https://doi.org/10.48550/arXiv.2404.05934.
  53. Charles Yuan, Agnes Villanyi, and Michael Carbin. Quantum control machine: The limits of control flow in quantum programming. Proceedings of the ACM on Programming Languages, 8(OOPSLA1):1-28, April 2024. URL: https://doi.org/10.1145/3649811.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact