In the last decade, various models and programming languages for describing quantum computation have been introduced. The semantic foundation of quantum programming languages is being built. In this talk, we will review some recent results on generalizing traditional proof techniques such as coinduction and Hoare logic to reason about quantum programs.