Constructing and refining modules in a type theory. - Shahad N. Ahmed (1994)