publications:
- title: "A Module System for a Programming Language Based on the LF Logical Framework"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Frank Pfenning"
    link: "http://www.cs.cmu.edu/~fp/"
  year: "1998"
  tags:
  - "programming languages"
  - "rule-based"
  - "programming"
  researchr: "https://researchr.org/publication/HarperP98"
  cites: 0
  citedby: 0
  journal: "logcom"
  volume: "8"
  number: "1"
  pages: "5-31"
  kind: "article"
  key: "HarperP98"
- title: "A type system for higher-order modules"
  author:
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  year: "2003"
  doi: "http://doi.acm.org/10.1145/640128.604151"
  abstract: "We present a type theory for higher-order modules that accounts for many central issues in module system design, including translucency, applicativity, generativity, and modules as first-class values. Our type system harmonizes design elements from previous work, resulting in a simple, economical account of modular programming. The main unifying principle is the treatment of abstraction mechanisms as computational effects. Our language is the first to provide a complete and practical formalization of all of these critical issues in module system design."
  links:
    doi: "http://doi.acm.org/10.1145/640128.604151"
  tags:
  - "type system"
  researchr: "https://researchr.org/publication/DreyerCH03"
  cites: 0
  citedby: 0
  pages: "236-249"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "DreyerCH03"
- title: "A Closer Look at Export and Import Statements"
  author:
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  - name: "Daniel P. Friedman"
    link: "https://researchr.org/alias/daniel-p.-friedman"
  year: "1986"
  researchr: "https://researchr.org/publication/FelleisenF86"
  cites: 0
  citedby: 0
  journal: "Comp. Lang., Syst. \\& Struct."
  volume: "11"
  number: "1"
  pages: "29-37"
  kind: "article"
  key: "FelleisenF86"
- title: "A modular module system"
  author:
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "2000"
  researchr: "https://researchr.org/publication/Leroy00"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "10"
  number: "3"
  pages: "269-303"
  kind: "article"
  key: "Leroy00"
- title: "A Framework for Modular Linking in OO Languages"
  author:
  - name: "Sean McDirmid"
    link: "https://researchr.org/alias/sean-mcdirmid"
  - name: "Wilson C. Hsieh"
    link: "https://researchr.org/alias/wilson-c.-hsieh"
  - name: "Matthew Flatt"
    link: "http://www.cs.utah.edu/~mflatt/"
  year: "2006"
  doi: "http://dx.doi.org/10.1007/11860990_9"
  links:
    doi: "http://dx.doi.org/10.1007/11860990_9"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/McDirmidHF06"
  cites: 0
  citedby: 0
  pages: "116-135"
  booktitle: "jmlc"
  kind: "inproceedings"
  key: "McDirmidHF06"
- title: "A syntactic type system for recursive modules"
  author:
  - name: "Hyeonseung Im"
    link: "https://researchr.org/alias/hyeonseung-im"
  - name: "Keiko Nakata"
    link: "https://researchr.org/alias/keiko-nakata"
  - name: "Jacques Garrigue"
    link: "https://researchr.org/alias/jacques-garrigue"
  - name: "Sungwoo Park"
    link: "https://researchr.org/alias/sungwoo-park"
  year: "2011"
  doi: "http://doi.acm.org/10.1145/2048066.2048141"
  abstract: "A practical type system for ML-style recursive modules should address at least two technical challenges. First, it needs to solve the double vision problem, which refers to an inconsistency between external and internal views of recursive modules. Second, it needs to overcome the tension between practical decidability and expressivity which arises from the potential presence of cyclic type definitions caused by recursion between modules. Although type systems in previous proposals solve the double vision problem and are also decidable, they fail to typecheck common patterns of recursive modules, such as functor fixpoints, that are essential to the expressivity of the module system and the modular development of recursive modules. This paper proposes a novel type system for recursive modules that solves the double vision problem and typechecks common patterns of recursive modules including functor fixpoints. First, we design a type system with a type equivalence based on weak bisimilarity, which does not lend itself to practical implementation in general, but accommodates a broad range of cyclic type definitions. Then, we identify a practically implementable fragment using a type equivalence based on type normalization, which is expressive enough to typecheck typical uses of recursive modules. Our approach is purely syntactic and the definition of the type system is ready for use in an actual implementation."
  links:
    doi: "http://doi.acm.org/10.1145/2048066.2048141"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/oopsla/ImNGP11"
  researchr: "https://researchr.org/publication/ImNGP11"
  cites: 0
  citedby: 0
  pages: "993-1012"
  booktitle: "OOPSLA"
  kind: "inproceedings"
  key: "ImNGP11"
- title: "Submodules in racket: you want it when, again?"
  author:
  - name: "Matthew Flatt"
    link: "http://www.cs.utah.edu/~mflatt/"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2517208.2517211"
  abstract: "In an extensible programming language, programmers write code that must run at different times - in particular, at compile time versus run time. The module system of the Racket programming language enables a programmer to reason about programs in the face of such extensibility, because the distinction between run-time and compile-time phases is built into the language model. Submodules extend Racket's module system to make the phase-separation facet of the language extensible. That is, submodules give programmers the capability to define new phases, such as \"test time\" or \"documentation time,\" with the same reasoning and code-management benefits as the built-in distinction between run time and compile time."
  links:
    doi: "http://doi.acm.org/10.1145/2517208.2517211"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/conf/gpce/Flatt13"
  researchr: "https://researchr.org/publication/Flatt13"
  cites: 0
  citedby: 0
  pages: "13-22"
  booktitle: "GPCE"
  kind: "inproceedings"
  key: "Flatt13"
- title: "Recursive type generativity"
  author:
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  year: "2007"
  doi: "http://dx.doi.org/10.1017/S0956796807006429"
  links:
    doi: "http://dx.doi.org/10.1017/S0956796807006429"
  researchr: "https://researchr.org/publication/Dreyer07"
  cites: 0
  citedby: 0
  journal: "JFP"
  volume: "17"
  number: "4-5"
  pages: "433-471"
  kind: "article"
  key: "Dreyer07"
- title: "Advanced module systems: a guide for the perplexed (abstract of invited talk)"
  author:
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Benjamin C. Pierce"
    link: "http://www.cis.upenn.edu/~bcpierce/"
  year: "2000"
  doi: "http://doi.acm.org/10.1145/351240.351252"
  links:
    doi: "http://doi.acm.org/10.1145/351240.351252"
  tags:
  - "C++"
  researchr: "https://researchr.org/publication/HarperP00"
  cites: 0
  citedby: 0
  pages: "130"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "HarperP00"
- title: "Units: Cool Modules for HOT Languages"
  author:
  - name: "Matthew Flatt"
    link: "http://www.cs.utah.edu/~mflatt/"
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  year: "1998"
  abstract: "A module system ought to enable assembly-line programming using separate compilation and an expressive linking language. Separate compilation allows programmers to develop parts of a program independently. A linking language gives programmers precise control over the assembly of parts into a whole. This paper presents models of program units, MzScheme's module language for assembly-line programming. Units support separate compilation, independent module reuse, cyclic dependencies, hierarchical structuring, and dynamic linking. The models explain how to integrate units with untyped and typed languages such as Scheme and ML."
  researchr: "https://researchr.org/publication/FlattF98"
  cites: 0
  citedby: 0
  pages: "236-248"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "FlattF98"
- title: "Mixin' Up the ML Module System"
  author:
  - name: "Andreas Rossberg"
    link: "https://researchr.org/alias/andreas-rossberg"
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  year: "2013"
  doi: "http://doi.acm.org/10.1145/2450136.2450137"
  links:
    doi: "http://doi.acm.org/10.1145/2450136.2450137"
    dblp: "http://dblp.uni-trier.de/rec/bibtex/journals/toplas/RossbergD13"
  researchr: "https://researchr.org/publication/RossbergD13"
  cites: 0
  citedby: 0
  journal: "TOPLAS"
  volume: "35"
  number: "1"
  pages: "2"
  kind: "article"
  key: "RossbergD13"
- title: "Hygienic Macro Expansion"
  author:
  - name: "Eugene E. Kohlbecker"
    link: "https://researchr.org/alias/eugene-e.-kohlbecker"
  - name: "Daniel P. Friedman"
    link: "https://researchr.org/alias/daniel-p.-friedman"
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  - name: "Bruce F. Duba"
    link: "https://researchr.org/alias/bruce-f.-duba"
  year: "1986"
  doi: "http://delivery.acm.org/10.1145/320000/319859/p151-kohlbecker.pdf?key1=319859&key2=7573098711&coll=&dl=ACM&CFID=15151515&CFTOKEN=6184618"
  links:
    doi: "http://delivery.acm.org/10.1145/320000/319859/p151-kohlbecker.pdf?key1=319859&key2=7573098711&coll=&dl=ACM&CFID=15151515&CFTOKEN=6184618"
  tags:
  - "macros"
  - "e-science"
  - "Hygienic Macro"
  researchr: "https://researchr.org/publication/KohlbeckerFFD86"
  cites: 0
  citedby: 0
  pages: "151-161"
  booktitle: "lfp"
  kind: "inproceedings"
  key: "KohlbeckerFFD86"
- title: "What is a Recursive Module?"
  author:
  - name: "Karl Crary"
    link: "https://researchr.org/alias/karl-crary"
  - name: "Robert Harper"
    link: "http://www.cs.cmu.edu/~rwh/"
  - name: "Sidd Puri"
    link: "https://researchr.org/alias/sidd-puri"
  year: "1999"
  doi: "http://doi.acm.org/10.1145/301618.301641"
  abstract: "A hierarchical module system is an effective tool for structuring large programs. Strictly hierarchical module systems impose an acyclic ordering on import dependencies among program units. This can impede modular programming by forcing mutually-dependent components to be consolidated into a single module. Recently there have been several proposals for module systems that admit cyclic dependencies, but it is not clear how these proposals relate to one another, nor how one might integrate them into an expressive module system such as that of ML.To address this question we provide a type-theoretic analysis of the notion of a recursive module in the context of a \"phase-distinction\" formalism for higher-order module systems. We extend this calculus with a recursive module mechanism and a new form of signature, called a recursively dependent signature, to support the definition of recursive modules. These extensions are justified by an interpretation in terms of more primitive language constructs. This interpretation may also serve as a guide for implementation."
  links:
    doi: "http://doi.acm.org/10.1145/301618.301641"
  researchr: "https://researchr.org/publication/CraryHP99"
  cites: 0
  citedby: 0
  pages: "50-63"
  booktitle: "PLDI"
  kind: "inproceedings"
  key: "CraryHP99"
- title: "Applicative Functors and Fully Transparent Higher-Order Modules"
  author:
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "1995"
  researchr: "https://researchr.org/publication/Leroy95"
  cites: 0
  citedby: 0
  pages: "142-153"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "Leroy95"
- title: "Extensible Denotational Language Specifications"
  author:
  - name: "Robert Cartwright"
    link: "https://researchr.org/alias/robert-cartwright"
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  year: "1994"
  abstract: "Traditional denotational semantics assigns radically different meanings to one and the same phrase depending on the rest of the programming language. If the language is purely functional, the denotation of a numeral is a function from environments to integers. But, in a functional language with imperative control operators, a numeral denotes a function from environments and continuations to integers. This paper introduces a new format for denotational language specifications, extended direct semantics, that accommodates orthogonal extensions of a language without changing the denotations of existing phrases. An extended direct semantics always maps a numeral to the same denotation: the injection of the corresponding number into the domain of values. In general, the denotation of a phrase in a functional language is always a projection of the denotation of the same phrase in the semantics of an extended language—no matter what the extension is. Based on extended direct semantics, it is also possible to construct interpreters for complete languages by composing interpreters for language fragments."
  tags:
  - "extensible language"
  researchr: "https://researchr.org/publication/CartwrightF94"
  cites: 0
  citedby: 0
  pages: "244-272"
  booktitle: "tacs"
  kind: "inproceedings"
  key: "CartwrightF94"
- title: "Mixin modules in a call-by-value setting"
  author:
  - name: "Tom Hirschowitz"
    link: "https://researchr.org/alias/tom-hirschowitz"
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "2005"
  doi: "http://doi.acm.org/10.1145/1086642.1086644"
  links:
    doi: "http://doi.acm.org/10.1145/1086642.1086644"
  researchr: "https://researchr.org/publication/HirschowitzL05"
  cites: 0
  citedby: 0
  journal: "TOPLAS"
  volume: "27"
  number: "5"
  pages: "857-881"
  kind: "article"
  key: "HirschowitzL05"
- title: "A type system for recursive modules"
  author:
  - name: "Derek Dreyer"
    link: "https://researchr.org/alias/derek-dreyer"
  year: "2007"
  doi: "http://doi.acm.org/10.1145/1291151.1291196"
  links:
    doi: "http://doi.acm.org/10.1145/1291151.1291196"
  tags:
  - "type system"
  researchr: "https://researchr.org/publication/Dreyer07%3A0"
  cites: 0
  citedby: 0
  pages: "289-302"
  booktitle: "ICFP"
  kind: "inproceedings"
  key: "Dreyer07:0"
- title: "Hygienic macro expansion"
  author:
  - name: "Kohlbecker, Eugene"
    link: "https://researchr.org/alias/kohlbecker%2C-eugene"
  - name: "Friedman, Daniel P."
    link: "https://researchr.org/alias/friedman%2C-daniel-p."
  - name: "Matthias Felleisen"
    link: "http://www.ccs.neu.edu/home/matthias/"
  - name: "Duba, Bruce"
    link: "https://researchr.org/alias/duba%2C-bruce"
  year: "1986"
  doi: "http://doi.acm.org/10.1145/319838.319859"
  links:
    doi: "http://doi.acm.org/10.1145/319838.319859"
  tags:
  - "macros"
  researchr: "https://researchr.org/publication/319859"
  cites: 0
  citedby: 0
  booktitle: "LFP '86: Proceedings of the 1986 ACM conference on LISP and functional programming"
  kind: "inproceedings"
  key: "319859"
- title: "Manifest Types, Modules, and Separate Compilation"
  author:
  - name: "Xavier Leroy"
    link: "http://pauillac.inria.fr/~xleroy/"
  year: "1994"
  doi: "10.1145/174675.176926"
  abstract: "This paper presents a variant of the SML module system that introduces a strict distinction between abstract types and manifest types (types whose definitions are part of the module specification), while retaining most of the expressive power of the SML module system. The resulting module system provides much better support for separate compilation. "
  researchr: "https://researchr.org/publication/Leroy94"
  cites: 0
  citedby: 0
  pages: "109-122"
  booktitle: "POPL"
  kind: "inproceedings"
  key: "Leroy94"