A function has dependent type if the type of a function's result depends on the VALUE of its argument; this is not the same thing as a ParameterizedType. The second order lambda calculus possesses functions with dependent types.
Languages with dependent types:
- CayenneLanguage; "Cayenne a Language With Dependent Types" (1998) http://citeseer.ist.psu.edu/augustsson98cayenne.html
- XanaduLanguage: http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html
- EpigramLanguage: http://cliki.tunes.org/Epigram
Why Dependent Types Matter http://www.cs.nott.ac.uk/~txa/talks/nijmegen-03.pdf
Dependent Types course handout http://www-2.cs.cmu.edu/~fp/courses/logic/handouts/dependent.pdf
Dependent types in practical programming (ACM subscription required) http://portal.acm.org/citation.cfm?id=292560&dl=ACM&coll=portal&CFID=11111111&CF TOKEN=2222222
Dynamic Typing With Dependent Types http://www.cs.princeton.edu/~gtan/paper/dynamic.pdf
mentioned in Formal Abstract Data Types http://www.cs.caltech.edu/~jyh/papers/depend/paper.ps
"Static Dependent Types for First Class Modules"
- "Static dependent types are the basis of a new type system that permits types and values to be packaged together into first class modules. Unlike other approaches to modules, static dependent types permit unrestricted access to the types and values in first class modules without sacrificing static type checking or data abstraction..."
- http://www.psrg.lcs.mit.edu/history/publications/Papers/lfp90abs.htm
Workshop on Subtyping & Dependent Types in Programming http://www-sop.inria.fr/oasis/DTP00/
Non-Dependent Types for Standard ML Modules http://www.dcs.ed.ac.uk/home/cvr/ppdp99.html