•Typed, staged interpreters
–For languages with binding, with patterns, algebraic
datatypes
•Type preserving transformations
–Simplify :: Exp t -> Exp t
–Cps:: Exp t -> Exp {trans t}
•Proof carrying code
•Data Structures
–Red-Black trees, Binomial Heaps , Static length
lists
•Languages with security properties
•Typed self-describing databases, where meta data in the database describes the database schema
•Programs that slip easily between dynamic and statically
typed sections. Type-case is easy to
encode with no additional
mechanism