The field of quantum algorithms is vibrant. Nevertheless, there is currently a lack of programming languages for describing and formalizing quantum computation on a practical scale, i.e., not just at the level of toy problems. We address this issue by introducing Quipper, a scalable, expressive, functional, higher-order quantum programming language. Quipper has been used to program a diverse set of non-trivial quantum algorithms, and is able to generate quantum gate representations using trillions of gates.

In this talk, I will present the setting and the current (limited) semantics for quantum computation. I will introduce Quipper and discuss what is currently missing, that is, a linear type system to capture the non-duplicability of quantum data. From there I will present two uses for this type-system: (1) an denotational semantics for all of quantum computation, and (2) resource estimation for quantum algorithms.