Skip to main content
SpringerLink
Log in

A Double Effect λ-calculus for Quantum Computation

  • Conference paper
Programming Languages (SBLP 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8129))

Included in the following conference series:

Abstract

In this paper we present a double effect version of the simply typed λ-calculus where we can represent both pure and impure quantum computations. The double effect calculus comprises a quantum arrow layer defined over a quantum monadic layer. In previous works we have developed the quantum arrow calculus, a calculus where we can consider just impure (or mixed) quantum computations. Technically, here we extend the quantum arrow calculus with a construct (and equations) that allows the communication of the monadic layer with the arrow layer of the calculus. That is, the quantum arrow is defined over a monadic instance enabling to consider pure and impure quantum computations in the same framework. As a practical contribution, the calculus allows to express quantum algorithms including reversible operations over pure states and measurements in the middle of the computation using a traditional style of functional programming and reasoning. We also define equations for algebraic reasoning of computations involving measurements.

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 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 73.00
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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Selinger, P.: Towards a quantum programming language. Mathematical Structures in Computer Science 4(14), 527–586 (2004)

    Article  MathSciNet  Google Scholar 

  2. Altenkirch, T., Grattage, J.: A functional quantum programming language. In: 20th Annual IEEE Symposium on Logic in Computer Science (2005)

    Google Scholar 

  3. van Tonder, A.: A lambda calculus for quantum computation. SIAM Journal of Computing 33, 1109–1135 (2004)

    Article  MATH  Google Scholar 

  4. Arrighi, P., Dowek, G.: Linear-algebraic λ-calculus: higher-order, encodings, and confluence. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 17–31. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science 16(3), 527–552 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  6. Selinger, P., Valiron, B.: Quantum lambda calculus. In: Gay, S., Mackie, I. (eds.) Semantic Techniques in Quantum Computation, pp. 135–172. Cambridge University Press (2009)

    Google Scholar 

  7. Uustalu, T., Vene, V.: The essence of dataflow programming. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 2–18. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  8. Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pp. 14–23. IEEE Press (1989)

    Google Scholar 

  9. Vizzotto, J.K., Altenkirch, T., Sabry, A.: Structuring quantum effects: Superoperators as arrows. Journal of Mathematical Structures in Computer Science: Special Issue in Quantum Programming Languages 16, 453–468 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  10. Hughes, J.: Generalising monads to arrows. Science of Computer Programming 37, 67–111 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  11. Lindley, S., Wadler, P., Yallop, J.: The arrow calculus. Journal of Functional Programming, 51–69 (2010)

    Google Scholar 

  12. Vizzotto, J.K., Librelotto, G.R., Sabry, A.: Reasoning about general quantum programs over mixed states. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol. 5902, pp. 321–335. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  13. Mu, S.C., Bird, R.: Functional quantum programming. In: Second Asian Workshop on Programming Languages and Systems, KAIST, Korea (December 2001)

    Google Scholar 

  14. Vizzotto, J.K., Du Bois, A.R., Sabry, A.: The arrow calculus as a quantum programming language. In: Ono, H., Kanazawa, M., de Queiroz, R. (eds.) WoLLIC 2009. LNCS, vol. 5514, pp. 379–393. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  15. Altenkirch, T., Chapman, J., Uustalu, T.: Relative monads formalised. Under consideration for Publication in Mathematical Structures in Computer Science (2010)

    Google Scholar 

  16. Abramsky, S.: High-level methods for quantum computation and information. In: LICS, pp. 410–414 (2004)

    Google Scholar 

  17. Selinger, P.: Dagger compact closed categories and completely positive maps. Electronic Notes in Theoretical Computer Science 170, 139–163 (2007)

    Article  MathSciNet  Google Scholar 

  18. Coecke, B.: Strongly compact closed semantics. Electronic Notes Theoretical Computer Science 155, 331–340 (2006)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Programa de Pós Graduação em Informática, DELC/CT, Cidade Universitária, Brazil

    Juliana Kaizer Vizzotto, Bruno Crestani Calegaro & Eduardo Kessler Piveta

  2. Universidade Federal de Santa Maria, RS, Brazil

    Juliana Kaizer Vizzotto, Bruno Crestani Calegaro & Eduardo Kessler Piveta

Authors
  1. Juliana Kaizer Vizzotto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bruno Crestani Calegaro
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Eduardo Kessler Piveta
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Programa de Pós-Graduação em Computação, Universidade Federal de Pelotas, Rua Gomes Carneiro 1, Pelotas, RS, Brazil

    André Rauber Du Bois

  2. School of Computing Science, Glasgow University, Lilybank Gardens, G12 8QQ, Glasgow, UK

    Phil Trinder

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Vizzotto, J.K., Calegaro, B.C., Piveta, E.K. (2013). A Double Effect λ-calculus for Quantum Computation. In: Du Bois, A.R., Trinder, P. (eds) Programming Languages. SBLP 2013. Lecture Notes in Computer Science, vol 8129. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40922-6_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40922-6_5

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40921-9

  • Online ISBN: 978-3-642-40922-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation