Auteur : Elie Soubiran  (PPS/INRIA - PI.R2)

Titre : A unified framework and a transparent name-space for Coq module system.

Abstract : 

We present an evolution of the Coq module system where we unify both structure
(i.e. module implementation) and signature (i.e. module interface) into a 
single concept called \textit{theory}. In order to easily derive theories, we 
equip our system with three theory combinators: application, inclusion and 
refinement. We also isolate a new notion of $\Delta$-equivalence that 
characterizes in a decidable way the exact equalities between paths implied by
modular construction. This equivalence provides the adequate information to 
simulate a transparent name-space from the user's point of view and furthermore
eases the integration of the non-logical features of Coq.