Most of the work on programming language metatheory mechanization focus on the declarative properties of the languages (e.g., type soundness), but fail to address the algorithmic side, i.e. the type checking (or reconstruction) algorithm.
As far as I know, the only works that verified the algorithmic properties of type systems are the early papers on the mechanization of Algorithm W (Naraschewski & Nipkow 1999, Urban & Nipkow 2009), and Jacques Garrigue's certified type checker for a representative subset of OCaml (2014).
Are there any other work on formally verifying the completeness, soundness & other algorithmic properties (e.g., decidability) of type checking (or type inference) algorithms?