<p>Here are some results of a simple Google search:</p>

<ul>
<li><p><a href="https://doi.org/10.1023/A:1006285817788" rel="noreferrer">Certification of a Type Inference Tool for ML: Damas–Milner within Coq</a> by Catherine Dubois and Valérie Ménissier-Morain</p></li>
<li><p><a href="https://i.cs.hku.hk/~bruno/papers/itp2018.pdf" rel="noreferrer">Formalization of a Polymorphic Subtyping Algorithm</a> by Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers</p></li>
<li><p><a href="https://github.com/sdemos/type-inference" rel="noreferrer"><code>type-inference</code></a> formalization in Coq, based on <a href="https://people.cs.uchicago.edu/~gkuan/pubs/esop07-kmf.pdf" rel="noreferrer">A Rewriting Semantics for Type Inference</a></p></li>
</ul>

CC BY-SA 4.0
2019-06-05T10:29:40.777Z
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.
Neel Krishnaswami
CC BY-SA 4.0
2019-06-05T10:37:24.160Z
I am glad to hear that Google works so well :-)
Andrej Bauer
CC BY-SA 4.0
2019-06-05T07:27:29.427Z
2019-06-05T07:27:29.427Z
Andrej Bauer
<p>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.</p>

<p>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).</p>

<p>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?</p>

CC BY-SA 4.0
2019-06-06T12:40:26.820Z
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.
Stefan
<pl.programming-languages><type-theory><program-verification><type-inference>
Verified type checkers
xrq
# Verified type checkers

(Asked by: username_0 on 2019-06-05)

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?

**Tags:** pl.programming-languages, type-theory, program-verification, type-inference

> **Comments:**
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2019-06-05. Score: 6

Here are some results of a simple Google search:

* [Certification of a Type Inference Tool for ML: Damas–Milner within Coq](https://doi.org/10.1023/A:1006285817788) by Catherine Dubois and Valérie Ménissier-Morain
* [Formalization of a Polymorphic Subtyping Algorithm](https://i.cs.hku.hk/~bruno/papers/itp2018.pdf) by Jinxu Zhao, Bruno C. d. S. Oliveira, and Tom Schrijvers
* [`type-inference`](https://github.com/sdemos/type-inference) formalization in Coq, based on [A Rewriting Semantics for Type Inference](https://people.cs.uchicago.edu/~gkuan/pubs/esop07-kmf.pdf)

> **Comments:**
> **username_3**: 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.  
> **username_2**: I am glad to hear that Google works so well :-)  

---

