# A lambda calculus for density matrices with classical and probabilistic controls

## TL;DR

This paper introduces two quantum lambda calculi using density matrices, enabling formal reasoning about quantum data and mixed states with classical and probabilistic controls.

## Contribution

It presents two novel quantum lambda calculi, $
ho$ and $
ho^ullet$, for modeling quantum data and mixed states within a formal lambda calculus framework.

## Key findings

- Provides formal semantics for density matrix-based quantum programs
- Defines two calculi capturing classical control and mixed quantum states
- Lays groundwork for reasoning about quantum algorithms in lambda calculus

## Abstract

In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, $\lambda_\rho$, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, $\lambda_\rho^\circ$, take advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach.