Reuse of SML module system for the B language

Abstract. In this paper, we are concerned with studying the semantic of the B modularity. We reuse the Harper-Lillibridge-Leroy (HLL) module system. This system implements an SML like module system for a core language. We will discuss how to simulate the B modularity with such a system. This simulation is based on the syntax categories of the B language that makes possible the expres-sion of a major part of the type-checking rules in the core B language. Thus the B modularity is easier to understand.