coq

Formalization of Metatheory of the Quipper Quantum Programming Language in a Linear Logic

We develop a linear logical framework within the Hybrid system and use it to reason about the type system of a quantum lambda calculus. In particular, we consider a practical version of the calculus called Proto-Quipper, which contains the core of …