Reasoning about Entanglement and Separability in Quantum Higher-Order Functions

  • Frédéric Prost
  • Chaouki Zerrari
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5715)


We present a logical approach to the separability analysis issue for a functional quantum computation language. This logic is inspired by previous works on logical analysis of aliasing for imperative functional programs. Both analyses share similarities notably because they are highly non-compositional. Nevertheless, the intrisic non determinism of quantum computation has a large impact on the definitions of the semantics and the validity of logical assertions. To the knowledge of the authors, it is the first proposal of an entanglement/separability analysis for a functional quantum programming language with higher-order functions.


Quantum State Operational Semantic Quantum Gate Reduction Rule Typing Rule 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AG05]
    Altenkirch, T., Grattage, J.: A functional quantum programming language. In: 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pp. 249–258. IEEE Computer Society, Los Alamitos (2005)CrossRefGoogle Scholar
  2. [Bar96]
    Barber, A.: Dual intuitionistic logic. Technical Report ECS-LFCS-96-347, Laboratory for Foundations of Computer Science, University of Edimburgh (1996)Google Scholar
  3. [BHY05]
    Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing in imperative higher-order functions. In: Danvy, O., Pierce, B.C. (eds.) Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming, ICFP 2005, pp. 280–293 (2005)Google Scholar
  4. [CMS06]
    Chadha, R., Mateus, P., Sernadas, A.: Reasoning about imperative quantum programs. Electr. Notes Theoretical Computer Science 158, 19–39 (2006)CrossRefzbMATHGoogle Scholar
  5. [Hoa69]
    Hoare, T.: An axiomatic basis of computer programming. CACM 12(10), 576–580 (1969)CrossRefzbMATHGoogle Scholar
  6. [NC00]
    Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information. Cambridge University Press, Cambridge (2000)zbMATHGoogle Scholar
  7. [Per07]
    Perdrix, S.: Quantum patterns and types for entanglement and separability. Electronic Notes Theoretical Computer Science 170, 125–138 (2007)CrossRefzbMATHGoogle Scholar
  8. [Per08]
    Perdrix, S.: Quantum entanglement analysis based on abstract interpretation. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 270–282. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. [Pie02]
    Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)zbMATHGoogle Scholar
  10. [Pro07]
    Prost, F.: Taming non-compositionality using new binders. In: Akl, S.G., Calude, C.S., Dinneen, M.J., Rozenberg, G., Wareham, H.T. (eds.) UC 2007. LNCS, vol. 4618, pp. 150–162. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  11. [PZ08]
    Prost, F., Zerrari, C.: A logical analysis of entanglement and separability in quantum higher-order functions (2008),
  12. [Smu68]
    Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)CrossRefzbMATHGoogle Scholar
  13. [SV05]
    Selinger, P., Valiron, B.: A lambda calculus for quantum computation with classical control. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 354–368. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  14. [Vid03]
    Vidal, G.: Efficient classical simulation of slightly entangled quantum computations. Physical Review Letters 91(14) (2003)Google Scholar
  15. [vT04]
    van Tonder, A.: A lambda calculus for quantum computation. SIAM Journal on Computing 33(5), 1109–1135 (2004)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Frédéric Prost
    • 1
  • Chaouki Zerrari
    • 2
  1. 1.Grenoble Université, LIGFrance
  2. 2.VERIMAG, Grenoble UniversitéFrance

Personalised recommendations