- I think the Calculus of Inductive Constructions sounds solid. I don't know what the difference between most dependently typed systems is, though.
- Possible "stretch" features
- "Notation"-like mechanism to specify custom n-ary operators. Something like Agda's maybe?
- Reimplement and verify the language in itself.
- Module system? Either advanced (OCaml-like) or basic (just imports etc)
- I'm messing around with various ideas that Eric suggested. Check out
misc/ExtensibleExpr.lhs, for instance.