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
----
See MultiParadigmWeenie