  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 Quipper. Quipper is a new quantum programming language
under active development and recently has gained much popularity among the
quantum computing communities. Hybrid is a system that is designed to support
the use of higher-order abstract syntax (HOAS) for representing and reasoning
about formal systems implemented in the Coq Proof Assistant. In this work, we
extend the system with a linear specification logic (SL) in order to reason
about the linear type system of Quipper. To this end, we formalize the
semantics of Proto-Quipper by encoding the typing and evaluation rules in the
SL, and prove type soundness.
