Equational reasoning for linking with first-class primitive modules

Abstract

Modules and linking are usually formalized by encodings which use the λ-calculus, records (possibly dependent), and possibly some construct for recursion. In contrast, we introduce the m-calculus, a calculus where the primitive constructs are modules, linking, and the selection and hiding of module components. The m-calculus supports smooth encodings of software structuring tools such as functions (λ - calculus), records, objects (ς-calculus), and mutually recursive denitions. The m-calculus can also express widely varying kinds of module systems as used in languages like C, Haskell, and ML. We prove the m- calculus is confluent, thereby showing that equational reasoning via the m-calculus is sensible and well behaved. © 2000 Springer-Verlag Berlin Heidelberg.