Here are some milestone theory papers that you might want to read (and
pick up the formalisms needed along the way). This list is in no way
complete---these are just a few milestones in a rich and rapidly
developing field. For a comprehensive history, refer to the paper and video in
http://research.microsoft.com/en-us/um/people/simonpj/papers/history-of-haskell/

-------------------------[ Papers ]-------------------------

http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
(watch https://www.youtube.com/watch?v=IOiZatlZtGU)
(see also http://wadler.blogspot.co.uk/2014/06/propositions-as-types-updated.html)

"Compiling pattern matching", Lennart Augustsson
http://link.springer.com/chapter/10.1007%2F3-540-15975-4_48 [paywalled :(]

(PDF should be available from a Dartmouth IP address;
 see http://stackoverflow.com/questions/7883023/algorithm-for-type-checking-ml-like-pattern-matching
 for a nicely digested example) 

"Principal type-schemes for functional programs", Luis Damas and Robin Milner
http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf

"Introduction to generalized type systems", Henk Barendregt 
http://repository.ubn.ru.nl/bitstream/2066/17240/1/13256.pdf  [rename to PDF after you get the file]

(this paper introduced the idea that types can depend not just on
 other types, like "List a", but also on expressions. The research
 field that developed from it is called dependent types, and includes
 languages like Agda and Idris, which some see as successors to
 Haskell)