Quantization of a classical system (e.g. the case of a billiard) 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?    
 A: There have been many attempts to develop a mathematical theory of quantisation, a functor that produces a quantum system for a given classical (Hamiltonian) system. Ideally, one would like to replace classical observables (functions on phase space) by quantum observables (operators on a Hilbert space) such that the commutator bracket of the quantum observable agrees, to first order in the Planck constant, with the Poisson bracket of the corresponding classical observables. Such a functor doesn't exist, there are various theorems that show that in general this is not possible.
See also
http://en.wikipedia.org/wiki/Geometric_quantization
http://arxiv.org/abs/dg-ga/9703010
http://arxiv.org/abs/quant-ph/0601176
A: Quantization is not a functor.
A: As to the bulk of your question, which I take to be a reference request for mathematical accounts of quantum mechanics, I am partial to the book Quantum Mechanics for Mathematicians by L. Takhtajan.
Be sure to look over the MathOverflow thread Where does a math person go to learn quantum mechanics?, as it contains many good references.
A: Let me add some comments. 
I think the question has many faces: 1)  general principles of correspondence classical to quantum world 2)  quite a concrete question about boundary conditions for quantization of billiards.
About (1) I have written something in Quantum mechanics basics 
I can add more, but not sure it is appropriate...
About (2), let me add some comments, it is not full answer, but may be still of some use.
So Joel asks " But I am not sure why the wave function should be defined on R^2 instead of just on B, and even while it should be continuous." 
Yes, I think from physical point of view it should be defined on R^2 and should be continuous, let me explain some arguments which come to my mind.
How can you confine a particle to restricted billiard region "B" in practice ? What physical experiment you keep in mind ? 
The answer is the following - let us create a potential barrier with very high energy  U(x) = U_0  - outside "B" and U(x) = 0 inside "B". 
Well, actually I think such discontinuous potential barrier is not practical, but we can smooth as much as we want.
Classical particle with energy < U_0 cannot go outside the barrier, but quantum particle
can make tunneling inside barrier with exponentially decaying wave function.
Now we just want to consider the limit U_0 -> infinity. 
That would correspond to confining quantum particle to the region "B", again in practice there are NO infinities, so always small probability for particle to be  outside region B,
but as mathematical abstraction it is Okay to take U_0 = inf.
So now we come to  mathematically  well-formulated questions :
Consider smooth potentials U_n(x) which approximate U(x), where U(x) =inf in R^2\B and U(x) = 0, inside B.  Consider  the wave functions Psi(x) which is solution of the corresponding problem (Laplace + U_n(x) ) \Psi_n(x) = \Lambda Psi_n(x)
0) Is it true the limit \Psi (x) does not depend on approximating sequence U_n(x) ?
1) Is it true that limit Psi_n (x) is continuouos ?  
2) Is it true that Psi_n(x) = 0 outside B (including the boundary) ?
I hope the answer is YES, on both questions, but I am not sure I know the arguments. 
It is better to start with these question on R^1 not R^2 - this is done in any quantum mechanics textbook, I am sorry I a little forget the details.
A: Joël asked in a comment that amplified on the original question: "What is not clear to me is how this hypothesis get translated in the quantum setting... I was told that the corresponding quantum system is the space V of function on B vanishing on δB, and the Hamiltonian is the Laplacian. But how does that translate the hypothesis about bouncing? If we assume a weird bouncing where the the inward angle is said twice the outward angle, what would be the attached quantum system?"
A basic requirement for any method of quantization is that it should recover the classical behavior in the limit $h\rightarrow0$. As a first example, let's take the standard classical billiard-ball system, with equal angles of incidence and reflection $\theta_r=\theta_i$, and do our quantization using the path integral method. In the limit $h\rightarrow0$, you get complete interference for all paths except for the one of extremal length, which is the one that has equal angles of incidence and reflection.
Now let's consider your system with $\theta_r=\theta_i/2$. The time-evolution of this system doesn't preserve volume in phase space, so by Liouville's theorem it can't be described by a Hamiltonian. Typically a quantization method starts from a Hamiltonian description, so that's a problem. Physically, the rule $\theta_r=\theta_i/2$ lacks time-reversal symmetry, so under quantization, I suppose the wave equation would have to have a first derivative with respect to time in it. I think what this example shows is that quantization methods are like a set of tools that are made to be used for different purposes. Only certain kinds of classical systems have quantized counterparts that are of interest, and each quantization method is a tool that was only designed to be used on certain classes of systems of interest. As another example, the quantization methods used for the electromagnetic field fail when applied to gravitational fields.
Other answers have discussed the fact that quantization is not a turn-key process. To make this more concrete, I think it's helpful to consider the simplest example I know that is of actual physical interest, which is an electron in an externally applied electromagnetic field. There you get the Aharonov-Bohm effect, which is a nontrivial nonclassical effect that would be hard to anticipate.
A: As the non-uniques of a quantization scheme was already brought up, I will add a nice resource which gives a broad overview of different techniques:
Quantization Methods: A Guide for Physicists and Analysts, arXiv:math-ph/0405065
For geometric quantization the standard textbook account is Woodhouse: Geometric Quantization.
A: Apparently you have been told that the Laplacian with homogeneous Dirichlet boundary conditions is the quantization of the classical billard on the unit sphere bundle over $B$. That is not the only possibility. If the Dirichlet conditions are replaced by Neumann (or Robin) boundary conditions, the corresponding classical Hamilton system is the same billard. 
The correspondence between quantum and classical systems typically arises by taking the semi-classical limit which, in a quantum mechanical setting, consists of letting Planck's "constant" tend to zero. Given that quantum mechanics is more fundamental than classical mechanics, why should one even hope to be generally able to go from classical to quantum, or to have a quantization functor? The non-existence of a quantization functor has already been pointed out in an answer, which maybe refers to the Groenewold-van Hove Theorem.
