Document Open Access Logo

On Dynamic Lifting and Effect Typing in Circuit Description Languages

Authors Andrea Colledan , Ugo Dal Lago

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2022.3.pdf
  • Filesize: 0.83 MB
  • 21 pages

Document Identifiers

Author Details

Andrea Colledan
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France

Funding

The research leading to these results has received funding from the European Union - NextGenerationEU through the Italian Ministry of University and Research under PNRR - M4C2 - I1.4 Project CN00000013 "National Centre for HPC, Big Data and Quantum Computing".

Cite AsGet BibTex

Andrea Colledan and Ugo Dal Lago. On Dynamic Lifting and Effect Typing in Circuit Description Languages. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 3:1-3:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.TYPES.2022.3

Abstract

In the realm of quantum computing, circuit description languages represent a valid alternative to traditional QRAM-style languages. They indeed allow for finer control over the output circuit, without sacrificing flexibility nor modularity. We introduce a generalization of the paradigmatic lambda-calculus Proto-Quipper-M, which models the core features of the quantum circuit description language Quipper. The extension, called Proto-Quipper-K, is meant to capture a very general form of dynamic lifting. This is made possible by the introduction of a rich type and effect system in which not only computations, but also the very types are effectful. The main results we give for the introduced language are the classic type soundness results, namely subject reduction and progress.

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Theory of computation → Type theory
  • Hardware → Quantum computation
Keywords
  • Circuit-Description Languages
  • λ-calculus
  • Dynamic lifting
  • Type and effect systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Thorsten Altenkirch and Jonathan Grattage. A functional quantum programming language. In Proc. of LICS, 2005. URL: https://doi.org/10.1109/lics.2005.1.
  2. Andrea Colledan and Ugo Dal Lago. On dynamic lifting and effect typing in circuit description languages (extended version), 2022. URL: https://arxiv.org/abs/2202.07636.
  3. Ugo Dal Lago and Charles Grellois. Probabilistic termination by monadic affine sized typing. ACM Trans. Program. Lang. Syst., 41(2), March 2019. URL: https://doi.org/10.1145/3293605.
  4. Vincent Danos, Elham Kashefi, and Prakash Panangaden. The measurement calculus. J. ACM, 54(2), April 2007. URL: https://doi.org/10.1145/1219092.1219096.
  5. Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. A tutorial introduction to quantum circuit programming in dependently typed proto-quipper. In Proc. of RC, Berlin, Heidelberg, 2020. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-52482-1_9.
  6. Peng Fu, Kohei Kishida, Neil J. Ross, and Peter Selinger. Proto-quipper with dynamic lifting. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571204.
  7. Peng Fu, Kohei Kishida, and Peter Selinger. Linear dependent type theory for quantum programming languages: Extended abstract. In Proc. of LICS, 2020. URL: https://doi.org/10.1145/3373718.3394765.
  8. Soichiro Fujii, Shin-ya Katsumata, and Paul-André Melliès. Towards a formal theory of graded monads. In Proc. of FoSSaCS, Berlin, Heidelberg, 2016. URL: https://doi.org/10.1007/978-3-662-49630-5_30.
  9. Simon J. Gay. Quantum programming languages: Survey and bibliography. Math. Struct. Comput. Sci., 16(4):581-600, August 2006. URL: https://doi.org/10.1017/S0960129506005378.
  10. Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. An introduction to quantum programming in quipper. In Proc. of RC, pages 110-124, 2013. URL: https://doi.org/10.1007/978-3-642-38986-3_10.
  11. Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper. In Proc. of PLDI, pages 333-342, June 2013. URL: https://doi.org/10.1145/2499370.2462177.
  12. Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Proc. of POPL, pages 633-645, January 2014. URL: https://doi.org/10.1145/2578855.2535846.
  13. Dongho Lee, Valentin Perrelle, Benoît Valiron, and Zhaowei Xu. Concrete Categorical Model of a Quantum Circuit Description Language with Measurement. In Proc. of FSTTCS, volume 213 of LIPIcs, pages 51:1-51:20, 2021. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2021.51.
  14. Alan Mycroft, Dominic Orchard, and Tomas Petricek. Effect systems revisited - control-flow algebra and semantics. In Christian W. Probst, Chris Hankin, and René Rydhof Hansen, editors, Semantics, Logics, and Calculi: Essays Dedicated to Hanne Riis Nielson and Flemming Nielson on the Occasion of Their 60th Birthdays, pages 1-32. Springer International Publishing, Cham, 2016. URL: https://doi.org/10.1007/978-3-319-27810-0_1.
  15. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010. URL: https://doi.org/10.1017/CBO9780511976667.
  16. Flemming Nielson and Hanne Riis Nielson. Type and effect systems. In Ernst-Rüdiger Olderog and Bernhard Steffen, editors, Correct System Design: Recent Insights and Advances, pages 114-136. Springer Berlin Heidelberg, 1999. URL: https://doi.org/10.1007/3-540-48092-7_6.
  17. Jens Palsberg. Toward a universal quantum programming language. XRDS: Crossroads, 26(1):14-17, September 2019. URL: https://doi.org/10.1145/3355759.
  18. Simon Perdrix and Philippe Jorrand. Classically controlled quantum computation. Math. Struct. Comput. Sci., 16(04):601, July 2006. URL: https://doi.org/10.1017/s096012950600538x.
  19. John Preskill. Quantum Computing in the NISQ era and beyond. Quantum, 2:79, August 2018. URL: https://doi.org/10.22331/q-2018-08-06-79.
  20. Francisco Rios and Peter Selinger. A categorical model for a quantum circuit description language. In Proc. of QPL, volume 266, June 2017. URL: https://doi.org/10.4204/EPTCS.266.11.
  21. Neil Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, 2015. Google Scholar
  22. Peter Selinger. A brief survey of quantum programming languages. In Proc. of FLOPS, pages 1-6, 2004. URL: https://doi.org/10.1007/978-3-540-24754-8_1.
  23. Peter Selinger and Benoît Valiron. A lambda calculus for quantum computation with classical control. In Proc. of TLCA, pages 354-368, 2005. URL: https://doi.org/10.1007/11417170_26.
  24. Mingsheng Ying. Foundations of Quantum Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 1st edition, 2016. URL: https://doi.org/10.1016/C2014-0-02660-3.
  25. Bernhard Ömer. Classical concepts in quantum programming. Int. J. Theor. Phys., 44(7):943-955, July 2005. URL: https://doi.org/10.1007/s10773-005-7071-x.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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