Peter Selinger, Towards a quantum programming language, Mathematical Structures in Computer Science 14 4 (2004) 527–586 [doi:10.1017/S0960129504004256, pdf, web]

and specifically the quantum lambda-calculus of:

Benoît Valiron, A functional programming language for quantum computation with classical control, MSc thesis, University of Ottawa (2004) [doi:10.20381/ruor-18372, pdf]
Peter Selinger, Benoît Valiron, A lambda calculus for quantum computation with classical control, Proc. of TLCA 2005 [arXiv:cs/0404056, doi:10.1007/11417170_26]
Peter Selinger, Benoît Valiron, Quantum Lambda Calculus, in: Semantic Techniques in Quantum Computation, Cambridge University Press (2009) 135-172 [doi:10.1017/CBO9781139193313.005, pdf]

[Selinger (2016):] When the QPL workshop series was first founded, it was called “Quantum Programming Languages”. One year I wasn’t participating, and while I wasn’t looking they changed the name to “Quantum Physics and Logic” — same acronym!

Back in those days in the early 21st century we were actually trying to do programming languages for quantum computing [[Selinger & Valiron 2004]], but the sad thing is: In those days nobody really cared. [...][...]

Now it’s 15 years later and several of these parameters have changed: There has been a renewed interest, from government agencies and also from companies who are actually building quantum computers. [...][...].

So now people are working on quantum programming languages again.

On categorical semantics on von Neumann algebras:

Kenta Cho, Semantics for a Quantum Programming Language by Operator Algebras, EPTCS 172 (2014) 165-190 [arXiv:1412.8545, doi:10.4204/EPTCS.172.12]

Quipper as such

Exposition of the general idea of quantum programming languages for classically controlled quantum computation with an eye towards the Quipper-language:

Benoît Valiron, Neil J. Ross, Peter Selinger, D. Scott Alexander, Jonathan M. Smith, Programming the quantum future, Communications of the ACM 58 8 (2015) 52–61 [doi:10.1145/2699415, pdf, web, promo vid:YT]

Original articles on Quipper:

Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: A Scalable Quantum Programming Language, ACM SIGPLAN Notices 48 6 (2013) 333-342 [arXiv:1304.3390, doi:10.1145/2499370.2462177]
Jonathan Smith, Neil Ross, Peter Selinger, Benoît Valiron, Quipper: Concrete Resource Estimation in Quantum Algorithms, QAPL 2014 (arXiv:1412.0625)
Neil J. Ross, Chapters 8-9 in: Algebraic and Logical Methods in Quantum Computation, Ph.D. thesis, Dalhousie University (2015) [arXiv:1510.02198]

(introducing Proto-Quipper)

Introduction and review:

Alexander Green, Peter LeFanu Lumsdaine, Neil Ross, Peter Selinger, Benoît Valiron, An Introduction to Quantum Programming in Quipper, Lecture Notes in Computer Science 7948 Springer (2013) 110-124 [arXiv:1304.5485, doi:10.1007/978-3-642-38986-3_10]
Peter Selinger, Introduction to Quipper, talk at QPL2016 (2016) [video]

Example algorithms:

Safat Siddiqui, Mohammed Jahirul Islam, Omar Shehab, Five Quantum Algorithms Using Quipper [arXiv:1406.4481]

On quantum software verification for/with Quipper:

Linda Anticoli, Carla Piazza, Leonardo Taglialegne, Paolo Zuliani, Towards Quantum Programs Verification: From Quipper Circuits to QPMC, In: Devitt S., Lanese I. (eds) Reversible Computation. RC 2016. Lecture Notes in Computer Science, vol 9720. Springer, Cham (doi:10.1007/978-3-319-40578-0_16)

Dependent linear types and categorical semantics

Discussion of some dependent linear type theory and categorical semantics for (proto-)Quipper:

Francisco Rios, Peter Selinger, A Categorical Model for a Quantum Circuit Description Language, EPTCS 266 (2018) 164-178 [arXiv:1706.02630, doi:10.4204/EPTCS.266.11]
Peng Fu, Kohei Kishida, Neil Ross, Peter Selinger, A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed Proto-Quipper, in I. Lanese, M. Rawski (eds.) Reversible Computation RC 2020. Lecture Notes in Computer Science, vol 12227 [arXiv:2005.08396, doi:10.1007/978-3-030-52482-1_9]
Peng Fu, Kohei Kishida, Peter Selinger, Linear Dependent Type Theory for Quantum Programming Languages, LICS ‘20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer ScienceJuly 2020 Pages 440–453 (arXiv:2004.13472, doi:10.1145/3373718.3394765, pdf, video)
Francisco Rios, On a Categorically Sound Quantum Programming Language for Circuit Description, Dalhousie University (2021) [hdl:10222/80771]
Dongho Lee, Formal Methods for Quantum Programming Languages, Paris Saclay (Dec 2022) [hal:tel-03895847]

Semantics on quantum CPOs (via quantum relations on quantum sets) for interpreting Quipper with term recursion:

Andre Kornell, Bert Lindenhovius, Michael Mislove, Quantum CPOs, EPTCS 340 (2021) 174-187 [arXiv:2109.02196, doi:10.4204/EPTCS.340.9]

Dynamic lifting

The issue of “dynamic lifting” (of “bits” resulting from quantum measurement back into the “context”):

brief mentioning on GLRSV13, p. 5
Robert Rand, Formally Verified Quantum Programming, UPenn (2018) [ediss:3175]
Dongho Lee, Sebastien Bardin, Valentin Perrelle, Benoît Valiron, Formalization of a Programming Language for Quantum Circuits with Measurement and Classical Control, talk at Journées Informatique Quantique 2019 (Nov 2019) [pdf, pdf]
Dongho Lee, Valentin Perrelle, Benoît Valiron, Zhaowei Xu, Concrete Categorical Model of a Quantum Circuit Description Language with Measurement, Leibniz International Proceedings in Informatics 213 (2021) 51:1-51:20 [arXiv:2110.02691, doi:10.4230/LIPIcs.FSTTCS.2021.51]
Andrea Colledan, Ugo Dal Lago, On Dynamic Lifting and Effect Typing in Circuit Description Languages [arXiv:2202.07636]
Andrea Colledan, Ugo Dal Lago, On Dynamic Lifting and Effect Typing in Circuit Description Languages, talk at TYPES Workshop, Nantes (2022) [pdf, pdf]
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, A biset-enriched categorical model for Proto-Quipper with dynamic lifting, in proceedings of Quantum Physics and Logic 2022 [arXiv:2204.13039]
Peng Fu, Kohei Kishida, Neil J. Ross, Peter Selinger, Proto-Quipper with dynamic lifting, in proceedings of Quantum Physics and Logic 2022 [arXiv:2204.13041]
Dongho Lee, Formal Methods for Quantum Programming Languages, Paris Saclay (Dec 2022) [hal:tel-03895847]
Frank (Peng) Fu, Proto-Quipper with Dynamic Lifting, talk at CQTS (23 Oct 2023) [video:YT]

Last revised on April 24, 2024 at 05:47:49. See the history of this page for a list of all contributions to it.