qpv.bib

@techreport{Knill1996,
  author      = {Knill, Emanuel},
  title       = {Conventions for Quantum Pseudocode},
  year        = {1996},
  month       = jun,
  number      = {LA-UR-96-2724},
  abstract    = {A few conventions for thinking about and writing quantum pseudocode are proposed. The conventions can be used for presenting any quantum algorithm down to the lowest level and are consistent with a quantum random access machine (QRAM) model for quantum computing. In principle a formal version of quantum pseudocode could be used in a future extension of a conventional language.},
  doi         = {10.2172/366453},
  institution = {{Los Alamos National Laboratory}}
}

@article{Selinger2004a,
  author    = {Selinger, Peter},
  journal   = {Mathematical Structures in Computer Science},
  title     = {Towards a Quantum Programming Language},
  year      = {2004},
  month     = aug,
  number    = {4},
  pages     = {527--586},
  volume    = {14},
  abstract  = {We propose the design of a programming language for quantum computing. Traditionally, quantum algorithms are frequently expressed at the hardware level, for instance in terms of the quantum circuit model or quantum Turing machines. These approaches do not encourage structured programming or abstractions such as data types. In this paper, we describe the syntax and semantics of a simple quantum programming language with high-level features such as loops, recursive procedures, and structured data types. The language is functional in nature, statically typed, free of run-time errors, and has an interesting denotational semantics in terms of complete partial orders of superoperators.},
  doi       = {10.1017/S0960129504004256},
  url       = {https://www.mathstat.dal.ca/~selinger/papers/papers/qpl.pdf},
  publisher = {{Cambridge University Press}}
}

@inproceedings{Gay2005,
  author        = {Gay, Simon J. and Nagarajan, Rajagopal},
  booktitle     = {Proceedings of the 32nd {{ACM SIGPLAN}}-{{SIGACT}} Symposium on {{Principles}} of Programming Languages},
  title         = {Communicating Quantum Processes},
  year          = {2005},
  address       = {{New York, NY, USA}},
  month         = jan,
  pages         = {145--157},
  publisher     = {{Association for Computing Machinery}},
  series        = {{{POPL}} '05},
  abstract      = {We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and transformation of quantum state; in particular, quantum bits (qubits) can be transmitted from process to process along communication channels. CQP has a static type system which classifies channels, distinguishes between quantum and classical data, and controls the use of quantum state. We formally define the syntax, operational semantics and type system of CQP, prove that the semantics preserves typing, and prove that typing guarantees that each qubit is owned by a unique process within a system. We illustrate CQP by defining models of several quantum communication systems, and outline our plans for using CQP as the foundation for formal analysis and verification of combined quantum and classical systems.},
  doi           = {10.1145/1040305.1040318},
  url           = {http://www.dcs.gla.ac.uk/~simon/publications/CQP-POPL.pdf},
  eprint        = {quant-ph/0409052},
  archiveprefix = {arxiv}
}

@inproceedings{Altenkirch2005,
  author        = {Altenkirch, Thorsten and Grattage, Jonathan},
  abstract      = {We introduce the language QML, a functional language for quantum computations on finite types. Its design is guided by its categorical semantics: QML programs are interpreted by morphisms in the category FQC of finite quantum computations, which provides a constructive semantics of irreversible quantum computations realisable as quantum gates. QML integrates reversible and irreversible quantum computations in one language, using first order strict linear logic to make weakenings explicit. Strict programs are free from decoherence and hence preserve superpositions and entanglement - which is essential for quantum parallelism.},
  booktitle     = {Proceedings of the Twentieth Annual {{IEEE}} Symposium on Logic in Computer Science ({{LICS}} 2005)},
  title         = {A Functional Quantum Programming Language},
  note          = {Introduces QML, see also \cite{Grattage2011}},
  year          = {2005},
  address       = {{Chicago, USA}},
  month         = jun,
  pages         = {249--258},
  publisher     = {{IEEE Computer Society Press}},
  doi           = {10.1109/LICS.2005.1},
  archiveprefix = {arXiv},
  eprint        = {quant-ph/0409065}
}

@inproceedings{Grattage2011,
  title         = {An Overview of QML With a Concrete Implementation in Haskell},
  author        = {Jonathan Grattage},
  year          = {2011},
  month         = feb,
  booktitle     = {Proceedings of the Joint 5th International Workshop on Quantum Physics and Logic and 4th Workshop on Developments in Computational Models (QPL/DCM 2008)},
  series        = {Electronic Notes in Theoretical Computer Science},
  volume        = {270},
  pages         = {165--174},
  doi           = {https://doi.org/10.1016/j.entcs.2011.01.015},
  archiveprefix = {arxiv},
  eprint        = {0806.2735},
  abstract      = {This paper gives an introduction to and overview of the functional quantum programming language QML. The syntax of this language is defined and explained, along with a new QML definition of the quantum teleport algorithm. The categorical operational semantics of QML is also briefly introduced, in the form of annotated quantum circuits. This definition leads to a denotational semantics, given in terms of superoperators. Finally, an implementation in Haskell of the semantics for QML is presented as a compiler. The compiler takes QML programs as input, which are parsed into a Haskell datatype. The output from the compiler is either a quantum circuit (operational), an isometry (pure denotational) or a superoperator (impure denotational). Orthogonality judgements and problems with coproducts in QML are also discussed.},
  note          = {See \cite{Altenkirch2005} for original description of QML}
}

@incollection{Altenkirch2009,
  author    = {Altenkirch, Thorsten and Green, Alexander S.},
  booktitle = {Semantic {{Techniques}} in {{Quantum Computation}}},
  publisher = {{Cambridge University Press}},
  title     = {The {{Quantum IO Monad}}},
  year      = {2009},
  month     = nov,
  address   = {{Cambridge}},
  editor    = {Mackie, Ian and Gay, Simon},
  isbn      = {978-0-521-51374-6},
  pages     = {173--205},
  abstract  = {The quantum IO monad is a purely functional interface to quantum programming implemented as a Haskell library. At the same time it provides a constructive semantics of quantum programming. The QIO monad separates reversible (i.e., unitary) and irreversible (i.e., probabilistic) computations and provides a reversible let operation (ulet), allowing us to use ancillas (auxiliary qubits) in a modular fashion. QIO programs can be simulated either by calculating a probability distribution or by embedding it into the IO monad using the random number generator. As an example we present a complete implementation of Shor's algorithm.},
  doi       = {10.1017/CBO9781139193313.006},
  note      = {Also see \cite{Green2010} for a reimplementation in Agda.},
  url       = {https://www.cs.nott.ac.uk/~psztxa/g5xnsc/chapter.pdf}
}

@phdthesis{Green2010,
  title     = {Towards a Formally Verified Functional Quantum Programming Language},
  author    = {Green, Alexander S.},
  year      = {2010},
  month     = jul,
  school    = {University of Nottingham},
  url       = {http://eprints.nottingham.ac.uk/11457/},
  abstract  = {This thesis looks at the development of a framework for a functional quantum programming language. The framework is first developed in Haskell, looking at how a monadic structure can be used to explicitly deal with the side-effects inherent in the measurement of quantum systems, and goes on to look at how a dependently-typed reimplementation in Agda gives us the basis for a formally verified quantum programming language. The two implementations are not in themselves fully developed quantum programming languages, as they are embedded in their respective parent languages, but are a major step towards the development of a full formally verified, functional quantum programming language. Dubbed the ``Quantum IO Monad'', this framework is designed following a structural approach as given by a categorical model of quantum computation.},
  timestamp = {2021-04-18}
}

@inproceedings{Green2013,
  author        = {Green, Alexander S. and Lumsdaine, Peter LeFanu and Ross, Neil J. and Selinger, Peter and Valiron, Beno{\^i}t},
  booktitle     = {Proceedings of the 34th {{ACM SIGPLAN Conference}} on {{Programming Language Design}} and {{Implementation}}},
  title         = {Quipper: {{A Scalable Quantum Programming Language}}},
  year          = {2013},
  address       = {{New York, NY, USA}},
  month         = jun,
  pages         = {333--342},
  publisher     = {{ACM}},
  series        = {{{PLDI}} '13},
  volume        = {48},
  abstract      = {The field of quantum algorithms is vibrant. Still, there is currently a lack of programming languages for describing quantum computation on a practical scale, i.e., not just at the level of toy problems. We address this issue by introducing Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and can generate quantum gate representations using trillions of gates. It is geared towards a model of computation that uses a classical computer to control a quantum device, but is not dependent on any particular model of quantum hardware. Quipper has proven effective and easy to use, and opens the door towards using formal methods to analyze quantum algorithms.},
  doi           = {10.1145/2491956.2462177},
  isbn          = {978-1-4503-2014-6},
  shorttitle    = {Quipper},
  eprint        = {1304.3390},
  archiveprefix = {arXiv}
}

@inproceedings{Green2013a,
  author        = {Green, Alexander S. and Lumsdaine, Peter LeFanu and Ross, Neil J. and Selinger, Peter and Valiron, Beno{\^i}t},
  booktitle     = {Reversible {{Computation}}},
  title         = {An {{Introduction}} to {{Quantum Programming}} in {{Quipper}}},
  year          = {2013},
  editor        = {Dueck, Gerhard W. and Miller, D. Michael},
  month         = jul,
  pages         = {110--124},
  publisher     = {{Springer Berlin Heidelberg}},
  series        = {Lecture {{Notes}} in {{Computer Science}}},
  volume        = {7948},
  abstract      = {Quipper is a recently developed programming language for expressing quantum computations. This paper gives a brief tutorial introduction to the language, through a demonstration of how to make use of some of its key features. We illustrate many of Quipper's language features by developing a few well known examples of Quantum computation, including quantum teleportation, the quantum Fourier transform, and a quantum circuit for addition.},
  doi           = {10.1007/978-3-642-38986-3_10},
  eprint        = {1304.5485},
  archiveprefix = {arxiv},
  isbn          = {978-3-642-38986-3}
}

@inproceedings{Bichsel2020,
  author     = {Bichsel, Benjamin and Baader, Maximilian and Gehr, Timon and Vechev, Martin},
  booktitle  = {Proceedings of the 41st {{ACM SIGPLAN Conference}} on {{Programming Language Design}} and {{Implementation}}},
  title      = {Silq: A High-Level Quantum Language with Safe Uncomputation and Intuitive Semantics},
  year       = {2020},
  address    = {{New York, NY, USA}},
  month      = jun,
  pages      = {286--300},
  publisher  = {{Association for Computing Machinery}},
  series     = {{{PLDI}} 2020},
  abstract   = {Existing quantum languages force the programmer to work at a low level of abstraction leading to unintuitive and cluttered code. A fundamental reason is that dropping temporary values from the program state requires explicitly applying quantum operations that safely uncompute these values. We present Silq, the first quantum language that addresses this challenge by supporting safe, automatic uncomputation. This enables an intuitive semantics that implicitly drops temporary values, as in classical computation. To ensure physicality of Silq's semantics, its type system leverages novel annotations to reject unphysical programs. Our experimental evaluation demonstrates that Silq programs are not only easier to read and write, but also significantly shorter than equivalent programs in other quantum languages (on average -46\% for Q\#, -38\% for Quipper), while using only half the number of quantum primitives.},
  doi        = {10.1145/3385412.3386007},
  isbn       = {978-1-4503-7613-6},
  shorttitle = {Silq},
  url        = {https://files.sri.inf.ethz.ch/website/papers/pldi20-silq.pdf}
}

@inproceedings{Chareton2021,
  title     = {An Automated Deductive Verification Framework for Circuit-Building Quantum Programs},
  author    = {Chareton, Christophe and Bardin, S{\'e}bastien and Bobot, Fran{\c c}ois and Perrelle, Valentin and Valiron, Beno{\^i}t},
  year      = {2021},
  month     = mar,
  booktitle = {Programming Languages and Systems},
  editor    = {Yoshida, Nobuko},
  publisher = {{Springer International Publishing}},
  address   = {{Cham}},
  pages     = {148--177},
  doi       = {10.1007/978-3-030-72019-3_6},
  abstract  = {While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor's integer factoring, quantum phase estimation (QPE) and Grover's search.},
  note      = {See extended version~\cite{Chareton2020} for additional technical material.}
}

@misc{Chareton2020,
  title         = {A {{Deductive Verification Framework}} for {{Circuit}}-Building {{Quantum Programs}}},
  author        = {Chareton, Christophe and Bardin, S{\'e}bastien and Bobot, Fran{\c c}ois and Perrelle, Valentin and Valiron, Beno{\^i}t},
  year          = {2020},
  month         = jul,
  crossref      = {Chareton2021},
  archiveprefix = {arxiv},
  eprint        = {2003.05841},
  abstract      = {While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Early attempts either suffer from the lack of automation or parametrized reasoning, or target high-level abstract algorithm description languages far from the current de facto consensus of circuit-building quantum programming languages. As a consequence, no significant quantum algorithm implementation has been currently verified in a scale-invariant manner. We propose Qbricks, the first formal verification environment for circuit-building quantum programs, featuring clear separation between code and proof, parametric specifications and proofs, high degree of proof automation and allowing to encode quantum programs in a natural way, i.e. close to textbook style. Qbricks builds on best practice of formal verification for the classical case and tailor them to the quantum case: we bring a new domain-specific circuit-building language for quantum programs, namely Qbricks-DSL, together with a new logical specification language Qbricks-Spec and a dedicated Hoare-style deductive verification rule named Hybrid Quantum Hoare Logic. Especially, we introduce and intensively build upon HOPS, a higher-order extension of the recent path-sum symbolic representation, used for both specification and automation. To illustrate the opportunity of Qbricks, we implement the first verified parametric implementations of several famous and non-trivial quantum algorithms, including the quantum part of Shor integer factoring (Order Finding - Shor-OF), quantum phase estimation (QPE) - a basic building block of many quantum algorithms, and Grover search. These breakthroughs were amply facilitated by the specification and automated deduction principles introduced within Qbricks.},
  note          = {Extended version of \cite{Chareton2021}}
}

@article{Hietala2021,
  author   = {Hietala, Kesha and Rand, Robert and Hung, Shih-Han and Wu, Xiaodi and Hicks, Michael},
  journal  = {Proceedings of the ACM on Programming Languages},
  title    = {A Verified Optimizer for {{Quantum}} Circuits},
  year     = {2021},
  month    = jan,
  number   = {POPL},
  pages    = {37:1--37:29},
  volume   = {5},
  abstract = {We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.},
  doi      = {10.1145/3434318}
}

@incollection{Baez2010,
  author        = {Baez, J. and Stay, M.},
  booktitle     = {New Structures for Physics},
  publisher     = {{Springer Berlin Heidelberg}},
  title         = {Physics, Topology, Logic and Computation: {{A}} Rosetta Stone},
  year          = {2010},
  month         = jul,
  address       = {{Berlin, Heidelberg}},
  editor        = {Coecke, Bob},
  isbn          = {978-3-642-12821-9},
  pages         = {95--172},
  abstract      = {In physics, Feynman diagrams are used to reason about quantum processes. In the 1980s, it became clear that underlying these diagrams is a powerful analogy between quantum physics and topology. Namely, a linear operator behaves very much like a ``cobordism'': a manifold representing spacetime, going between two manifolds representing space. This led to a burst of work on topological quantum field theory and ``quantum topology''. But this was just the beginning: similar diagrams can be used to reason about logic, where they represent proofs, and computation, where they represent programs. With the rise of interest in quantum cryptography and quantum computation, it became clear that there is extensive network of analogies between physics, topology, logic and computation. In this expository paper, we make some of these analogies precise using the concept of ``closed symmetric monoidal category''. We assume no prior knowledge of category theory, proof theory or computer science.},
  doi           = {10.1007/978-3-642-12821-9_2},
  archiveprefix = {arxiv},
  eprint        = {0903.0340}
}

@misc{Paykin2019,
  author        = {Paykin, Jennifer and Zdancewic, Steve},
  note          = {Talk at QPL '19},
  title         = {A {{HoTT Quantum Equational Theory}} ({{Extended Version}})},
  month         = apr,
  year          = {2019},
  abstract      = {This paper presents an equational theory for the QRAM model of quantum computation, formulated as an embedded language inside of homotopy type theory. The embedded language approach is highly expressive, and reflects the style of state-of-the art quantum languages like Quipper and QWIRE. The embedding takes advantage of features of homotopy type theory to encode unitary transformations as higher inductive paths, simplifying the presentation of an equational theory. We prove that this equational theory is sound and complete with respect to established models of quantum computation.},
  eprint        = {1904.04371},
  archiveprefix = {arxiv}
}

@inproceedings{Unruh2019,
  title         = {Quantum {{Hoare Logic}} with {{Ghost Variables}}},
  author        = {Unruh, Dominique},
  year          = {2019},
  month         = jun,
  booktitle     = {2019 34th {{Annual ACM}}/{{IEEE Symposium}} on {{Logic}} in {{Computer Science}}},
  series        = {{{LICS}} '19},
  pages         = {1--13},
  doi           = {10.1109/LICS.2019.8785779},
  archiveprefix = {arxiv},
  eprint        = {1902.00325},
  abstract      = {Quantum Hoare logic allows us to reason about quantum programs. We present an extension of quantum Hoare logic that introduces ``ghost variables'' to extend the expressive power of pre-/postconditions. Ghost variables are variables that do not actually occur in the program and are allowed to have arbitrary quantum states (in a sense, they are existentially quantified), and be entangled with program variables. Ghost variables allow us to express properties such as the distribution of a program variable or the fact that a variable has classical content. And as a case study, we show how quantum Hoare logic with ghost variables can be used to prove the security of the quantum one-time pad.}
}