Quantum Typing: A Functional Programming Language for Quantum Computers

Title: Quantum Typing: A Functional Programming Language for Quantum Computers

Research Question: How can we develop a functional programming language that combines classical and quantum features, allowing for efficient and accurate computation on quantum systems?

Methodology: The researchers proposed a higher-order quantum programming language that encodes the control structure of a program as a lambda term, which is implemented classically. The data on which the lambda terms act is quantum and stored on a QRAM quantum device. To handle the unique properties of quantum data, they introduced two distinct basic data types: classical bits and quantum bits. The semantics of the language is operational, with reduction rules that are probabilistic. To manage the manipulation of functions, they developed a typing system based on affine intuitionistic linear logic.

Results: The main result of this preprint is the subject reduction of the language. This means that the validity of a program is linked to the reduction procedure, which induces the choice of typing rules. This allows for the verification of the subject reduction property, ensuring the correctness and efficiency of the programming language.

Implications: The development of this functional programming language for quantum computers has significant implications for the field. It provides a practical and efficient way to write programs that can manipulate both classical and quantum data, potentially leading to new algorithms and applications in quantum computing. The use of affine intuitionistic linear logic in the typing system also contributes to the theoretical foundations of quantum programming languages.

Link to Article: https://arxiv.org/abs/0404056v1 Authors: arXiv ID: 0404056v1