Bibliography on Module systems in Coq and Pure Type Systems

• Elie Soubiran. Modular development of theories and name-space management for the Coq proof assistant. PhD thesis. 2010. http://tel.archives-ouvertes.fr/docs/00/67/92/01/PDF/these.pdf
• Ulf Norell. A Module System for Agda. CHIT-CHAT 2006. http://www.cse.chalmers.se/~ulfn/talks/modules-061220.pdf
• Jacek Chrząszcz. Modules in Type Theory with Generative Definitions. PhD thesis. 2004. http://www.mimuw.edu.pl/~chrzaszcz/papers/thesis/
• Judicaël Courant. A Module Calculus for Pure Type Systems. TLCA 1997. https://web.archive.org/web/20061128053717/https://www.lri.fr/~jcourant/papers/tlca97/tlca.ps.gz