Introduction to modules through a ModuleSystemTutorial.
ModulesForTheories: Using modules and records to capture mathematical theories.
RecordsNotModules: Why you shouldn't use the module system at all, and use dependent records instead.
ModulesNotRecords: Why the previous line does not always stand.
ProofTermsConsideredHarmful: Why using dependent records can be difficult, and sometimes inadvisable.