Skip to main content
SpringerLink
Log in

\(\mathsf {qPCF}\): A Language for Quantum Circuit Computations

  • Conference paper
  • First Online:
Theory and Applications of Models of Computation (TAMC 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10185))

Abstract

We propose qPCF, a functional language able to define and manipulate quantum circuits in an easy and intuitive way. qPCF follows the tradition of “quantum data & classical control” languages, inspired to the QRAM model. Ideally, qPCF computes finite circuit descriptions which are offloaded to a quantum co-processor (i.e. a quantum device) for the execution. qPCF extends \(\text {PCF}\) with a new kind of datatype: quantum circuits. The typing of qPCF is quite different from the mainstream of “quantum data & classical control” languages that involves linear/exponential modalities. qPCF uses a simple form of dependent types to manage circuits and an implicit form of monad to manage quantum states via a destructive-measurement operator.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Arrighi, P., Dowek, G.: Linear-algebraic lambda-calculus: higher-order, encodings and confluence. In: Proceedings of the 19th Annual Conference on Term Rewriting and Applications, pp. 17–31 (2008)

    Google Scholar 

  2. Aschieri, F., Zorzi, M.: Non-determinism, non-termination and the strong normalization of system T. In: Hasegawa, M. (ed.) TLCA 2013. LNCS, vol. 7941, pp. 31–47. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38946-7_5

    Chapter  Google Scholar 

  3. Aspinall, D., Hofmann, M.: Dependent types. In: Pierce, B. (ed.) Advanced Topics in Types and Programming Languages, Chap. 2, pp. 45–86. MIT Press (2005)

    Google Scholar 

  4. Dal Lago, U., Masini, A., Zorzi, M.: On a measurement-free quantum lambda calculus with classical control. Math. Struct. Comput. Sci. 19(2), 297–335 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  5. Gaboardi, M., Paolini, L., Piccolo, M.: Linearity and PCF: a semantic insight! In: Proceeding of ICFP 2011, pp. 372–384 (2011)

    Google Scholar 

  6. Gaboardi, M., Paolini, L., Piccolo, M.: On the reification of semantic linearity. Math. Struct. Comput. Sci. 26(5), 829–867 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  7. Grattage, J.: An overview of QML with a concrete implementation in haskell. Electron. Not. Theor. Comput. Sci. 270(1), 165–174 (2011)

    Article  MATH  Google Scholar 

  8. Hasuo, I., Hoshino, N.: Semantics of higher-order quantum computation via geometry of interaction. In: LICS 2011, pp. 237–246 (2011)

    Google Scholar 

  9. Kaye, P., Laflamme, R., Mosca, M.: An Introduction to Quantum Computing. Oxford University Press, Oxford (2007)

    MATH  Google Scholar 

  10. Knill, E.: Conventions for quantum pseudocode. Technical Report, Los Alamos National Laboratory (1996)

    Book  Google Scholar 

  11. Lago, U.D., Masini, A., Zorzi, M.: Quantum implicit computational complexity. Theor. Comput. Sci. 411(2), 377–409 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  12. Lago, U.D., Masini, A., Zorzi, M.: Confluence results for a quantum lambda calculus with measurements. Electron. Not. Theor. Comput. Sci. 270(2), 251–261 (2011)

    Article  MATH  Google Scholar 

  13. Lago, U.D., Zorzi, M.: Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inf. Appl. 46(3), 413–450 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  14. Mahmoud, M., Felty, A.P.: Formalization of Metatheory of the Quipper Programming Language in a Linear Logic. University of Ottawa, Canada (2016)

    Google Scholar 

  15. Masini, A., Viganò, L., Zorzi, M.: A qualitative modal representation of quantum register transformations. In: Proceedings of the 38th International Symposium on Multiple-Valued Logic (ISMVL ), pp. 131–137 (2008)

    Google Scholar 

  16. Masini, A., Viganò, L., Zorzi, M.: Modal deduction systems for quantum state transformations. J. Multiple-Valued Logic Soft Comput. 17(5–6), 475–519 (2011)

    MathSciNet  MATH  Google Scholar 

  17. Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2000)

    MATH  Google Scholar 

  18. Nishimura, H., Ozawa, M.: Perfect computational equivalence between quantum turing machines and finitely generated uniform quantum circuit families. Quant. Inf. Process. 8(1), 13–24 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  19. Pagani, M., Selinger, P., Valiron, B.: Applying quantitative semantics to higher-order quantum computing. In: Proceedings of POPL 2014, pp. 647–658. ACM (2014)

    Google Scholar 

  20. Paolini, L., Piccolo, M., Roversi, L.: A class of reversible primitive recursive functions. Electron. Not. Theor. Comput. Sci. 322(18605), 227–242 (2016)

    Article  MathSciNet  MATH  Google Scholar 

  21. Paolini, L., Pimentel, E., Rocca, S.R.: An operational characterization of strong normalization. In: Aceto, L., Ingólfsdóttir, A. (eds.) FoSSaCS 2006. LNCS, vol. 3921, pp. 367–381. Springer, Heidelberg (2006). doi:10.1007/11690634_25

    Chapter  Google Scholar 

  22. Payikin, J., Rand, R., Zdancewic: QWire: A Core Language for Quantum Circuits. University of Pennsylvania, USA (2016)

    Google Scholar 

  23. Pierce, B.C.: Types and Programming Languages. The MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  24. Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5, 223–255 (1977)

    Article  MathSciNet  MATH  Google Scholar 

  25. Roman, S.: Advanced Linear Algebra. Graduate Texts in Mathematics, vol. 135, 3rd edn. Springer, New York (2008)

    Book  MATH  Google Scholar 

  26. Ross, N.: Algebraic and Logical Methods in Quantum Computation. Ph.D. thesis, Dalhousie University Halifax, Nova Scotia (2015)

    Google Scholar 

  27. Selinger, P.: Towards a quantum programming language. Math. Struct. Comput. Sci. 14(4), 527–586 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  28. Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Math. Struct. Comput. Sci. 16, 527–552 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  29. Selinger, P., Valiron, B.: Quantum lambda calculus. In: Semantic Techniques in Quantum Computation, pp. 135–172. Cambridge University Press (2009)

    Google Scholar 

  30. Shende, V.V., Prasad, A.K., Markov, I.L., Hayes, J.P.: Synthesis of reversible logic circuits. IEEE Trans. Comput.-Aided Des. Integr. Circ. Syst. 22(6), 710–722 (2003)

    Article  Google Scholar 

  31. Valiron, B., Ross, N.J., Selinger, P., Alexander, D.S., Smith, J.M.: Programming the quantum future. Commun. ACM 58(8), 52–61 (2015)

    Article  Google Scholar 

  32. Viganò, L., Volpe, M., Zorzi, M.: Quantum state transformations and branching distributed temporal logic. In: Kohlenbach, U., Barceló, P., Queiroz, R. (eds.) WoLLIC 2014. LNCS, vol. 8652, pp. 1–19. Springer, Heidelberg (2014). doi:10.1007/978-3-662-44145-9_1

    Google Scholar 

  33. Viganò, L., Volpe, M., Zorzi, M.: A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations. Inf. Comput., 1–24 (2017). http://dx.doi.org/10.1016/j.ic.2017.01.007

  34. Ying, M.: Foundations of Quantum Programming. Morgan Kaufmann, Cambridge (2016)

    Google Scholar 

  35. Zorzi, M.: On quantum lambda calculi: a foundational perspective. Math. Struct. Comput. Sci. 26(7), 1107–1195 (2016)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Torino, Turin, Italy

    Luca Paolini

  2. Department of Computer Science, University of Verona, Verona, Italy

    Margherita Zorzi

Authors
  1. Luca Paolini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Margherita Zorzi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Luca Paolini or Margherita Zorzi .

Editor information

Editors and Affiliations

  1. Anna University, Chennai, India

    T.V. Gopal

  2. Universität Bern , Bern, Switzerland

    Gerhard Jäger

  3. Universität Bern , Bern, Switzerland

    Silvia Steila

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Paolini, L., Zorzi, M. (2017). \(\mathsf {qPCF}\): A Language for Quantum Circuit Computations. In: Gopal, T., Jäger , G., Steila, S. (eds) Theory and Applications of Models of Computation. TAMC 2017. Lecture Notes in Computer Science(), vol 10185. Springer, Cham. https://doi.org/10.1007/978-3-319-55911-7_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-55911-7_33

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-55910-0

  • Online ISBN: 978-3-319-55911-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation