  Quipper is a domain-specific programming language for the description of
quantum circuits. Because it is implemented as an embedded language in Haskell,
Quipper is a very practical functional language. However, for the same reason,
it lacks a formal semantics and it is limited by Haskell's type system. In
particular, because Haskell lacks linear types, it is easy to write Quipper
programs that violate the non-cloning property of quantum states. In order to
formalize relevant fragments of Quipper in a type-safe way, the Proto-Quipper
family of research languages has been introduced over the last years. In this
paper we first review Proto-Quipper-M, an instance of the Proto-Quipper family
based on a categorical model for quantum circuits, which features a linear type
system that guarantees that the non-cloning property holds at compile time. We
then derive a tentative small-step operational semantics from the big-step
semantics of Proto-Quipper-M and we prove that the two are equivalent. After
proving subject reduction and progress results for the tentative semantics, we
build upon it to obtain a truly small-step semantics in the style of an
abstract machine, which we eventually prove to be equivalent to the original
semantics.
