@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},
)