There have been already several questions asking for an introduction to quantum mechanics for a mathematician, but this one is slightly different, and more restrictive.

I know (some) quantum mechanics, but I'd like to find a reference which explains, in a way as clear and systematic as possible, how we pass from a classical system (in the hamiltonian formulation, with a phase space $X$, and an Hamiltonian function $H$ on it) to the corresponding quantum system, with an Hilbert space $V$ and an Hamiltonian operator $\hat H$ on it.

If the reference is precise and rigorous mathematically, that's a plus (ideally it would even define a functor $(X,H) \mapsto (V,\hat{H})$ of the adequate categories); if the reference gives a lot of physical intuition, that's also a plus.

I ask this question because I am trying to understand Quantum Unique Ergodicity, in particular
the classical example of Billiard. In this example $B$ is a closed region of the plane with a
smooth boundary, and $X=B \times S^{1}$, the second factor corresponding to the velocity vector. The Hamiltonian in the inside of $X$ corresponds to free motion, but it has to be defined somehow on the boundary so that it corresponds to the ball reflecting on the boundary in the standard way (I am not sure how exactly). Then I am told that the quantic version of this system is a $V$ which is the space of function on $B$ *which vanishes on the boundary*,
and I'd like to understand why, and $\tilde H$ is the laplacian (that I more or less understand). If anyone has an explanation for that example, that would be great.

EDIT: Thanks to all for your five answers. Each of them taught me something valuable, and collectively they taught me I knew much less about Quantum Mechanics than I thought.

SECOND EDIT: Since answers keep arriving, let me add something:
When I said I was "told" that quantization of a Billiard B is the space of functions on B
**vanishing at the boundary**, it is true but I also read it A. Hassel, "What is quantum unique ergodicity?", page 161.
Now that I realize that my question was too vast and too difficult (for me to understand fully the answer).

I'd like to precise it by asking: when people working in Quantum Theory quantize a classical physical system (like in the article quoted above), what specific method do they use? Or are they just math people happy with any quantum system having some analogy with the classical one and leading to a mathematically interesting problem?