@misc(Qiskit,
 author       = {Gadi Aleksandrowicz et. al.},
 year         = {2019},
 title        = {{Qiskit: An open-source framework for quantum computing}},
 doi          = {10.5281/zenodo.2562111},
)
@inproceedings(AltenkirchGrattageLICS05,
 author       = {Thorsten Altenkirch and Jonathan J. Grattage},
 year         = {2005},
 title        = {A functional quantum programming language},
 booktitle    = {Proceedings of {LICS}-2005},
 publisher    = {IEEE Computer Society},
 pages        = {249--258},
 doi          = {10.1109/LICS.2005.1},
)
@article(ArrighiDiazcaroLMCS12,
 author       = {Pablo Arrighi and D{\'\i}az-Caro, Alejandro},
 year         = {2012},
 title        = {A {S}ystem {F} accounting for scalars},
 journal      = {Logical Methods in Computer Science},
 volume       = {8},
 number       = {1:11},
 doi          = {10.2168/LMCS-8(1:11)2012},
)
@article(ArrighiDiazcaroValironIC17,
 author       = {Pablo Arrighi and D{\'\i}az-Caro, Alejandro and Beno\^it Valiron},
 year         = {2017},
 title        = {The vectorial $\lambda$-calculus},
 journal      = {Information and Computation},
 volume       = {254},
 number       = {1},
 pages        = {105--139},
 doi          = {10.1016/j.ic.2017.04.001},
)
@inproceedings(ArrighiDowekRTA08,
 author       = {Pablo Arrighi and Gilles Dowek},
 year         = {2008},
 title        = {Linear-algebraic $\lambda$-calculus: higher-order, encodings, and confluence},
 editor       = {Andrei Voronkov},
 booktitle    = {Rewritting Techniques and Applications (RTA 2008)},
 series       = {Lecture Notes in Computer Science},
 volume       = {5117},
 publisher    = {Springer},
 pages        = {17--31},
 doi          = {10.1007/978-3-540-70590-1_2},
)
@article(ArrighiDowekLMCS17,
 author       = {Pablo Arrighi and Gilles Dowek},
 year         = {2017},
 title        = {Lineal: A linear-algebraic lambda-calculus},
 journal      = {Logical Methods in Computer Science},
 volume       = {13},
 number       = {1:8},
 doi          = {10.23638/LMCS-13(1:8)2017},
)
@inproceedings(BentonCSL94,
 author       = {Nick Benton},
 year         = {1994},
 title        = {A mixed linear and non-linear logic: Proofs, terms and models},
 editor       = {Leszek Pacholski and Jerzy Tiuryn},
 booktitle    = {Computer Science Logic (CSL 1994)},
 series       = {Lecture Notes in Computer Science},
 volume       = {933},
 publisher    = {Springer},
 pages        = {121--135},
 doi          = {10.1007/BFb0022251},
)
@article(BirkhoffvonNeumann36,
 author       = {Garrett Birkhoff and John von Neumann},
 year         = {1936},
 title        = {The logic of quantum mechanics},
 journal      = {Annals of Mathematics},
 volume       = {37},
 number       = {4},
 pages        = {823--843},
 doi          = {10.2307/1968621},
)
@inproceedings(ChardonnetSaurinValironRC20,
 author       = {Kostia Chardonnet and Alexis Saurin and Beno\^it Valiron},
 year         = {2020},
 title        = {Towards a Curry-Howard equivalence for linear, reversible computation},
 editor       = {Ivan Lanese and Mariusz Rawski},
 booktitle    = {Reversible Computation (RC 2020)},
 series       = {Lecture Notes in Computer Science},
 volume       = {12227},
 publisher    = {Springer},
 pages        = {348--364},
 doi          = {10.1007/978-3-030-52482-1_8},
)
@inproceedings(DiazcaroDowekTPNC17,
 author       = {D{\'\i}az-Caro, Alejandro and Gilles Dowek},
 year         = {2017},
 title        = {Typing quantum superpositions and measurement},
 editor       = {Mart{\'\i}n-Vide, Carlos and Roman Neruda and Vega-Rodr{\'\i}guez, Miguel A.},
 booktitle    = {Theory and Practice of Natural Computing (TPNC 2017)},
 series       = {Lecture Notes in Computer Science},
 volume       = {10687},
 publisher    = {Springer},
 pages        = {281--293},
 doi          = {10.1007/978-3-319-71069-3_22},
)
@inproceedings(SystemI,
 author       = {D{\'\i}az-Caro, Alejandro and Gilles Dowek},
 year         = {2019},
 title        = {Proof normalisation in a logic identifying isomorphic propositions},
 editor       = {Herman Geuvers},
 booktitle    = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
 series       = {Leibniz International Proceedings in Informatics (LIPIcs)},
 volume       = {131},
 pages        = {14:1--14:23},
 doi          = {10.4230/LIPIcs.FSCD.2019.14},
)
@misc(SystemIeta,
 author       = {D\'{\i}az-Caro, Alejandro and Gilles Dowek},
 year         = {2020},
 title        = {Extensional proofs in a propositional logic modulo isomorphisms},
 howpublished = {arXiv:2002.03762},
)
@inproceedings(DiazcaroDowekICTAC2021,
 author       = {D\'{\i}az-Caro, Alejandro and Gilles Dowek},
 year         = {2021},
 title        = {A new connective in natural deduction, and its application to quantum computing},
 editor       = {Antonio Cerone and Peter Csaba {\"O}lveczky},
 booktitle    = {Theoretical Aspects of Computing (ICTAC 2021)},
 series       = {Lecture Notes in Computer Science},
 volume       = {12819},
 publisher    = {Springer},
 pages        = {175--193},
 doi          = {10.1007/978-3-030-85315-0_11},
)
@article(DiazcaroDowekRinaldiBIO19,
 author       = {D\'{\i}az-Caro, Alejandro and Gilles Dowek and {Juan Pablo} Rinaldi},
 year         = {2019},
 title        = {Two linearities for quantum computing in the lambda calculus},
 journal      = {BioSystems},
 volume       = {186},
 pages        = {104012},
 doi          = {10.1016/j.biosystems.2019.104012},
)
@inproceedings(DiazcaroGuillermoMiquelValironLICS19,
 author       = {D\'{\i}az-Caro, Alejandro and Mauricio Guillermo and Alexandre Miquel and Beno\^{\i}t Valiron},
 year         = {2019},
 title        = {Realizability in the unitary sphere},
 booktitle    = {Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019)},
 pages        = {1--13},
 doi          = {10.1109/LICS.2019.8785834},
)
@inproceedings(DiazcaroMalherbeLSFA18,
 author       = {D\'{\i}az-Caro, Alejandro and Octavio Malherbe},
 year         = {2019},
 title        = {A concrete categorical semantics for Lambda-S},
 editor       = {Beniamino Accattoli and Carlos Olarte},
 booktitle    = {Logical and Semantic Frameworks with Applications (LSFA'18)},
 series       = {Electronic Notes in Theoretical Computer Science},
 volume       = {344},
 publisher    = {Elsevier},
 pages        = {83--100},
 doi          = {10.1016/j.entcs.2019.07.006},
)
@article(DiazcaroMalherbeACS2020,
 author       = {D\'{\i}az-Caro, Alejandro and Octavio Malherbe},
 year         = {2020},
 title        = {A categorical construction for the computational definition of vector spaces},
 journal      = {Applied Categorical Structures},
 volume       = {28},
 number       = {5},
 pages        = {807--844},
 doi          = {10.1007/s10485-020-09598-7},
)
@misc(DiazcaroMalherbe2021,
 author       = {D\'{\i}az-Caro, Alejandro and Octavio Malherbe},
 year         = {2021},
 title        = {A concrete model for a linear algebraic lambda calculus},
 howpublished = {arXiv:1806.09236},
)
@misc(DiazcaroMalherbe2020b,
 author       = {D\'{\i}az-Caro, Alejandro and Octavio Malherbe},
 year         = {2021},
 title        = {Quantum control in the unitary sphere: Lambda-$\mathcal S_1$ and its categorical model},
 howpublished = {arXiv:2012.05887},
)
@inproceedings(DiazcaroMartinezlopezIFL15,
 author       = {D\'iaz-Caro, Alejandro and Mart\'inez L\'opez, Pablo E.},
 year         = {2015},
 title        = {Isomorphisms considered as equalities: Projecting functions and enhancing partial application through an implementation of $\lambda^+$},
 booktitle    = {Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages (IFL 2015)},
 series       = {ICPS Proceedings},
 publisher    = {ACM},
 pages        = {9:1--9:11},
 doi          = {10.1145/2897336.2897346},
)
@inproceedings(DiazcaroPetitWoLLIC12,
 author       = {D{\'\i}az-Caro, Alejandro and Barbara Petit},
 year         = {2012},
 title        = {Linearity in the non-deterministic call-by-value setting},
 editor       = {Luke Ong and {de Queiroz}, Ruy},
 booktitle    = {Logic, Language, Information and Computation (WoLLIC 2012)},
 series       = {Lecture Notes in Computer Science},
 volume       = {7456},
 pages        = {216--231},
 doi          = {10.1007/978-3-642-32621-9_16},
)
@misc(DowekICTAC2021,
 author       = {Gilles Dowek},
 year         = {2021},
 title        = {Presentation of \cite{DiazcaroDowekICTAC2021} at ICTAC 2021},
 url          = {https://drive.google.com/file/d/1E1DLQfTUg48jC325kOCNnftVgBe_k01A/view},
)
@misc(DowekQPL2021,
 author       = {Gilles Dowek},
 year         = {2021},
 title        = {Presentation of \cite{DiazcaroDowekICTAC2021} at QPL 2021},
 url          = {https://www.youtube.com/watch?v=au0TDDp5qSw},
)
@book(Dummett,
 author       = {Michael Dummett},
 year         = {1991},
 title        = {The logical basis of metaphysics},
 publisher    = {Duckworth},
)
@article(Gentzen,
 author       = {Gerhard Gentzen},
 year         = {1935},
 title        = {Untersuchungen \"uber das logische {S}chlie{\ss}en},
 journal      = {Mathematische Zeitschrift},
 volume       = {39},
 pages        = {176--210},
 doi          = {10.1007/BF01201353},
)
@article(GreenLeFanulumsdaineRossSelingerValironPLDI13,
 author       = {Alexander S. Green and Peter LeFanu Lumsdaine and Neil J. Ross and Peter Selinger and Beno\^it Valiron},
 year         = {2013},
 title        = {Quipper: a scalable quantum programming language},
 journal      = {ACM SIGPLAN Notices (PLDI'13)},
 volume       = {48},
 number       = {6},
 pages        = {333--342},
 doi          = {10.1145/2491956.2462177},
)
@article(KleeneJSL45,
 author       = {Stephen C. Kleene},
 year         = {1945},
 title        = {On the interpretation of intuitionistic number theory},
 journal      = {The Journal of Symbolic Logic},
 volume       = {10},
 number       = {4},
 pages        = {109--124},
 doi          = {10.2307/2269016},
)
@techreport(KnillTR96,
 author       = {Emanuel H. Knill},
 year         = {1996},
 title        = {Conventions for quantum pseudocode},
 type         = {Technical Report},
 number       = {LA-UR-96-2724},
 institution  = {Los Alamos National Laboratory},
 doi          = {10.2172/366453},
)
@article(KrivinePS09,
 author       = {Jean-Louis Krivine},
 year         = {2009},
 title        = {Realizability in classical logic},
 journal      = {Panoramas et synth\`eses: Interactive models of computation and program behaviour},
 volume       = {27},
 pages        = {197--229},
 url          = {hal-00154500},
)
@misc(LemonnierChardonnetValiron21,
 author       = {Louis Lemonnier and Kostia Chardonnet and Beno\^it Valiron},
 year         = {2021},
 title        = {Categorical semantics of reversible pattern-matching},
 howpublished = {arXiv:2109.05837},
)
@article(MillerPimentel,
 author       = {Dave Miller and Elaine Pimentel},
 year         = {2013},
 title        = {A formal framework for specifying sequent calculus proof systems},
 journal      = {Theoretical Computer Science},
 volume       = {474},
 pages        = {98--116},
 doi          = {10.1016/j.tcs.2012.12.008},
)
@inproceedings(MiquelTLCA11,
 author       = {Alexandre Miquel},
 year         = {2011},
 title        = {A survey of classical realizability},
 editor       = {Luke Ong},
 booktitle    = {Typed Lambda Calculi and Applications (TLCA 2011)},
 series       = {Lecture Notes in Computer Science},
 volume       = {6690},
 pages        = {1--2},
 doi          = {10.1007/978-3-642-21691-6_1},
)
@book(NegriPlato,
 author       = {Sara Negri and Jan von Plato},
 year         = {2008},
 title        = {Structural Proof Theory},
 publisher    = {Cambridge University Press},
)
@book(NielsenChuang00,
 author       = {Michael {Nielsen} and Isaac Chuang},
 year         = {2000},
 title        = {Quantum Computation and Quantum Information},
 publisher    = {Cambridge University Press.},
 doi          = {10.1017/CBO9780511976667},
)
@misc(NoriegaDiazcaro20,
 author       = {Francisco Noriega and D\'iaz-Caro, Alejandro},
 year         = {2020},
 title        = {The Vectorial Lambda Calculus Revisited},
 howpublished = {arXiv:2007.03648},
)
@incollection(Parigot,
 author       = {Michel Parigot},
 year         = {1991},
 title        = {Free deduction: An analysis of ``Computations'' in classical logic},
 editor       = {A. Voronkov},
 booktitle    = {Logic Programming},
 series       = {Lecture Notes in Computer Science},
 volume       = {592},
 publisher    = {Springer},
 pages        = {361--380},
 doi          = {10.1007/3-540-55460-2_27},
)
@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},
 pages        = {846--858},
 doi          = {10.1145/3009837.3009894},
)
@book(Prawitz,
 author       = {Dag Prawitz},
 year         = {1965},
 title        = {Natural deduction. A proof-theoretical study},
 publisher    = {Almqvist \& Wiksell},
)
@article(Prior,
 author       = {Arthur N. Prior},
 year         = {1960},
 title        = {The runabout inference-ticket},
 journal      = {Analysis},
 volume       = {21},
 number       = {2},
 pages        = {38--39},
 doi          = {10.1093/analys/21.2.38},
)
@article(Read04,
 author       = {Stephen Read},
 year         = {2004},
 title        = {Identity and harmony},
 journal      = {Analysis},
 volume       = {64},
 number       = {2},
 pages        = {113--119},
 doi          = {10.1093/analys/64.2.113},
)
@article(Read10,
 author       = {Stephen Read},
 year         = {2010},
 title        = {General-elimination harmony and the meaning of the logical constants},
 journal      = {Journal of Philosophical Logic},
 volume       = {39},
 pages        = {557--576},
 doi          = {10.1007/s10992-010-9133-7},
)
@unpublished(Read,
 author       = {Stephen Read},
 year         = {2014},
 title        = {Identity and harmony revisited},
 url          = {https://www.st-andrews.ac.uk/~slr/identity_revisited.pdf},
 note         = {Informal publication},
)
@inproceedings(SabryValironVizzottoF18,
 author       = {Amr Sabry and Beno\^it Valiron and Juliana Kaizer Vizzotto},
 year         = {2018},
 title        = {From Symmetric Pattern-Matching to Quantum Control},
 editor       = {Christel Baier and Dal Lago, Ugo},
 booktitle    = {Foundations of Software Science and Computation Structures (FoSSaCS 2018)},
 series       = {Lecture Notes in Computer Science},
 volume       = {10803},
 publisher    = {Springer},
 pages        = {348--364},
 doi          = {10.1007/978-3-319-89366-2_19},
)
@inproceedings(SandersZulianiMPC00,
 author       = {Jeff W. Sanders and Paolo Zuliani},
 year         = {2000},
 title        = {Quantum programming},
 editor       = {Roland Backhouse and Jos\'e Nuno Oliveira},
 booktitle    = {Mathematics of Program Construction (MPC 2000)},
 series       = {Lecture Notes in Computer Science},
 volume       = {1837},
 publisher    = {Springer},
 pages        = {80--99},
 doi          = {10.1007/10722010_6},
)
@article(SchroederHeister,
 author       = {Schroeder-Heister, Peter},
 year         = {1984},
 title        = {A natural extension of {N}atural deduction},
 journal      = {The Journal of Symbolic Logic},
 volume       = {49},
 number       = {4},
 pages        = {1284--1300},
 doi          = {10.2307/2274279},
)
@article(SelingerMSCS04,
 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(SelingerValironMSCS06,
 author       = {Peter Selinger and Beno\IeC{\^\i}t Valiron},
 year         = {2006},
 title        = {A lambda calculus for quantum computation with classical control},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {16},
 number       = {3},
 pages        = {527--552},
 doi          = {10.1017/S0960129506005238},
)
@book(SorensenUrzyczyn98,
 author       = {S{\o}rensen, Morten Heine and Pawe{\l} Urzyczyn},
 year         = {1998},
 title        = {Lectures on the Curry-Howard isomorphism},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {149},
 publisher    = {Elsevier},
)
@inproceedings(SotilleDiazcaroMartinezlopezIFL20,
 author       = {Cristian Sottile and D\'iaz-Caro, Alejandro and Mart\'inez L\'opez, Pablo E.},
 year         = {2020},
 title        = {Polymorphic System I},
 booktitle    = {Proceedings of the 32nd Symposium on the Implementation and Application of Functional Programming Languages (IFL 2020)},
 series       = {ICPS Proceedings},
 publisher    = {ACM},
 pages        = {127--137},
 doi          = {10.1145/3462172.3462198},
)
@misc(Qsharp,
 author       = {Microsoft Quantum Team},
 year         = {2017},
 title        = {The Q$\sharp$ programming language},
 url          = {{https://docs.microsoft.com/en-us/quantum/quantum-qr-intro?view=qsharp-preview}},
)
@book(Vonoosten08,
 author       = {{van Oosten}, Jaap},
 year         = {2008},
 title        = {Realizability. An introduction to its categorical side},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {152},
 publisher    = {Elsevier},
)
@article(WoottersZurekNATURE82,
 author       = {William K. Wootters and Wojciech H. Zurek},
 year         = {1982},
 title        = {A single quantum cannot be cloned},
 journal      = {Nature},
 volume       = {299},
 pages        = {802--803},
 doi          = {10.1038/299802a0},
)
@book(FOQ,
 author       = {Mingsheng Ying},
 year         = {2016},
 title        = {Foundations of Quantum Programming},
 publisher    = {Elsevier},
)