quantum algorithms:
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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
QML is a functional quantum programming language.
Original description:
Thorsten Altenkirch, Jonathan Grattage, A functional quantum programming language, Logic in Computer Science (2005) 249-258 [arXiv:quant-ph/0409065, doi:10.1109/LICS.2005.1, pdf]
Jonathan Grattage, A functional quantum programming language, PhD thesis, Nottingham (2006) [eprints:10250, pdf]
Alexander Green, Towards a formally verified functional quantum programming language (2010) [eprints:11457]
(emphasis on formal software verification)
and with emphasis on the quantum IO monad:
Review:
Jonathan Grattage, An overview of QML with a concrete implementation in Haskell, Quantum Physics and Logic 2008 [arXiv:0806.2735]
Jonathan Grattage with Thorsten Altenkirch, Compiling a functional quantum programming language (talk slides) [pdf, pdf]
Last revised on September 22, 2023 at 10:12:44. See the history of this page for a list of all contributions to it.