References

  1. Ebrahim Ardeshir-Larijani, Simon J. Gay & Rajagopal Nagarajan (2013): Equivalence Checking of Quantum Protocols. In: Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '13), Springer LNCS 7795, pp. 478–492. Available at http://dx.doi.org/10.1007/978-3-642-36742-7_33.
  2. Ebrahim Ardeshir-Larijani, Simon J. Gay & Rajagopal Nagarajan (2014): Verification of Concurrent Quantum Protocols by Equivalence Checking. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '14), Springer LNCS 8413, pp. 500–514. Available at http://dx.doi.org/10.1007/978-3-642-54862-8_42.
  3. C. H. Bennett, G. Brassard, C. Crépeau, R. Jozsa, A. Peres & W K Wootters (1993): Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters 70(13), doi:10.1103/PhysRevLett.70.1895.
  4. Charles H. Bennett & Gilles Brassard (1984): An Update on Quantum Cryptography. In: G. R. Blakley & David Chaum: CRYPTO, Lecture Notes in Computer Science 196. Springer, pp. 475–480. Available at http://dx.doi.org/10.1007/3-540-39568-7_39.
  5. Y. Bertot & P. Castéran (2004): Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions. EATCS Texts in Theoretical Computer Science. Springer, doi:10.1007/978-3-662-07964-5.
  6. Cerberis: Layer 2 Link Encryprion with Quantum Key Distribution. Available at http://www.idquantique.com/wordpress/wp-content/uploads/Cerberis-Datasheet.pdf. Retrieved 27.9.2015.
  7. Adam Chlipala (2011): Certified Programming with Dependent Types. MIT Press. Available at http://adam.chlipala.net/cpdt/. http://adam.chlipala.net/cpdt/.
  8. Jacek Chrzaszcz (2003): Implementing Modules in the Coq System. In: David A. Basin & Burkhart Wolff: TPHOLs, Lecture Notes in Computer Science 2758. Springer, pp. 270–286. Available at http://dx.doi.org/10.1007/10930755_18.
  9. Th. Coquand & C. Paulin-Mohring (1990): Inductively defined types. In: P. Martin-Löf & G. Mints: Proceedings of Colog'88, Lecture Notes in Computer Science 417. Springer-Verlag. Available at http://dx.doi.org/10.1007/3-540-52335-9_47.
  10. Luís Cruz-Filipe, Herman Geuvers & Freek Wiedijk (2004): C-CoRN, the Constructive Coq Repository at Nijmegen. In: Andrea Asperti, Grzegorz Bancerek & Andrzej Trybulec: MKM, Lecture Notes in Computer Science 3119. Springer, pp. 88–103. Available at http://dx.doi.org/10.1007/978-3-540-27818-4_7.
  11. Timothy A. S. Davidson (2011): Formal Verification Techniques using Quantum Process Calculus. University of Warwick.
  12. Yuan Feng, Runyao Duan & Mingsheng Ying (2011): Bisimulation for quantum processes. In: 38th ACM Symposium on Principles of Programming Languages (POPL 2011). ACM, doi:10.1145/1926385.1926446.
  13. Yuan Feng, Nengkun Yu & Mingsheng Ying (2012): Model checking quantum Markov chains. arXiv:1205.2187 [quant-ph].
  14. S. J. Gay & R. Nagarajan (2005): Communicating Quantum Processes. In: POPL'05. ACM, doi:10.1145/1040305.1040318.
  15. Simon J. Gay & Rajagopal Nagarajan (2006): Types and typechecking for Communicating Quantum Processes. Mathematical Structures in Computer Science 16(3), pp. 375–406, doi:10.1017/S0960129506005263.
  16. Simon J. Gay, Nikolaos Papanikolaou & Rajagopal Nagarajan (2008): QMC: a model-checker for quantum systems. In: Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), Springer LNCS 5123, pp. 543–547. Available at http://dx.doi.org/10.1007/978-3-540-70545-1_51.
  17. Simon J. Gay, Nikolaos Papanikolaou & Rajagopal Nagarajan (2010): Specification and verification of quantum protocols. In: Semantic Techniques in Quantum Computation. Cambridge University Press.
  18. Georges Gonthier (2008): Formal proof - the four color theorem.. Notices of the American Mathematical Society 55(11), pp. 1382–1393. Available at http://dx.doi.org/10.1007/978-3-540-87827-8_28.
  19. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi & Laurent Théry (2013): A Machine-Checked Proof of the Odd Order Theorem. In: Sandrine Blazy, Christine Paulin-Mohring & David Pichardie: ITP, Lecture Notes in Computer Science 7998. Springer, pp. 163–179. Available at http://dx.doi.org/10.1007/978-3-642-39634-2.
  20. William Howard (1980): The formulae-as-types notion of construction. In: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, pp. 479–490.
  21. INRIA (2013): The Coq Proof Assistant. Available at http://coq.inria.fr/. Accessed on 8.5.2013.
  22. Philippe Jorrand & Marie Lalire (2004): Toward a Quantum Process Algebra. In: 1st ACM Conference on Computing Frontiers, doi:10.1145/977091.977108.
  23. Marie Lalire (2006): Relations among quantum processes: bisimilarity and congruence. Mathematical Structures in Computer Science 16(3), pp. 407–428, doi:10.1017/S096012950600524X.
  24. Xavier Leroy (2009): Formal verification of a realistic compiler. Communications of the ACM 52(7), pp. 107–115, doi:10.1145/1538788.1538814. Available at http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf.
  25. MagiQ: Quantum Key Distribution System (Q-Box). Available at http://www.magiqtech.com/Products.html. Retrieved 27.9.2015.
  26. D. Mayers (2001): Unconditional Security in Quantum Cryptography. Journal of the ACM 48(3), pp. 351–406, doi:10.1145/382780.382781.
  27. Robin Milner, Joachim Parrow & David Walker (1992): A Calculus of Mobile Processes, I. Inf. Comput. 100(1), pp. 1–40, doi:10.1016/0890-5401(92)90009-5.
  28. Michael A. Nielsen & Isaac L. Chuang (2000): Quantum Computation and Quantum Information. Cambridge University Press.
  29. M.E. Peck (2007): Geneva Vote Will Use Quantum Cryptography. IEEE Spectrum. Available at http://spectrum.ieee.org/computing/networks/geneva-vote-will-use-quantum-cryptography.
  30. Quantum-Coq (2014): Coq sources for quantum protocol proofs. Available at https://www.dropbox.com/sh/fhldyg1mfnxdmcl/AAC0T7tWxDrOnt4SZGshOKeua. Shared Dropbox folder, read only – work in progress.
  31. H. de Riedmatten, I. Marcikic, W. Tittel, H. Zbinden, D. Collins & N. Gisin (2004): Long distance quantum teleportation in a quantum relay configuration. Physical Review Letters 92(4), pp. 047904, doi:10.1103/PhysRevLett.92.047904.
  32. Eleanor G. Rieffel & Wolfgang Polak (2000): An introduction to quantum computing for non-physicists. ACM Comput. Surv. 32(3), pp. 300–335. Available at http://doi.acm.org/10.1145/367701.367709.
  33. Mingsheng Ying, Yuan Feng, Runyao Duan & Zhengfeng Ji (2009): An algebra of quantum processes. ACM Transactions on Computational Logic 10(3), pp. 19, doi:10.1145/1507244.1507249.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org