1 MC 2 A Module Calculus for Pure Type Systems

Several proof-assistants rely on the very formal basis of Pure Type Systems (PTS) as their foundations. We are concerned with the issues involved in the development of large proofs in these provers such as namespace management, development of reusable proof libraries and separate verification. Although implementations offer many features to address them, few theoretical foundations have been laid for them up to now. This is a problem as features dealing with modularity may have harmful, unsuspected effects on the reliability or usability of an implementation. In this paper, we propose an extension of Pure Type Systems with a module system, MC2, adapted from SML-like module systems for programming languages. This system gives a theoretical framework addressing the issues mentioned above in a quite uniform way. It is intended to be a theoretical foundation for the module systems of proofassistants such as Coq or Agda. We show how reliability and usability can be formalized as metatheoretical properties and prove they hold for MC2.