Classic papers
Conventions for Quantum Pseudocode
Knill proposes reusable conventions for describing quantum algorithms in a QRAM model.
Quantum Programming
Sanders and Zuliani apply guarded commands and probabilistic-programming ideas to quantum program semantics.
Towards a Quantum Programming Language
Selinger proposes QPL, combining quantum data, classical control, typing, and superoperator semantics.
A Lambda Calculus for Quantum Computation
van Tonder develops a quantum lambda calculus related to linear logic, with an equational proof system and a quantum-Turing-machine correspondence.
A Categorical Semantics of Quantum Protocols
Abramsky and Coecke give a compositional semantics for quantum protocols using compact closed categories with biproducts.
A Functional Quantum Programming Language
Altenkirch and Grattage propose QML, combining finite types, linear logic, and categorical semantics for reversible and irreversible quantum computation.
A Lambda Calculus for Quantum Computation with Classical Control
Selinger and Valiron use an affine linear lambda calculus to express quantum data, classical control, and safety properties.
Communicating Quantum Processes
Gay and Nagarajan introduce CQP, combining pi-calculus communication, quantum operations, typing, and unique ownership.
Quantum Weakest Preconditions
D'Hondt and Panangaden develop predicate transformers and weakest-precondition semantics for quantum computation.
Reasoning About Imperative Quantum Programs
Chadha, Mateus, and Sernadas study logical reasoning for imperative quantum programs and its connection to probabilistic-program methods.