QPCF: higher-order languages and quantum circuits
From MaRDI portal
Publication:2331073
Abstract: qPCF is a paradigmatic quantum programming language that ex- tends PCF with quantum circuits and a quantum co-processor. Quantum circuits are treated as classical data that can be duplicated and manipulated in flexible ways by means of a dependent type system. The co-processor is essentially a standard QRAM device, albeit we avoid to store permanently quantum states in between two co-processor's calls. Despite its quantum features, qPCF retains the classic programming approach of PCF. We introduce qPCF syntax, typing rules, and its operational semantics. We prove fundamental properties of the system, such as Preservation and Progress Theorems. Moreover, we provide some higher-order examples of circuit encoding.
Recommendations
Cites work
- \textsc{qPCF}: a language for quantum circuit computations
- A branching distributed temporal logic for reasoning about entanglement-free quantum state transformations
- A categorical model for a quantum circuit description language (extended abstract)
- A class of reversible primitive recursive functions
- A lambda calculus for quantum computation with classical control
- A stable programming language
- A System F accounting for scalars
- Algorithmic probabilistic game semantics. Playing games with automata
- An algebra of pure quantum programming
- An introduction to quantum programming in Quipper
- An overview of QML with a concrete implementation in Haskell
- Applying quantitative semantics to higher-order quantum computing
- Confluence results for a quantum lambda calculus with measurements
- Constructive quantum scaling of unitary matrices
- Foundations of Software Science and Computation Structures
- Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases
- Full abstraction for probabilistic PCF
- scientific article; zbMATH DE number 1579275 (Why is no real title available?)
- scientific article; zbMATH DE number 5076264 (Why is no real title available?)
- scientific article; zbMATH DE number 5708038 (Why is no real title available?)
- scientific article; zbMATH DE number 1263427 (Why is no real title available?)
- scientific article; zbMATH DE number 1776257 (Why is no real title available?)
- scientific article; zbMATH DE number 1406118 (Why is no real title available?)
- Indexed types
- LCF considered as a programming language
- Lectures on Quantum Theory
- Linear-algebraic λ-calculus: higher-order, encodings, and confluence.
- Logic for Programming, Artificial Intelligence, and Reasoning
- Measurements and confluence in quantum lambda calculi with explicit qubits
- Modal deduction systems for quantum state transformations
- Non-determinism, non-termination and the strong normalization of System T
- On a measurement-free quantum lambda calculus with classical control
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- On quantum lambda calculi: a foundational perspective
- On the reification of semantic linearity
- Perfect computational equivalence between quantum Turing machines and finitely generated uniform quantum circuit families
- Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
- Probabilistic coherence spaces as a model of higher-order probabilistic computation
- Probabilistic operational semantics for the lambda calculus
- QIP = PSPACE
- Quantum computation and quantum information. 10th anniversary edition
- Quantum computation by measurement and quantum memory
- Quantum computation: from a programmer's perspective
- Quantum Computing
- Quantum implicit computational complexity
- Quantum programming made easy
- Quantum State Transformations and Branching Distributed Temporal Logic
- Quantum theory, the Church–Turing principle and the universal quantum computer
- QWIRE: a core language for quantum circuits
- Semantics of higher-order quantum computation via geometry of interaction
- Semi-decidability of may, must and probabilistic testing in a higher-type setting
- The algebraic lambda calculus
- The computer as a physical system: a microscopic quantum mechanical Hamiltonian model of computers as represented by Turing machines
- The measurement calculus
- The physical implementation of quantum computation.
- Towards a quantum programming language
- Types and programing languages
- Wave-style token machines and quantum lambda calculi
Cited in
(10)- An automated deductive verification framework for circuit-building quantum programs
- \textsc{qPCF}: a language for quantum circuit computations
- qPCF
- A categorical model for a quantum circuit description language (extended abstract)
- scientific article; zbMATH DE number 7364199 (Why is no real title available?)
- Quantum programming made easy
- Sized Types for Low-Level Quantum Metaprogramming
- QWIRE: a core language for quantum circuits
- Quantum symbolic execution
- A rewriting theory for quantum -calculus
This page was built for publication: QPCF: higher-order languages and quantum circuits
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2331073)
