Dependent types: de Brujin (1967)
Curry-Howard: Curry (1934, 1958), Howard (1968)
MLTT: Martin-Lof (1972)
Polymorphic lambda-calculus: Girard (1972/3), Reynolds (1974)
Effect systems: Gifford/Lucassen (1986)
Calculus of constructions: Coquand/Huet (1988)
HKTs: Girard (1971)
Type classes: Kaes (1988)
Dates are imprecise and from memory.