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?

  • $\begingroup$ There is much less work on this because it is much less important: for example, decidability is largely irrelevant because it assumes that time and other resources don't matter. $\endgroup$
    – Stefan
    Commented Jun 6, 2019 at 12:40

1 Answer 1


Here are some results of a simple Google search:

  • 2
    $\begingroup$ Let me very strongly recommend the second link. They began with a formalization of my 2013 paper with J. Dunfield, and mechanization led them to an extremely elegant improvement to our algorithm. $\endgroup$ Commented Jun 5, 2019 at 10:29
  • $\begingroup$ I am glad to hear that Google works so well :-) $\endgroup$ Commented Jun 5, 2019 at 10:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.