QPCF: Higher-Order Languages and Quantum Circuits

Stanley Gudder

Luca Paolini, Mauro Piccolo, Margherita Zorzi

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.

Samson Abramsky, Radha Jagadeesan

Many mainstream quantum programming languages confine higher-order structure to a classical host while restricting the quantum layer to first-order operations on qubits. This paper presents Granthi, a purely unitary higher-order quantum programming language built on three design commitments: quantum programs are first-class values that may be passed, returned, and coherently composed; additive structure is tag-preserving routing rather than observational branching, so control may remain in superposition; and programmer-facing finite label types with staged reversible-operation bindings provide domain-level control spaces without exposing tag management. These bindings are eliminated by elaboration before Source typing. Granthi deterministically normalizes each Source program to a canonical wiring form. Every well-typed Source program, including a term of function type, has a unitary boundary interpretation. Under backend correctness (BC), the reference compiler produces a unitary circuit realizing that interpretation. Granthi's currently supported executable fragment is implemented end-to-end: an OCaml DSL elaborates surface programs through a higher-order Core IR to executable quantum circuits via pytket. The language directly supports the pure-unitary quantum switch for explicitly supplied operations; closed instances compile to static circuits. It also supports interference on control-flow history and structured finite control, all within the purely unitary fragment

Margherita Zorzi

In the last 20 years, several approaches to quantum programming have been introduced. In this survey, we focus on the QRAM (Quantum Random Access Machine) architectural model. We explore the twofold perspective (theoretical and concrete) of the approach and we list the main problems one has to face in quantum language design. Moreover, we propose an overview of some interesting languages and open-source platforms for quantum programming currently available. We also provide the higher-order encoding in the functional languages qPCF and IQu of the well known Deutsch-Jozsa and Simon’s algorithms.

María Luisa Dalla Chiara, Roberto Giuntini, Roberto Leporini +1 more

Kathleen Barsse, Romain Péchoux, Simon Perdrix

Processes with indefinite causal orders (ICOs), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In both cases, they do not realize the full computational power of ICOs. We introduce a higher-order quantum functional language that supports general quantum computation, not merely the permutation of channels, and whose linear type system allows quantum control to be well-defined beyond the unitary case, on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics by means of completely positive maps. With linearity as the only constraint, some well-typed terms would denote unphysical maps. We therefore impose a typing discipline that goes beyond linearity, and interpret programs in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. Last but not least, we show that this language is well-designed enough to be extended to the nonlinear setting with recursion.