The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Does anyone have any pointers to lists of commercial systems that use 
dependent type theory?  I mean "type theory" in a fairly loose sense, 
but the core characteristic I'm interested in is a complete copy of 
simply typed lambda calculus, or something fancier, embedded in a static 
type language.  I think GHC Haskell doesn't qualify, because they don't 
really seem to have type-level lambdas that can be computed with in the 
usual way, to support predictable enough type inference.

Thanks!