3
$\begingroup$

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?

Improve this question
$\endgroup$
1
  • $\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
    Jun 6, 2019 at 12:40

1 Answer 1

Reset to default
6
$\begingroup$

Here are some results of a simple Google search:

Improve this answer
$\endgroup$
2
  • 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$
    – Neel Krishnaswami
    Jun 5, 2019 at 10:29
  • $\begingroup$ I am glad to hear that Google works so well :-) $\endgroup$
    – Andrej Bauer
    Jun 5, 2019 at 10:37

Your Answer

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

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