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