Quantum Computing is a new and upcoming way to utilize Quantum Mechanics for computation. It is easy to introduce bugs while programming quantum computers similar to classical computing. Strong static type systems have prevented a lot of bugs from being introduced in the classical paradigm. There is a similar need for well-designed types in the domain of quantum computing. We introduce Quantum Hoare Types that let programmers reason statically about certain semantic properties of their quantum programs and further allow a limited form of formal verification.