Peng, YuxiangQuantum computing promises to revolutionize solutions to valuable computational problems like factorization and quantum system simulation. Harnessing the power of quantum computers in real life cannot happen without a supportive software stack. This thesis studies the fundamental problems appearing in the software for quantum computing to shed light on shaping software that controls quantum computing devices in the near term and long future. First, we consider the software for Hamiltonian-oriented quantum computing (HOQC). We discuss our new software framework, SimuQ, for programming quantum Hamiltonian simulation on analog quantum simulators (AQS). To characterize the capability of AQSs, we introduce new abstractions named abstract analog instruction sets (AAIS), which enable us to design several domain-specific languages and a novel compiler. SimuQ reduces knowledge barriers for the study of HOQC because front-end users can easily program Hamiltonian systems and simulate their dynamics on AQSs. We then demonstrate how SimuQ inspires new algorithm design and hardware improvements, and extend our view to the full-stack software support of quantum applications via HOQC. Second, we study the software for circuit-oriented quantum computing (COQC). Many prototypes of quantum programming languages have been proposed in recent years based on quantum circuits, while how to debug programs written in these languages remains a critical challenge. Formal methods, a mature area in programming language research, provide a new perspective in guaranteeing the correctness of quantum programs, and we adapt several formal verification techniques to accommodate the nature of quantum programs. In compilers for quantum while programs, rewrite rules need to preserve the semantics of the programs. We connect non-idempotent Kleene algebra with quantum program semantics and propose an equivalence-proving system with algebraic expression derivation. Besides, deductive program verification can also be leveraged on quantum programs to ensure the semantics correctness. To this end, we formally certify an end-to-end implementation of Shor's algorithm, justifying the feasibility of deductive verification for quantum programs.enDissertationComputer science