@book{nielsen2010quantum,
  title={Quantum Computation and Quantum Information},
  author={Nielsen, Michael A and Chuang, Isaac L},
  year={2010},
  publisher={Cambridge University Press},
  page={89}
}

@article{QHLProver-AFP,
  author  = {Junyi Liu and Bohua Zhan and Shuling Wang and Shenggang Ying and Tao Liu and Yangjia Li and Mingsheng Ying and Naijun Zhan},
  title   = {Quantum Hoare Logic},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2019},
  note    = {\url{https://isa-afp.org/entries/QHLProver.html},
             Formal proof development},
  ISSN    = {2150-914x},
}