Qudit Quantum Programming with Projective Cliffords

TL;DR

This paper presents LambdaPC, a new programming language for qudit quantum operations based on projective Cliffords, extending the framework to any dimension and enabling advanced quantum programming and error correction.

Contribution

It introduces LambdaPC, a type system and lambda calculus for projective Cliffords over qudits, generalizing previous qubit-focused approaches and capturing well-formed operations.

Findings

LambdaPC accurately models qudit Clifford operations.

The language supports programming with projective Cliffords across dimensions.

Case study demonstrates application to stabilizer error correcting codes.

Abstract

This paper introduces a novel abstraction for programming quantum operations, specifically projective Cliffords, as functions over the qudit Pauli group. Generalizing the idea behind Pauli tableaux, we introduce a type system and lambda calculus for projective Cliffords called LambdaPC, which captures well-formed Clifford operations via a Curry-Howard correspondence with a particular encoding of the Clifford and Pauli groups. Importantly, the language captures not just qubit operations, but qudit operations for any dimension $d$. Throughout the paper we explore what it means to program with projective Cliffords through a number of examples and a case study focusing on stabilizer error correcting codes.