Equivalence of canonical quantization and path integral quantization
This type of problems is often referred to as constrained mechanical system. It was studied by Dirac, who developed the theory of constrained quantization. This theory was formalized and further developed by Marseden and Weinstein to what is called "Symplectic reduction". A particularly illiminating chapter for finite dimensional systems may be found in Marsden and Ratiu's book: "Introduction to mechanics and symmetry".
When the phase space of a dynamical system is a cotangent bundle, one can use the usual methods of canonical quantization, and the corresponding path integral. However, this formalism does not work in general for nonlinear phase spaces. One important example is when the phase space is defined by a nonlinear surface in a larger linear phase space.
Basically, Given a symmetry of a phase space, one can reduce the problem to a smaller phase space in two stages
- Work on "constant energy surfaces" of the Hamiltonian generating this stymmetry.
- Consider only "invariant observables" on these surfaces.
This procedure reduces by 2 the dimensions of the phase space, and the reduced dimension remains even. One can prove that if the original phase space is symplectic, so will be the reduced phase space.
May be the most simple example is the elimination of the center of mass motion in a two particle system and working in the reduced dynamics.
There is a theorem by Guillemin and Sternberg for certain types of finite dimensional phase spaces which states that quantization commutes with reduction. That is, one can either quantize the original theory and impose the constraints on the quantum Hilbert space to obtain the "physical" states. Or, on can reduce the classical theory, then quantize. In this case the reduced Hilbert space is automatically obtained. The second case is not trivuial because the reduced phase space becomes a non-linear symplectic manifold and in many cases it is not even a manifold (because the group action is not free).
Most of the physics applications treat however field theories which correspond to infinite dimensional phase spaces and there is no counterpart of the Guillemin-Sternberg theorem. (There are works trying to generalize the theorem to some infinite dimensional spaces by N. P. Landsman). But in general, the commutativity of the reduction and quantization is used in the physics literature, even though a formal proof is still lacking. The most known example is the quantization of the moduli space of flat connections in relation to the Chern-Simons theory.
The most known example of constrained dynamics in infinite dimensional spaces is the Yang-Mills theory where the momentum conjugate to $A_0$ vanishes. It should be mentioned that there is an alternative (and equivalent) approach to treat the constraints and perform the Marsden-Weinstein reduction through BRST, and this is the usual way in which the Yang-Mills theory is treated. In this approach, the phase space is extended to a supermanifold instead of being reduced. The advantage of this approach is that the resulting supermanifold is flat and methods of canonical quantization can be used.
In the mentioned case of the scalar field, the phase space may be considered as an infinite numer of copies of $T^{*}\mathbb{R}$. The relation $\Pi = \partial_x \phi$ is the constraint surface. In a naive dimension count of the reduced phase space dimensions one finds that in every space point the 1+1 dimensions the phase space (The field and its conjugate momentum) are fully reduced by the constraint and its symmetry generator. Thus we are left with a "zero-dimensional" theory. I haven't worked out this example, but I am quite sure that if this case is done carefully we would have been left with a finite number of residual parameters. This is a sign that this theory is topological - which can be seen through the quantization of the global coefficient".
Update:
In response to Greg's comments here are further references and details.
The following review article (Aspects of BRST Quantization) by J.W. van Holten explains the BRST quantization of electrdynamics and Yang-Mills theory (Faddeev-Popov theory) as constrained mechanical systems.The article contains other example from (finite dimensioal phase space) quantum mechanics as well.
The following article by Phillial Oh. (Classical and Quantum Mechanics of Non-Abelian Chern-Simons Particles) describes the quantization of a (finite dimensional) mechanical system performing the symplectic reduction directly without using BRST. Here, the reduced spaces are coadjoint orbits (such as flag manifolds or projective spaces). The beautiful geometry of these spaces is very well known and this is the reason why the reduction can be performed here directly. For most of the reduced phase spaces, such an explicit knowledge of the geometry is lacking. In field theory, problems such as quantization of the two dimensional Yang-Mills theory possess such an explicit description, but for higher dimensional I don't know of an explicit treatment (besides BRST).
The following article by Kostant and Sternberg, describes the equivalence between the BRST theory and the direct symplectic reduction.
Now, concerning the path integral. I think that most of the recent physics achievements were obtained by means of the path integral, even if it has some loose points. I can refer you to the following book by Cartier and Cecile DeWitt-Morette, where they treated path integrals on non-flat symplectic manifolds and in addition, they formulated the oscillatory path integral in terms of Poisson processes.
There is a very readable reference by Orlando Alvarez describing the quantization of the global coefficients of topological terms in, Commun. Math. Phys. 100, 279-309 (1985)(Topological Quantization and Cohomology). I think that the Lagrangian given in the question can be treated by the same methods. basically, the quantization of these terms is due to the same physical reason that the product of electric and magnetic charges of magnetic monopoles should be quantized. This is known as the Dirac quantization condition. In the path integral formulation, it follows from the requirement that a gauge transformation should produce a phase shift of multiples of $2\pi$. In geometric quantization, this condition follows from the requirement that the prequantization line bundle should correspond to an integral symplectic form.
Procedures 1 and 2 are equivalent when the action is quadratic in the momentum, and when there is a gauge fixing which produces a unitary quantum field theory. Unitarity is not obvious in the Path integral, as immediately noted by Dirac. It is established either by proving reflection positivity in the path integral directly, or by passing to a canonical description where the unitarity is obvious, because the Hamiltonian is real.
It is important to note that the fact that the quantities in the path integral are not operators is completely insignificant. Their products don't commute, and require careful definition in terms of time order, which is in every way corresponds to the ordering ambiguities in the Hamiltonian formalism. If you want to think of them as operators, you can, they act on the boundary conditions coming in in the same way as Heisenberg operators, because they are just the matrix elements of Heisenberg operators. There is no difference in the properties of the quantities in the path integral formalism and any other formalism, they don't get easier in the path integral.
Feynman-Fourier transform
For Hamiltonians which are not quadratic in the momentum, it is trickier to pass to a path integral, the quantum action is not equal to the classical action. The general prescription to pass to the Feynman description is through the phase-space path integral:
$$ K(x,y) = \int Dx Dp e^{i\int (p\dot{x} - H(p,q))} dt$$
where the term $p\dot{x}$ is to be interpreted as $p_t(x_{t+\epsilon} - x_t)$, that is, $\dot{x}$ is a forward difference, and H(p,q) is "normal ordered", meaning all p terms are commuted to appear first.
Then the Feynman form is given by integrating out the momentum. This cannot be done in closed form in general, so there are many examples of well-behaved Hamiltonians whose Lagrangian description is not closed-form expressible, for example
$$H= p^4 + V(x)$$
and there are converse examples of nice Lagrangians whose Hamiltonian form is not very nice. I will give such an example in a minute. But first, the Feynman transform.
When the Hamiltonian is of the form
$$H =K(p) + V(x)$$
Then the Lagrangian description is expressed entirely in terms of the function K' appearing in this formula:
$$ e^{-K'(v)} = \int e^{-K(p) + i p v} dx$$
That is, the Feynman transform K' is the log of the fourier transform of the exponential of minus the original function. To see that this works is simple, you Wick rotate each integral over p and do the integral formally using K'.
Each exactly expressible Feynman transform is interesting, but there are very few. In the literature, there is exactly one:
$$ K(p) = {1\over 2} p^2 \implies K'(v) = {1\over 2} v^2 $$
This takes care of quadratic momentum. If you restrict your attention to the published literature, the Feynman integral table is that ridiculous. This much takes care of all the usual quantum field theories, however, so it is not insignificant.
More Feynman transforms
Since the literature on this is pathetic, here are some nontrivial Feynman transforms, and the physics they describe:
Cauchy quantum mechanics: $$ K(p) = |p| \implies K'(v) = -\log( 1+ x^2) $$
This is a nice transform, because the Lagrangian path integral you get (in imaginary time) is
$$\int Dx e^{-\int \log(1+|\dot{q}|^2) - V(x)}$$
This path integral defines a path integral over Levy flights whose stable distribution is the Cauchy distribution. You can see this by looking at the propagation function between adjacent times, it gives a Cauchy distribution. This path integral defines Cauchy quantum mechanics. It's a special case of
Levy quantum mechanics: $$ K(p) = |p|^\alpha \implies K(x) = - \log( L_\alpha(x) ) $$
For $0<\alpha<2$, and where $L_\alpha$ is the unit Levy stable distribution for exponent $\alpha$. These quantum mechanical systems have been studied in recent years, but their path integral doesn't appear anywhere in the literature. The path integral is given by the Feynman transform.
There are tons more interesting Feynman transforms, they are the analog of Legendre transforms in classical mechanics, and are just as useful.
Proving unitarity
The path integral is well defined for any Euclidean statistical theory, but only a very few of these continue to quantum mechanics. A proof of unitarity usually passes to a Hamiltonian formulation, because this is manifestly unitary.
An example of a nonunitary renormalizable path integral statistical system which is otherwise perfectly ok is
$$\int d^8x |\nabla \phi|^4 + Z|\nabla\phi|^2 + t(\phi)^2 + \lambda \phi^4 $$
This system was studied in $8-\epsilon$ dimensions by Mukhamel, because it's epsilon expansion is pretty much the same as the $4-\epsilon$ expansion of the $\phi^4$ model. In eight dimensions, it defines a perfectly good second order point when Z and t are tuned to the right values. But the theory is absolutely not unitary--- there aren't any interacting scalar quantum theories in 8 dimensions. This can be seen immediately from the Kallen representation.
Any propagator in a unitary theory can be expressed in Euclidean space as
$$ G(k) = \int ds {\rho(s) \over k^2 - s}$$
That is, as a superposition of ordinary propagators at different values $s$ of the squared mass. $\rho(s)$ is non-negative, because in real time it is the norm of the state created by the field whose propagator you are expressing. It is this representation that tells you that wrong sign poles are ghost states.
The ${1\over k^4 + (A+B) k^2 + AB}$ Mukhamel Lifschitz-point propagator (with strange parametrization) is expressible as a spectral representation by partial fractions:
$$G(k) \propto {1\over k^2 + A} - {1\over k^2 + B}$$
This Kallen-Lehman spectral representation is clearly ghosty. The double-pole case has a Lehman function which is the derivative of a delta function, which is not positive definite either, by limits.
There are tons of non-unitary Euclidean theories, and to find the unitary ones, the Hamiltonian formulation is very helpful. Finding a no-ghost gauge and transforming to canonical form is how you prove that Gauge theory is unitary, for example.