As quantum computers are developed, it becomes important to ask about the programming languages for quantum algorithms. At the same time, the hardness of simulation makes it hard to debug quantum programs. One way to solve this problem is to verify quantum programs prior to its execution. In this poster, we propose a quantum circuit language expanded from Proto-Quipper by adding measurement. The operational semantics of the language can be used to specify and prove properties of quantum programs.