UPenn has a ton of really interesting work on extending the Haskell type system to support dependent typing. Some of the coolest pieces I've heard about had to

UPenn has a ton of really interesting work on extending the Haskell type system to support dependent typing. Some of the coolest pieces I've heard about had to do with guaranteeing the security of a server application through dependent typing. I never found out what the actual paper or project was that accomplished this. But these two papers[1][2] seems pretty interesting - having to do with guaranteeing safety of database access. [1] http://www.cis.upenn.edu/%7Eeir/papers/2012/singletons/paper.pdf http://www.cis.upenn.edu/%7Eeir/papers/2012/singletons/paper... [2] http://www.cis.upenn.edu/~ahae/papers/dfuzz-popl2013.pdf http://www.cis.upenn.edu/~ahae/papers/dfuzz-popl2013.pdf