constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
quantum algorithms:
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Quipper is a functional quantum programming language, specifically a domain specific programming language for quantum circuits which is embedded into Haskell. As such it is similar to QWIRE.
Quipper landing page:
Quipper has grown out of developments initiated in
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.
Exposition of the general idea of quantum programming languages for classically controlled quantum computation with an eye towards the Quipper
-language:
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:
On quantum software verification for/with Quipper:
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]
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 Liftin 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]
Last revised on September 11, 2023 at 12:36:17. See the history of this page for a list of all contributions to it.