QPEL: Quantum Program and Effect Language

TL;DR

QPEL is a formal language designed for describing quantum programs and their properties, with semantics grounded in category theory, enabling rigorous reasoning about quantum effects.

Contribution

This work introduces QPEL, a novel language for quantum programs and effects, with a categorical semantics framework and proven soundness and completeness.

Findings

Semantic framework based on state-and-effect triangles

Soundness and completeness of the language

Applicability to various categorical models

Abstract

We present the syntax and rules of deduction of QPEL (Quantum Program and Effect Language), a language for describing both quantum programs, and properties of quantum programs - effects on the appropriate Hilbert space. We show how semantics may be given in terms of state-and-effect triangles, a categorical setting that allows semantics in terms of Hilbert spaces, C*-algebras, and other categories. We prove soundness and completeness results that show the derivable judgements are exactly those provable in all state-and-effect triangles.