Today, everyone in #IT fancies himself a connoisseur of dependent types. But David MacQueen—a pillar in the ML #FP community and the designer of the ML module system—was already leading the way in this area four decades ago. His 1986 paper, “Using Dependent Types to Express Modular Structure”, was the first time I came across the term #DependentTypes.

I did not have the knowledge and the perspective to fully appreciate the significance of MacQueen work, back then. Nor was I aware of Constable’s #NuPRL and similar proof assistants exploiting dependent types, in those days.

https://www.cs.cmu.edu/~crary/819-f09/MacQueen86.pdf