A module calculus for pure type systems

Abstract

Several proof-assistants rely on the very formal basis of Pure Type Systems (PTS). However, some practical issues raised by the development of large proofs lead to add other features to actual implementations for handling namespace management, for developing reusable proof libraries and for separate verification of distinct parts of large proofs. Unfortunately, few theoretical basis are given for these features. In this paper we propose an extension of Pure Type Systems with a module calculus adapted from SML-like module systems for programming pratiqueslanguages. Our module calculus gives a theoretical framework addressing the need for these features. We show that our module extension is conservative, and that type inference in the module extension of a given PTS is decidable under some hypotheses over this PTS.