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.
Resources:
Precursor discussion:
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:110-124, Springer, 2013 (arXiv:1304.5485)
Peter Selinger, Introduction to Quipper, talk at QPL2016 (2016) [video]
On quantum software verification for/with Quipper:
Discussion of some dependent linear type theory and categorical semantics for 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]
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 Lifting
and Effect Typing in Circuit Description Languages, talk atTYPES 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 March 14, 2023 at 05:31:06. See the history of this page for a list of all contributions to it.