The usual model of quantum computation describes operators by how they act on multi-qubit quantum states. However, in some situations quantum operators $U$ are better understood by their conjugation actions $P \mapsto U P U^\dag$ on the multi-qubit Pauli group. This is often the case for Clifford operators for example, which are defined as those unitaries whose conjugation action stabilizes the Pauli group.

In this work we explore what it looks like to to program projective Cliffords (up to phase) directly in terms of their conjugation action on Paulis, rather than as circuits or by their action on states. We establish a Curry-Howard correspondence in which projective Cliffords are viewed as certain functions between Pauli types. The result is a lambda-calculus called LambdaPC in which well-typed functions correspond exactly the set of projective Cliffords. The type system of LambdaPC consists of two main parts: a linear type system to describe vectors and linear transformations in a vector space; and an orthogonality check based on the symplectic form, which encodes the commutation relations of the Pauli group. In the full paper we prove that every Clifford can be represented as a function in LambdaPC and vice versa, and show that they can be efficiently synthesized into quantum circuits.