@book(Arora09,
 author       = {Sanjeev Arora and Boaz Barak},
 year         = {2009},
 title        = {Computational Complexity: A Modern Approach},
 edition      = {1st},
 publisher    = {Cambridge University Press},
 address      = {New York, NY, USA},
 doi          = {10.1017/CBO9780511804090},
)
@inproceedings(AschieriZ13,
 author       = {Federico Aschieri and Margherita Zorzi},
 year         = {2013},
 title        = {Non-determinism, Non-termination and the Strong Normalization of System {T}},
 booktitle    = {Typed Lambda Calculi and Applications, 11th International Conference, {TLCA} 2013, Eindhoven, The Netherlands, June 26-28, 2013. Lecture Notes in Computer Science, 7941},
 pages        = {31--47},
 doi          = {10.1007/978-3-642-38946-7\_5},
)
@article(AschieriZ16,
 author       = {Federico Aschieri and Margherita Zorzi},
 year         = {2016},
 title        = {On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem},
 journal      = {Theoretical Computer Science},
 volume       = {625},
 pages        = {125--146},
 doi          = {10.1016/j.tcs.2016.02.028},
)
@article(DLZ12,
 author       = {Dal Lago, Ugo and Margherita Zorzi},
 year         = {2012},
 title        = {Probabilistic operational semantics for the lambda calculus},
 journal      = {{RAIRO} - Theoretical Informatics and Applications},
 volume       = {46},
 number       = {3},
 pages        = {413--450},
 doi          = {10.1051/ita/2012012},
)
@article(danos2002acm,
 author       = {Vincent Danos and Russell S. Harmer},
 year         = {2002},
 title        = {Probabilistic Game Semantics},
 journal      = {ACM Trans. Comput. Logic},
 volume       = {3},
 number       = {3},
 pages        = {359--382},
 doi          = {10.1145/507382.507385},
)
@article(diaz11,
 author       = {D{\'{\i}}az{-}Caro, Alejandro and Pablo Arrighi and Manuel Gadella and Jonathan Grattage},
 year         = {2011},
 title        = {Measurements and Confluence in Quantum Lambda Calculi With Explicit Qubits},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {270},
 number       = {1},
 pages        = {59--74},
 doi          = {10.1016/j.entcs.2011.01.006},
)
@article(Grattage11entcs,
 author       = {Jonathan Grattage},
 year         = {2011},
 title        = {An Overview of {QML} With a Concrete Implementation in Haskell},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {270},
 number       = {1},
 pages        = {165--174},
 doi          = {10.1016/j.entcs.2011.01.015},
)
@inproceedings(green2013acm,
 author       = {Alexander S. Green and Peter LeFanu Lumsdaine and Neil J. Ross and Peter Selinger and Beno\^{\i}t Valiron},
 year         = {2013},
 title        = {Quipper: A Scalable Quantum Programming Language},
 booktitle    = {Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation},
 series       = {PLDI '13},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {333--342},
 doi          = {10.1145/2491956.2462177},
)
@book(KLM07,
 author       = {Phillip Kaye and Raymond Laflamme and Michele Mosca},
 year         = {2007},
 title        = {An introduction to quantum computing},
 publisher    = {Oxford University Press},
 address      = {Oxford},
)
@techreport(Knill96,
 author       = {E. Knill},
 year         = {1996},
 title        = {Conventions for quantum pseudocode},
 type         = {Technical Report},
 institution  = {Los Alamos National Laboratory},
 note         = {Technical Report},
)
@inproceedings(LagoZ15,
 author       = {Ugo Dal Lago and Margherita Zorzi},
 year         = {2014},
 title        = {Wave-Style Token Machines and Quantum Lambda Calculi},
 booktitle    = {Proceedings Third International Workshop on Linearity, {LINEARITY} 2014, Vienna, Austria, 13th July, 2014, Electronic Proceedings in Theoretical Computer Science 176},
 pages        = {64--78},
 doi          = {10.4204/EPTCS.176.6},
)
@article(Felty16,
 author       = {Mohamed Yousri Mahmoud and Amy P. Felty},
 year         = {2018},
 title        = {Formal Meta-level Analysis Framework for Quantum Programming Languages},
 journal      = {Electr. Notes Theor. Comput. Sci.},
 volume       = {338},
 pages        = {185--201},
 doi          = {10.1016/j.entcs.2018.10.012},
)
@article(MVZ11,
 author       = {Andrea Masini and Luca Vigan{\`o} and Margherita Zorzi},
 year         = {2011},
 title        = {{Modal Deduction Systems for Quantum State Transformations}},
 journal      = {Multiple-Valued Logic and Soft Computing},
 volume       = {17},
 number       = {5-6},
 pages        = {475--519},
 url          = {https://www.oldcitypublishing.com/journals/mvlsc-home/mvlsc-issue-contents/mvlsc-volume-17-number-5-6-2011/mvlsc-17-5-6-p-475-519/},
)
@book(NieCh10,
 author       = {Michael A. Nielsen and Isaac L. Chuang},
 year         = {2010},
 title        = {Quantum computation and quantum information, 10h Anniversary Edition},
 publisher    = {Cambridge University Press},
 address      = {Cambridge},
 doi          = {10.1017/CBO9780511976667},
)
@book(book1997ia,
 editor       = {Peter W. O'Hearn and Robert D. Tennent},
 year         = {1997},
 title        = {Algol-like Languages.},
 series       = {Progress in Theoretical Computer Science},
 publisher    = {Birkhauser},
 note         = {Two volumes.},
)
@article(ong2004apal,
 author       = {C.-H.L. Ong},
 year         = {2004},
 title        = {An approach to deciding the observational equivalence of Algol-like languages},
 journal      = {Annals of Pure and Applied Logic},
 volume       = {130},
 number       = {1},
 pages        = {125 -- 171},
 doi          = {10.1016/j.apal.2003.12.006},
)
@inproceedings(pagani14acm,
 author       = {Michele Pagani and Peter Selinger and Beno{\^{\i}}t Valiron},
 year         = {2014},
 title        = {Applying quantitative semantics to higher-order quantum computing},
 booktitle    = {Proceedings of {POPL} '14},
 publisher    = {{ACM}},
 pages        = {647--658},
 doi          = {10.1145/2535838.2535879},
)
@article(paolini2018arXivQPCF,
 author       = {L. {Paolini} and M. {Piccolo} and M. {Zorzi}},
 year         = {2019},
 title        = {{QPCF: higher order languages and quantum circuits}},
 journal      = {Journal of Automated Reasoning},
 note         = {To appear.},
)
@article(paolini2006iandc,
 author       = {Luca Paolini},
 year         = {2006},
 title        = {A stable programming language},
 journal      = {Information and Computation},
 volume       = {204},
 number       = {3},
 pages        = {339 -- 375},
 doi          = {10.1016/j.ic.2005.11.002},
)
@article(PaoliniPiccoloRoversi-ENTCS2016,
 author       = {Luca Paolini and Mauro Piccolo and Luca Roversi},
 year         = {2016},
 title        = {A Class of Reversible Primitive Recursive Functions},
 journal      = {Electronic Notes in Theoretical Computer Science},
 volume       = {322},
 number       = {18605},
 pages        = {227--242},
 doi          = {10.1016/j.entcs.2016.03.016},
)
@article(paolini2018ngc,
 author       = {Luca Paolini and Mauro Piccolo and Luca Roversi},
 year         = {2018},
 title        = {On a Class of Reversible Primitive Recursive Functions and Its Turing-Complete Extensions},
 journal      = {New Generation Computing},
 volume       = {36},
 number       = {3},
 pages        = {233--256},
 doi          = {10.1007/s00354-018-0039-1},
)
@inproceedings(paolini2017lncs,
 author       = {Luca Paolini and Margherita Zorzi},
 year         = {2017},
 title        = {q{PCF}: a language for quantum circuit computations},
 booktitle    = {Theory and Applications of Models of Computation},
 series       = {Lecture Notes in Computer Science},
 volume       = {10185},
 publisher    = {Springer},
 pages        = {455--469},
 doi          = {10.1007/978-3-319-55911-7\_33},
)
@inproceedings(qwire,
 author       = {Jennifer Paykin and Robert Rand and Steve Zdancewic},
 year         = {2017},
 title        = {QWIRE: A Core Language for Quantum Circuits},
 booktitle    = {Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
 series       = {POPL 2017},
 publisher    = {ACM},
 address      = {New York, NY, USA},
 pages        = {846--858},
 doi          = {10.1145/3009837.3009894},
)
@book(pierce2002mit,
 author       = {Benjamin C. Pierce},
 year         = {2002},
 title        = {Types and Programming Languages},
 publisher    = {The MIT Press},
)
@incollection(pitts1997chapter,
 author       = {Andrew M. Pitts},
 year         = {1997},
 title        = {Reasoning About Local Variables with Operationally-Based Logical Relations},
 booktitle    = {Algol-like Languages},
 chapter      = {17},
 series       = {Progress in Theoretical Computer Science},
 publisher    = {Birkh{\"a}user},
 pages        = {165--185},
 doi          = {10.1007/978-1-4757-3851-3_7},
)
@inproceedings(qwire2,
 author       = {Robert Rand and Jennifer Paykin and Steve Zdancewic},
 year         = {2017},
 title        = {QWIRE Practice: Formal Verification of Quantum Circuits in Coq},
 booktitle    = {{\rm Proceedings 14th International Conference on} Quantum Physics and Logic, {\rm Nijmegen, The Netherlands, 3-7 July 2017}},
 series       = {EPTCS},
 volume       = {266},
 pages        = {119--132},
 doi          = {10.4204/EPTCS.266.8},
)
@inproceedings(rios2017eptcs,
 author       = {Francisco Rios and Peter Selinger},
 year         = {2018},
 title        = {A Categorical Model for a Quantum Circuit Description Language},
 booktitle    = {{\rm Proceedings 14th International Conference on} Quantum Physics and Logic, {\rm Nijmegen, The Netherlands, 3-7 July 2017}},
 series       = {EPTCS},
 volume       = {266},
 publisher    = {Open Publishing Association},
 pages        = {164--178},
 doi          = {10.4204/EPTCS.266.11},
)
@phdthesis(Ross2015,
 author       = {Neil J. Ross},
 year         = {2015},
 title        = {Algebraic and Logical Methods in Quantum Computation},
 school       = {Department of Mathematics and Statistics, Dalhousie University},
 note         = {Available from arXiv:1510.02198.},
)
@article(selinger2004mscs,
 author       = {Peter Selinger},
 year         = {2004},
 title        = {Towards a Quantum Programming Language},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {14},
 number       = {4},
 pages        = {527--586},
 doi          = {10.1017/S0960129504004256},
)
@article(selinger2006mscs,
 author       = {Peter Selinger and Benoit Valiron},
 year         = {2006},
 title        = {A lambda calculus for quantum computation with classical control},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {16},
 pages        = {527--552},
 doi          = {10.1017/S0960129506005238},
)
@inbook(selinger09chap,
 author       = {Peter Selinger and Beno{\^{\i}}t Valiron},
 year         = {2009},
 title        = {Semantic Techniques in Quantum Computation},
 chapter      = {Quantum lambda calculus},
 pages        = {pp. 135--172},
 publisher    = {Cambridge University Press},
 doi          = {10.1017/CBO9781139193313},
)
@article(simon94,
 author       = {Daniel R. Simon},
 year         = {1994},
 title        = {On the Power of Quantum Computation},
 journal      = {SIAM Journal on Computing},
 volume       = {26},
 pages        = {116--123},
 doi          = {10.1137/S0097539796298637},
)
@article(quipperacm,
 author       = {Beno\^{\i}t Valiron and Neil J. Ross and Peter Selinger and D. Scott Alexander and Jonathan M. Smith},
 year         = {2015},
 title        = {Programming the Quantum Future},
 journal      = {Commun. ACM},
 volume       = {58},
 number       = {8},
 pages        = {52--61},
 doi          = {10.1145/2699415},
)
@inproceedings(VVZ14,
 author       = {Luca Vigan{\`o} and Marco Volpe and Margherita Zorzi},
 year         = {2014},
 title        = {Quantum state transformations and branching distributed temporal logic},
 booktitle    = {Logic, Language, Information, and Computation - 21st International Workshop, WoLLIC 2014, Valpara{\'{\i}}so, Chile, September 1-4, 2014},
 series       = {Lecture Notes in Computer Science 8652},
 publisher    = {Springer},
 pages        = {1--19},
 doi          = {10.1007/978-3-662-44145-9\_1},
)
@article(VVZ17,
 author       = {Luca Vigan\`o and Marco Volpe and Margherita Zorzi},
 year         = {2017},
 title        = {A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations},
 journal      = {Information \& Computation},
 volume       = {255},
 pages        = {311--333},
 doi          = {10.1016/j.ic.2017.01.007},
)
@article(Zorzi16,
 author       = {Margherita Zorzi},
 year         = {2016},
 title        = {On quantum lambda calculi: a foundational perspective},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {26},
 number       = {7},
 pages        = {1107--1195},
 doi          = {10.1017/S0960129514000425},
)