** Type theory
- [https://gist.github.com/chrisdone/0075a16b32bfd4f62b7b, [Typing Haskell in Haskell]], PDF: https://web.cecs.pdx.edu/~mpj/thih/thih.pdf
- http://okmij.org/ftp/ML/generalization.html
- http://smallshire.org.uk/sufficientlysmall/2010/04/11/a-hindley-milner-type-inference-implementation-in-python/
- http://okmij.org/ftp/Haskell/AlgorithmsH.html#teval
- https://github.com/tomprimozic/type-systems
- https://www21.in.tum.de/~nipkow/TRaAT/
- http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.65.7733&rep=rep1&type=pdf
- https://github.com/billpmurphy/hask
- http://canonical.org/~kragen/sw/dev3/term-rewriting.scm
- http://dev.stephendiehl.com/fun/006_hindley_milner.html
- http://dev.stephendiehl.com/fun/WYAH.pdf
- https://github.com/prakhar1989/type-inference
- http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec26-type-inference/type-inference.htm
- [Lambda The Ultimate discussion on type inference readling list](http://lambda-the-ultimate.org/node/3081) 
- https://github.com/computation-hs/comp-models
- https://github.com/UlfNorell/agda-summer-school
- https://github.com/coqoon/Software-Foundations
- https://github.com/TypeFunc/coq-intro
- https://github.com/UniversalAlgebra/Conferences
- https://github.com/williamdemeo/TypeFunc
- https://github.com/ifesdjeen/deflisp
- https://github.com/jozefg/hm
- https://github.com/pi8027/typeinfer
- Coq tutorials: https://www.youtube.com/playlist?list=PLDD40A96C2ED54E99
- https://github.com/wh5a/Algorithm-W-Step-By-Step

- http://www.cis.upenn.edu/~bcpierce/tapl/index.html
- http://www.seas.upenn.edu/~cis500/current/index.html
- http://www.cs.cornell.edu/courses/cs3110/2011sp/lectures/lec13-logic/logic.htm

** Compilers
- http://www.stephendiehl.com/llvm/
- https://github.com/jauhien/iron-kaleidoscope
- 2014 Software Foundations in Coq — Steve Zdancewic
- [[http://research.microsoft.com/en-us/um/people/simonpj/papers/slpj-book-1987/],[The Implementation of Functional Programming Languages]]


** Lang Design
- https://github.com/mietek/total-functional-programming