Verified type checkers 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 &amp; Nipkow 1999, Urban &amp; 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 &amp; other algorithmic properties (e.g., decidability) of type checking (or type inference) algorithms?
Here are some results of a simple Google search:


Certification of a Type Inference Tool for ML: Damas–Milner within Coq by Catherine Dubois and Valérie Ménissier-Morain
Formalization of a Polymorphic Subtyping Algorithm by Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers
type-inference formalization in Coq, based on A Rewriting Semantics for Type Inference