Time and date
11am-12pm 26 May 2019
In my presentation I would like to review Algorithm W of the Hindley–Milner type system, the type inference and type checking algorithm that powers the PureScript and Haskell compiler’s ability to prove a program’s type correctness. I would like to review and explain the rules of Algorithm W, unification, and also review the proofs currently used to show completeness and soundness, but offer a counter proof that shows Algorithm W isn’t necessarily complete. Specifically I would like to show that one can use diagonalization to show that some programs are undecidable when using Algorithm W.
For more other information regarding this research, please refer to this paper: https://www.sciencedirect.com/science/article/pii/S0168007298000475