Linear dependent types for quantum circuit programming

It is sometimes said that 99% of a quantum programmer's task is constructing and manipulating circuits and only 1% is actually running them. In this talk, I will introduce and demonstrate Proto-Quipper-D, an experimental quantum circuit programming language. Like previous versions of Proto-Quipper, it uses linear types to enforce the no-cloning property. In addition, Proto-Quipper-D features the use of dependent types for describing families of circuits and for type-safe garbage qubit management.