Quipper is a functional programming language for quantum computing.
Proto-Quipper is a family of languages aiming to provide a formal
foundation for Quipper. In this paper, we extend Proto-Quipper-M with
a construct called \emph{dynamic lifting}, which is present in Quipper. By
virtue of being a circuit description language, Proto-Quipper has two
separate runtimes: circuit generation time and circuit execution
time. Values that are known at circuit generation time are called
\emph{parameters}, and values that are known at circuit execution time
are called \emph{states}. Dynamic lifting is an operation that enables a state,
such as the result of a measurement, to be lifted to a parameter,
where it can influence the generation of the next portion of the
circuit. As a result, dynamic lifting enables Proto-Quipper programs
to interleave classical and quantum computation. We describe the
syntax of a language we call Proto-Quipper-Dyn. Its type system uses a
system of modalities to keep track of the use of dynamic lifting. We
also provide an operational semantics, as well as an abstract
categorical semantics for dynamic lifting based on enriched category
theory. We prove that both the type system and the operational
semantics are sound with respect to our categorical
semantics. Finally, we give some examples of Proto-Quipper-Dyn
programs that make essential use of dynamic lifting.