Hello, Here is probably a good paper to get people up to speed on dependent types (ironically written by two contributors to this mailing list??): okmij.org/ftp/papers/lightweight-static-capabilities.pdf Vasili