References

  1. T. Altenkirch & A.S. Green (2009): The Quantum IO Monad. In: Semantic Techniques in Quantum Computation. Cambridge University Press, pp. 173–205, doi:10.1017/CBO9781139193313.006. Available at http://www.cs.nott.ac.uk/~psztxa/g5xnsc/chapter.pdf.
  2. M. Amy (2018): Towards Large-scale Functional Verification of Universal Quantum Circuits. In: Proc. QPL '18, pp. 1–21, doi:10.4204/EPTCS.287.1.
  3. E.W. Dijkstra (1976): A Discipline of Programming. Prentice-Hall, Englewood Cliffs, NJ.
  4. J. Dunfield & N. Krishnaswami (2019): Bidirectional Typing. Available at https://arxiv.org/abs/1908.05839. Submitted to ACM Computing Surveys.
  5. E. D'hondt & P. Panangaden (2006): Quantum Weakest Preconditions. Math. Struct. Comput. Sci. 16(3), pp. 429–451, doi:10.1017/S0960129506005251. Available at https://www.cs.mcgill.ca/~prakash/Pubs/weakest_mscs.pdf.
  6. P. Fu, K. Kishida & P. Selinger (2020): Linear Dependent Type Theory for Quantum Programming Languages: Extended Abstract. In: Proc. LICS '20, pp. 440453, doi:10.1145/3373718.3394765.
  7. A.S. Green & T. Altenkirch (2008): From Reversible to Irreversible Computations. Electron. Notes Theor. Comput. Sci. 210, pp. 65–74, doi:10.1016/j.entcs.2008.04.018. Proc. QPL '06.
  8. A.S. Green (2010): Towards a formally verified functional quantum programming language. University of Nottingham. Available at http://eprints.nottingham.ac.uk/11457/.
  9. Y. Huang & M. Martonosi (2018): QDB: From Quantum Algorithms Towards Correct Quantum Programs. In: 9th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU '18), pp. 4:1–4:14, doi:10.4230/OASIcs.PLATEAU.2018.4.
  10. Y. Huang & M. Martonosi (2019): Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs. In: Proc. ISCA '19, pp. 541–553, doi:10.1145/3307650.3322213. Available at https://arxiv.org/abs/1905.09721.
  11. C.A.R. Hoare (1969): An Axiomatic Basis for Computer Programming. Commun. ACM 12(10), pp. 576–580, doi:10.1145/363235.363259.
  12. P. Jorrand & S. Perdrix (2009): Abstract Interpretation Techniques for Quantum Computation. In: Semantic Techniques in Quantum Computation. Cambridge University Press, pp. 206–234, doi:10.1017/CBO9781139193313.007.
  13. A. Matuschak & M.A. Nielsen (2019): Quantum Computing for the Very Curious (and other essays). Online. Available at https://quantum.country.
  14. M.A. Nielsen & I.L. Chuang (2010): Quantum Computation and Quantum Information, 10th anniversary edition. Cambridge University Press, doi:10.1017/CBO9780511976667.
  15. A. Nanevski, G. Morrisett & L. Birkedal (2008): Hoare Type Theory, Polymorphism and Separation. J. Funct. Program. 18(56), pp. 865–911, doi:10.1017/S0956796808006953. Available at https://software.imdea.org/~aleks/htt/jfpsep07.pdf.
  16. A. Nanevski, G. Morrisett, A. Shinnar, P. Govereau & L. Birkedal (2008): Ynot: Dependent Types for Imperative Programs. In: Proc. ICFP 08, pp. 229–240, doi:10.1145/1411204.1411237. Available at https://software.imdea.org/~aleks/htt/ynot08.pdf.
  17. J.T. Perconti (2012): Hoare Type Theory: Dependent Types for State. Available at http://www.ccs.neu.edu/home/amal/course/7480-s12/HTT-notes.pdf.
  18. J. Paykin, R. Rand & S. Zdancewic (2017): QWIRE: A Core Language for Quantum Circuits. In: Proc. POPL '17, pp. 846–858, doi:10.1145/3009837.3009894. Available at https://jpaykin.github.io/papers/prz_qwire_2017.pdf.
  19. R. Rand (2018): Formally Verified Quantum Programming. University of Pennsylvania. Available at https://repository.upenn.edu/edissertations/3175.
  20. J.C. Reynolds (2002): Separation Logic: A Logic for Shared Mutable Data Structures. In: Proc. LICS '02, pp. 55–74, doi:10.1109/LICS.2002.1029817. Available at https://www.cs.cmu.edu/~jcr/seplogic.pdf.
  21. N.J. Ross (2015): Algebraic and Logical Methods in Quantum Computation. Dalhousie University. Available at http://arxiv.org/abs/1510.02198.
  22. R. Rand, J. Paykin & S. Zdancewic (2018): QWIRE Practice: Formal Verification of Quantum Circuits in Coq. In: Proc. QPL '17, pp. 119–132, doi:10.4204/EPTCS.266.8.
  23. F. Rios & P. Selinger (2017): A Categorical Model for a Quantum Circuit Description Language (Extended Abstract). In: Proc. QPL '17, pp. 164–178, doi:10.4204/EPTCS.266.11.
  24. R. Rand, A. Sundaram, K. Singhal & B. Lackey (2019): A Type System for Quantum Resources. Available at http://ks.cs.uchicago.edu/publication/quantum-resource-types/. Draft.
  25. R. Rand, A. Sundaram, K. Singhal & B. Lackey (2020): Gottesman Types for Quantum Programs. In: Proc. QPL '20, this volume of EPTCS. Open Publishing Association.
  26. P. Selinger (2020): Dependently Typed Quantum Programming in Proto-Quipper. Available at https://popl20.sigplan.org/details/planqc-2020-papers/15/. Invited talk at PLanQC '20.
  27. K. Singhal (2020): Quantum Hoare Type Theory. Technical Report. University of Chicago. Available at https://arxiv.org/abs/2012.02154. Master's paper.
  28. D. Unruh (2019): Quantum Hoare Logic with Ghost Variables. In: Proc. LICS '19, pp. 1–13, doi:10.1109/LICS.2019.8785779. Available at https://arxiv.org/abs/1902.00325.
  29. J. Vizzotto, T. Altenkirch & A. Sabry (2006): Structuring Quantum Effects: Superoperators as Arrows. Math. Struct. Comput. Sci. 16(3), pp. 453–468, doi:10.1017/S0960129506005287. Available at https://arxiv.org/abs/quant-ph/0501151.
  30. M. Ying (2012): Floyd–Hoare Logic for Quantum Programs. ACM Trans. Program. Lang. Syst. 33(6):19, doi:10.1145/2049706.2049708.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org