We present a linear logical framework implemented within the Hybrid system. Hybrid is designed to support the use of higher-order abstract syntax 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, which provides infrastructure for reasoning directly about object languages with linear features. We developed this framework in order to address the chal- lenges of reasoning about the type system of a quantum lambda calculus. In particular, we started by considering the Proto-Quipper language, which contains the core of Quipper. Quipper is a new quantum programming lan- guage under active development with a linear type system. We have completed a formal proof of type soundness for Proto-Quipper. Our current work includes extending this work to other properties of Proto-Quipper as well as reason- ing about other quantum programming languages. It also includes reasoning about other object languages with linear features in areas such as meta-theory of low-level abstract machine code, proof theory of focused linear sequent calculi, and modeling biological processes as transition systems and proving properties about them.