The Coq mailing list

["J. Ian Johnson" <ianj AT ccs.neu.edu>]

Scala fits this bill, no? The shapeless library is a common tool in the 
toolbelt, which does lots of type level computation. I can't say which 
commercial entities are serious users of it off hand, however.
This might be a question for Twitter, since there are a bunch of Scala 
hackers there.

Also see the actual simply typed lambda calculus in Scala's type system here 
https://apocalisp.wordpress.com/2009/09/02/more-scala-typehackery/
-Ian
----- Original Message -----
From: "Adam Chlipala" 
<adamc AT csail.mit.edu>
To: "coq-club" 
<coq-club AT inria.fr>
Sent: Tuesday, March 25, 2014 11:21:45 AM GMT -05:00 US/Canada Eastern
Subject: [Coq-Club] Commercial applications of dependent type theory?

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!