As Urs mentioned in his answer, free fields really constitute the guiding examples for the various axiomatic systems of QFT. The construction of free fields in Minkowski space is a standard part of the theory, though it may take some digging to find the precise reference where it is checked that such a construction satisfies the desired set of axioms. In particular, for the Haag-Kastler axiom system, once the theory is built on all of Minkowski space, one must show injectivity and isomorphism of the algebras localized in subsets of Minkowski space, with respect to appropriate inclusions of these subsets.
Constructions of various free bosonic and fermionic fields, including the specific cases of scalar and Dirac fields can be found in these classic references, in somewhat varying degrees of detail:
Baez, J. C., Segal, I. E., Zhou, Z., Introduction to Algebraic and Constructive Quantum Field Theory (Princeton, 1992)
Wald, R. M., Quantum field theory in curved spacetime and black hole thermodynamics, (Chicago, 1994).
There are two main stages to the construction. One has to build the linear space of solutions as a symplectic manifold (that's the classical phase space). Then one has to turn the algebra of functions on this space into a non-commutative $C^*$-algebra of quantum observables (that's quantization). Since the theories in question are linear, once the necessary functional analysis is in place, this is done by an infinite dimensional version of how it is done for a simple harmonic oscillator. For fermions it's fairly straightforward. For bosons one has to use the intermediate trick of working with the algebra of bounded functions generated by exponentiated smeared fields (that's the Weyl algebra). The actual unbounded operators representing smeared fields are constructed by taking derivatives of the elements of the Weyl algebra, once a representation has been chosen.
The same steps appear also in the work on QFT on curved spacetime, where different references described the individual steps in varying levels of detail. To get something like the Haag-Kastler axioms out of the latter constructions, one simply has to restrict onself to spacetimes consisting of causal-diamond shaped subspaces of Minkowski space. Classic references for particular field theories include:
- Dimock, J., [Dirac field], Trans. Am. Math. Soc. 269, (1982) p.133 (1982)
- Dimock, J., [Maxwell field], Rev. Math. Phys. 4 (1992) p.223
- Furlani, E.P., [Proca field], J. Math. Phys. 40 (1999) p.2611
The biggest technical sticking point in these references is how they treat (or don't treat) non-compact Cauchy surfaces.
The modern generalization of the Haag-Kastler axioms to arbitrary globally hyperbolic Lorentzian spacetimes are the Brunetti-Fredenhagen-Verch (or Locally Covariant Quantum Field Theory) axioms. Here's a couple of modern references that give the construction of free fields (subsuming most of the above particular examples), in great mathematical detail, that fits directly into this framework:
- Bär, C., Ginoux, N. & Pfäffle, F., Wave Equations on Lorentzian Manifolds and Quantization, (EMS, 2007).
- Baer, C. & Ginoux, N., Classical and quantum fields on lorentzian manifolds (2011)
(Note for the cognoscenti: in this restricted situation, quantization does happen to be a functor!)
Of course, much more literature can be found by digging backward and forward in the citation network starting with the above references.