QPCF: higher order languages and quantum circuits

TL;DR

qPCF is a quantum programming language extending PCF with quantum circuits and a co-processor, enabling manipulation of quantum data within a classical framework while maintaining core language properties.

Contribution

It introduces qPCF, a novel higher-order quantum programming language with a dependent type system and formal semantics, bridging classical and quantum programming paradigms.

Findings

Proves Preservation and Progress Theorems for qPCF

Defines syntax, typing rules, and operational semantics

Provides higher-order examples of circuit encoding

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.