References

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