@inproceedings(ArdeshirLarijaniE:equcqp,
 author       = {Ardeshir-Larijani, Ebrahim and Simon~J. Gay and Rajagopal Nagarajan},
 year         = {2013},
 title        = {Equivalence Checking of Quantum Protocols},
 booktitle    = {Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '13)},
 series       = {Springer LNCS},
 volume       = {7795},
 pages        = {478--492},
 url          = {http://dx.doi.org/10.1007/978-3-642-36742-7_33},
)
@inproceedings(ArdeshirLarijaniE:vercqp,
 author       = {Ardeshir-Larijani, Ebrahim and Simon~J. Gay and Rajagopal Nagarajan},
 year         = {2014},
 title        = {Verification of Concurrent Quantum Protocols by Equivalence Checking},
 booktitle    = {Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '14)},
 series       = {Springer LNCS},
 volume       = {8413},
 pages        = {500--514},
 url          = {http://dx.doi.org/10.1007/978-3-642-54862-8_42},
)
@article(bbcjp:93,
 author       = {C.~H. Bennett and G.~Brassard and C.~Cr{\'e}peau and R.~Jozsa and A.~Peres and W~K Wootters},
 year         = {1993},
 title        = {Teleporting an unknown quantum state via dual classical and {E}instein-{P}odolsky-{R}osen channels},
 journal      = {Physical Review Letters},
 volume       = {70},
 number       = {13},
 doi          = {10.1103/PhysRevLett.70.1895},
)
@inproceedings(bb:84,
 author       = {Charles~H. Bennett and Gilles Brassard},
 year         = {1984},
 title        = {An Update on Quantum Cryptography},
 editor       = {G.~R. Blakley and David Chaum},
 booktitle    = {CRYPTO},
 series       = {Lecture Notes in Computer Science},
 volume       = {196},
 publisher    = {Springer},
 pages        = {475--480},
 url          = {http://dx.doi.org/10.1007/3-540-39568-7_39},
)
@book(coq:04,
 author       = {Y.~Bertot and P.~Cast\'eran},
 year         = {2004},
 title        = {Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions},
 series       = {EATCS Texts in Theoretical Computer Science},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-07964-5},
)
@misc(cer:13,
 author       = {Cerberis},
 title        = {Layer 2 Link Encryprion with Quantum Key Distribution},
 url          = {http://www.idquantique.com/wordpress/wp-content/uploads/Cerberis-Datasheet.pdf},
 note         = {Retrieved 27.9.2015},
)
@book(chlipalacpdt2011,
 author       = {Adam Chlipala},
 year         = {2011},
 title        = {Certified Programming with Dependent Types},
 publisher    = {MIT Press},
 url          = {{http://adam.chlipala.net/cpdt/}},
 note         = {\url{http://adam.chlipala.net/cpdt/}},
)
@inproceedings(chr:03,
 author       = {Jacek Chrzaszcz},
 year         = {2003},
 title        = {Implementing Modules in the {C}oq System},
 editor       = {David~A. Basin and Burkhart Wolff},
 booktitle    = {TPHOLs},
 series       = {Lecture Notes in Computer Science},
 volume       = {2758},
 publisher    = {Springer},
 pages        = {270--286},
 url          = {http://dx.doi.org/10.1007/10930755_18},
)
@inproceedings(cp:90,
 author       = {Th. Coquand and C.~Paulin-Mohring},
 year         = {1990},
 title        = {Inductively defined types},
 editor       = {P.~Martin-L{\"o}f and G.~Mints},
 booktitle    = {Proceedings of Colog'88},
 series       = {Lecture Notes in Computer Science},
 volume       = {417},
 publisher    = {Springer-Verlag},
 url          = {http://dx.doi.org/10.1007/3-540-52335-9_47},
)
@inproceedings(DBLP:conf/mkm/Cruz-FilipeGW04,
 author       = {Cruz-Filipe, Lu\'{\i}s and Herman Geuvers and Freek Wiedijk},
 year         = {2004},
 title        = {{C}-{C}o{RN}, the {C}onstructive {C}oq {R}epository at {N}ijmegen},
 editor       = {Andrea Asperti and Grzegorz Bancerek and Andrzej Trybulec},
 booktitle    = {MKM},
 series       = {Lecture Notes in Computer Science},
 volume       = {3119},
 publisher    = {Springer},
 pages        = {88--103},
 url          = {http://dx.doi.org/10.1007/978-3-540-27818-4_7},
)
@phdthesis(DavidsonT:forvtq,
 author       = {Timothy A.~S. Davidson},
 year         = {2011},
 title        = {Formal Verification Techniques using Quantum Process Calculus},
 school       = {University of Warwick},
)
@inproceedings(FengY:bisqp,
 author       = {Yuan Feng and Runyao Duan and Mingsheng Ying},
 year         = {2011},
 title        = {Bisimulation for quantum processes},
 booktitle    = {38th ACM Symposium on Principles of Programming Languages (POPL 2011)},
 publisher    = {ACM},
 doi          = {10.1145/1926385.1926446},
)
@misc(FengY:modcqm,
 author       = {Yuan Feng and Nengkun Yu and Mingsheng Ying},
 year         = {2012},
 title        = {Model checking quantum Markov chains},
 howpublished = {arXiv:1205.2187 [quant-ph]},
)
@inproceedings(gn:05,
 author       = {S.~J. Gay and R.~Nagarajan},
 year         = {2005},
 title        = {Communicating Quantum Processes},
 booktitle    = {POPL'05},
 publisher    = {ACM},
 doi          = {10.1145/1040305.1040318},
)
@article(GaySJ:typtcq,
 author       = {Simon~J. Gay and Rajagopal Nagarajan},
 year         = {2006},
 title        = {Types and typechecking for {C}ommunicating {Q}uantum {P}rocesses},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {16},
 number       = {3},
 pages        = {375--406},
 doi          = {10.1017/S0960129506005263},
)
@inproceedings(GaySJ:qmcmcq,
 author       = {Simon~J. Gay and Nikolaos Papanikolaou and Rajagopal Nagarajan},
 year         = {2008},
 title        = {{QMC}: a model-checker for quantum systems},
 booktitle    = {Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008)},
 series       = {Springer LNCS},
 volume       = {5123},
 pages        = {543--547},
 url          = {http://dx.doi.org/10.1007/978-3-540-70545-1_51},
)
@incollection(GaySJ:spevqp,
 author       = {Simon~J. Gay and Nikolaos Papanikolaou and Rajagopal Nagarajan},
 year         = {2010},
 title        = {Specification and verification of quantum protocols},
 booktitle    = {Semantic Techniques in Quantum Computation},
 publisher    = {Cambridge University Press},
)
@article(gon:08,
 author       = {Georges Gonthier},
 year         = {2008},
 title        = {Formal proof - the four color theorem.},
 journal      = {Notices of the American Mathematical Society},
 volume       = {55},
 number       = {11},
 pages        = {1382--1393},
 url          = {http://dx.doi.org/10.1007/978-3-540-87827-8_28},
)
@inproceedings(Gonthier:macpoo,
 author       = {Georges Gonthier and Andrea Asperti and Jeremy Avigad and Yves Bertot and Cyril Cohen and Fran\c{c}ois Garillot and St{\'e}phane~Le Roux and Assia Mahboubi and Russell O'Connor and Sidi~Ould Biha and Ioana Pasca and Laurence Rideau and Alexey Solovyev and Enrico Tassi and Laurent Th{\'e}ry},
 year         = {2013},
 title        = {A Machine-Checked Proof of the Odd Order Theorem},
 editor       = {Sandrine Blazy and Paulin{-}Mohring, Christine and David Pichardie},
 booktitle    = {ITP},
 series       = {Lecture Notes in Computer Science},
 volume       = {7998},
 publisher    = {Springer},
 pages        = {163--179},
 url          = {http://dx.doi.org/10.1007/978-3-642-39634-2},
)
@incollection(how:80,
 author       = {William Howard},
 year         = {1980},
 title        = {The formulae-as-types notion of construction},
 booktitle    = {To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
 publisher    = {Academic Press},
 pages        = {479--490},
)
@misc(coq:13,
 author       = {{INRIA}},
 year         = {2013},
 title        = {The {C}oq Proof Assistant},
 url          = {{http://coq.inria.fr/}},
 note         = {Accessed on 8.5.2013},
)
@inproceedings(JorrandP:towqpa,
 author       = {Philippe Jorrand and Marie Lalire},
 year         = {2004},
 title        = {Toward a Quantum Process Algebra},
 booktitle    = {1st ACM Conference on Computing Frontiers},
 doi          = {10.1145/977091.977108},
)
@article(LalireM:relqpb,
 author       = {Marie Lalire},
 year         = {2006},
 title        = {Relations among quantum processes: bisimilarity and congruence},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {16},
 number       = {3},
 pages        = {407--428},
 doi          = {10.1017/S096012950600524X},
)
@article(Leroy-CompCert-CACM,
 author       = {Xavier Leroy},
 year         = {2009},
 title        = {Formal verification of a realistic compiler},
 journal      = {Communications of the ACM},
 volume       = {52},
 number       = {7},
 pages        = {107--115},
 doi          = {10.1145/1538788.1538814},
 url          = {http://gallium.inria.fr/~xleroy/publi/compcert-CACM.pdf},
)
@misc(mag:13,
 author       = {MagiQ},
 title        = {Quantum Key Distribution System (Q-Box)},
 url          = {http://www.magiqtech.com/Products.html},
 note         = {Retrieved 27.9.2015},
)
@article(MayersD:uncsqc,
 author       = {D.~Mayers},
 year         = {2001},
 title        = {Unconditional {S}ecurity in {Q}uantum {C}ryptography},
 journal      = {Journal of the ACM},
 volume       = {48},
 number       = {3},
 pages        = {351--406},
 doi          = {10.1145/382780.382781},
)
@article(DBLP:journals/iandc/MilnerPW92a,
 author       = {Robin Milner and Joachim Parrow and David Walker},
 year         = {1992},
 title        = {A Calculus of Mobile Processes, I},
 journal      = {Inf. Comput.},
 volume       = {100},
 number       = {1},
 pages        = {1--40},
 doi          = {10.1016/0890-5401(92)90009-5},
)
@book(nc:00,
 author       = {Michael~A. Nielsen and Isaac~L. Chuang},
 year         = {2000},
 title        = {Quantum Computation and Quantum Information},
 publisher    = {Cambridge University Press},
)
@article(pec:07,
 author       = {M.E. Peck},
 year         = {2007},
 title        = {Geneva Vote Will Use Quantum Cryptography},
 journal      = {IEEE Spectrum},
 url          = {http://spectrum.ieee.org/computing/networks/geneva-vote-will-use-quantum-cryptography},
)
@misc(qoq:14,
 author       = {Quantum-Coq},
 year         = {2014},
 title        = {Coq sources for quantum protocol proofs},
 url          = {{https://www.dropbox.com/sh/fhldyg1mfnxdmcl/AAC0T7tWxDrOnt4SZGshOKeua}},
 note         = {Shared Dropbox folder, read only -- work in progress},
)
@article(Riedmatten2004a,
 author       = {H.~de~Riedmatten and I.~Marcikic and W.~Tittel and H.~Zbinden and D.~Collins and N.~Gisin},
 year         = {2004},
 title        = {Long distance quantum teleportation in a quantum relay configuration},
 journal      = {Physical Review Letters},
 volume       = {92},
 number       = {4},
 pages        = {047904},
 doi          = {10.1103/PhysRevLett.92.047904},
)
@article(rp:00,
 author       = {Eleanor~G. Rieffel and Wolfgang Polak},
 year         = {2000},
 title        = {An introduction to quantum computing for non-physicists},
 journal      = {ACM Comput. Surv.},
 volume       = {32},
 number       = {3},
 pages        = {300--335},
 url          = {http://doi.acm.org/10.1145/367701.367709},
)
@article(YingM:algqp,
 author       = {Mingsheng Ying and Yuan Feng and Runyao Duan and Zhengfeng Ji},
 year         = {2009},
 title        = {An algebra of quantum processes},
 journal      = {ACM Transactions on Computational Logic},
 volume       = {10},
 number       = {3},
 pages        = {19},
 doi          = {10.1145/1507244.1507249},
)