A modular module system

2000/05/01 by Xavier Leroy · 1 voice · 1 citation
Computer Science · #Formal Methods in Verification #Logic, programming, and type systems #Model-Driven Software Engineering Techniques

paper · pdf · doi:10.1017/s0956796800003683

openalex publication_date 2000/05/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/02

Abstract

A simple implementation of an SML-like module system is presented as a module parameterized by a base language and its type-checker. This implementation is useful both as a detailed tutorial on the Harper–Lillibridge–Leroy module system and its implementation, and as a constructive demonstration of the applicability of that module system to a wide range of programming languages.

Cited by

• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules

Discussions

• I found mention of this approach to compiling functors in Section 4 of “A modular module system” by Xavier Leroy doi.org/10.1017/S095... (author’s version: xavierleroy.org/publi/modula...), but I’ve n [bsky, 1 points, 0 comments]

Related

• The Design of a COM-Oriented Module System
• Achieving compositionality of the stable model semantics for Smodels programs
• Modula-2 and Oberon
• Removing Qualified Names in Modular Languages
• Modular System Synthesis