Bibliography of ML Modules
Journal
Logical relations as types: Proof-relevant parametricity for program modules
Jonathan Sterling and Robert Harper. 2021
https://www.jonmsterling.com/papers/sterling-harper-2021.pdf
DOI: 10.1145/3474834
Slides 1: https://www.cs.cmu.edu/~rwh/talks/paramstr.pdf
Slides 2: https://www.jonmsterling.com/slides/sterling-2021-au-ccs.pdf
A focused solution to the avoidance problem
Karl Crary. 2020
Fully abstract module compilation
Karl Crary. 2019
https://dl.acm.org/ft_gateway.cfm?id=3290323
DOI: 10.1145/3290323
Slides: https://popl19.sigplan.org/event/popl-2019-research-papers-fully-abstract-module-compilation
1ML — Core and modules united
Andreas Rossberg. 2018
F-ing modules
Andreas Rossberg, Claudio V. Russo and Derek Dreyer. 2014
Mixin’ up the ML module system
Andreas Rossberg and Derek Dreyer. 2013
Path resolution for nested recursive modules
Jacques Garrigue and Keiko Nakata. 2012
http://www.math.nagoya-u.ac.jp/~garrigue/papers/path-resolution-1205.pdf
A flattening strategy for SML module compilation and its implementation
Liu Bochao and Atsushi Ohori. 2010
https://www.jstage.jst.go.jp/article/imt/5/1/5_1_58/_pdf/-char/en
DOI: 10.11185/imt.5.58
Sound and complete elimination of singleton kinds
Karl Crary. 2007
Extensional equivalence and singleton types
Christopher Stone and Robert Harper. 2006
Mixin modules in a call-by-value setting
Tom Hirschowitz and Xavier Leroy. 2005
Types for modules
Claudio V. Russo. 2003
https://www.microsoft.com/en-us/research/wp-content/uploads/1998/03/Types-for-Modules.pdf
A theory of mixin modules: Basic and derived operators
Davide Ancona and Elena Zucca. 1998
A syntactic theory of type generativity and sharing
Xavier Leroy. 1996
Studying the ML module system in HOL
Elsa Gunter and Savi Maharaj. 1995
On the type structure of Standard ML
Robert Harper and John C. Mitchell. 1993
https://crypto.stanford.edu/~jcm/papers/harper-mitch-TOPLAS-93.pdf
A category-theoretic account of program modules
Eugenio Moggi. 1991
Abstract types have existential type
John C. Mitchell and Gordon D. Plotkin. 1988
https://theory.stanford.edu/~jcm/papers/mitch-plotkin-88.pdf
DOI: 10.1145/44501.45065
Modules for Standard ML
David B. MacQueen. 1985
http://lucacardelli.name/Papers/Polymorphism%20Vol%20II,%20No%202.pdf
Proceedings
Retrofitting OCaml modules: Fixing signature avoidance in the generative case
Clément Blaudeau, Didier Rémy and Gabriel Radanne. 2023
A metalanguage for multi-phase modularity
Jonathan Sterling and Robert Harper. 2021
https://www.jonmsterling.com/papers/sterling-harper-2021-mlw.pdf
Slides: https://www.jonmsterling.com/slides/sterling-harper-2021-mlw.pdf
Extending OCaml's open
Runhang Li and Jeremy Yallop. 2019
https://www.cl.cam.ac.uk/~jdy22/papers/extending-ocamls-open-draft.pdf
DOI: 10.4204/EPTCS.294.1
Characterising renaming within OCaml’s module system: Theory and implementation
Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson and Scott Owens. 2019
https://www.cs.kent.ac.uk/people/staff/rnsr/docs/renaming-pldi2019.pdf
Static interpretation of higher-order modules in Futhark: Functional GPU programming in the large
Martin Elsman, Troels Henriksen, Danil Annenkov and Cosmin E. Oancea. 2018
https://futhark-lang.org/publications/icfp18.pdf
DOI: 10.1145/3236792
Modules, abstraction, and parametric polymorphism
Karl Crary. 2017
Extending OCaml's open (extended abstract)
Runhang Li and Jeremy Yallop. 2017
https://www.cl.cam.ac.uk/~jdy22/papers/extending-ocamls-open.pdf
1ML with special effects (F-ing generativity polymorphism)
Andreas Rossberg. 2016
https://people.mpi-sws.org/~rossberg/1ml/1ml-effects.pdf
DOI: 10.1007/978-3-319-30936-1_18
Slides: https://events.inf.ed.ac.uk/wf2016/slides/rossberg.pdf
1ML — Core and modules united (F-ing first-class modules)
Andreas Rossberg. 2015
Type-level module aliases: independent and equal
Jacques Garrigue and Leo P. White. 2014
http://www.math.nagoya-u.ac.jp/~garrigue/papers/modalias.pdf
Slides: http://www.math.nagoya-u.ac.jp/~garrigue/papers/modalias-show.pdf
Backpack: Retrofitting Haskell with interfaces
Scott Kilpatrick, Derek Dreyer, Simon Peyton Jones and Simon Marlow. 2014
https://people.mpi-sws.org/~dreyer/papers/backpack/paper.pdf
Contractive signatures with recursive types, type parameters, and abstract types
Hyeonseung Im, Keiko Nakata and Sungwoo Park. 2013
A syntactic type system for recursive modules
Hyeonseung Im, Keiko Nakata, Jacques Garrigue and Sungwoo Park. 2011
http://www.math.nagoya-u.ac.jp/~garrigue/papers/oopsla2011.pdf
First-class modules and composable signatures in Objective Caml 3.12
Alain Frisch and Jacques Garrigue. 2010
http://www.math.nagoya-u.ac.jp/~garrigue/papers/ml2010.pdf
Slides: http://www.math.nagoya-u.ac.jp/~garrigue/papers/ml2010-show.pdf
F-ing modules
Andreas Rossberg, Claudio V. Russo and Derek Dreyer. 2010
Engineering higher-order modules in SML/NJ
George Kuan and David B. MacQueen. 2009
A syntactic account of singleton types via hereditary substitution
Karl Crary. 2009
Modeling abstract types in modules with open existential types
Benoît Montagu and Didier Rémy. 2009
http://gallium.inria.fr/~remy/modules/Montagu-Remy@popl09:fzip.pdf
Mixin’ up the ML module system
Derek Dreyer and Andreas Rossberg. 2008
Path resolution for recursive nested modules is undecidable
Keiko Nakata and Jacques Garrigue. 2007
Modular type classes
Derek Dreyer, Robert Harper and Manuel M. T. Chakravarty. 2007
https://people.mpi-sws.org/~dreyer/papers/mtc/main-short.pdf
Principal type schemes for modular programs
Derek Dreyer and Matthias Blume. 2007
https://people.mpi-sws.org/~dreyer/papers/infmod/main-short.pdf
A type system for recursive modules
Derek Dreyer. 2007
https://people.mpi-sws.org/~dreyer/papers/recmod/main-short.pdf
Towards a mechanized metatheory of Standard ML
Daniel K. Lee, Karl Crary and Robert Harper. 2007
From structures and functors to modules and units
Scott Owens and Matthew Flatt. 2006
Recursive modules for programming
Keiko Nakata and Jacques Garrigue. 2006
http://www.math.nagoya-u.ac.jp/~garrigue/papers/nakata-icfp2006.pdf
Type inference, principal typings, and let-polymorphism for first-class mixin modules
Henning Makholm and J. B. Wells. 2005
Recursion for structured modules
Keiko Nakata. 2005
Recursive object-oriented modules
Keiko Nakata, Akira Ito and Jacques Garrigue. 2005
http://www.math.nagoya-u.ac.jp/~garrigue/papers/fool_2005.pdf
An expressive language of signatures
Norman Ramsey, Kathleen Fisher and Paul Govereau. 2005
A type system for well-founded recursion
Derek Dreyer. 2004
https://people.mpi-sws.org/~dreyer/papers/recursion/popl.pdf
A type system for higher-order modules
Derek Dreyer, Karl Crary and Robert Harper. 2003
Mixin modules and computational effects
Davide Ancona, Sonia Fagorzi, Eugenio Moggi and Elena Zucca. 2003
A formal specification of the Haskell 98 module system
Iavor S. Diatchki, Mark P. Jones and Thomas Hallgren. 2002
First-class modules for Haskell
Mark Shields and Simon Peyton Jones. 2002
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/first_class_modules.pdf
Mixin modules in a call-by-value setting
Tom Hirschowitz and Xavier Leroy. 2002
Modules, abstract types, and distributed versioning
Peter Sewell. 2001
Recursive structures for Standard ML
Claudio V. Russo. 2001
First-class structures for Standard ML
Claudio V. Russo. 2000
https://link.springer.com/content/pdf/10.1007%2F3-540-46425-5_22.pdf
Sound and complete elimination of singleton kinds
Karl Crary. 2000
http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-161D.pdf
Deciding type equivalence in a language with singleton kinds
Christopher Stone and Robert Harper. 2000
Equational reasoning for linking with first-class primitive modules
J. B. Wells and René Vestergaard. 2000
Transparent modules with fully syntactic signatures
Zhong Shao. 1999
What is a recursive module?
Karl Crary, Robert Harper and Sidd Puri. 1999
http://www.cs.cmu.edu/~crary/papers/1999/recmod/recmod.ps.gz
Units: Cool modules for HOT languages
Matthew Flatt and Matthias Felleisen. 1998
Modular object-oriented programming with units and mixins
Robert Bruce Findler and Matthew Flatt. 1998
Programming language semantics in foundational type theory
Karl Crary. 1998
http://www.cs.cmu.edu/~crary/papers/1998/tt-semant/tt-semant.ps.gz
Parameterized modules, recursive modules and mixin modules
Dominic Duggan and Constantinos Sourelis. 1998
Elaboration and phase-splitting in the TIL/ML compiler
Christopher Stone. 1997
http://www.cs.cmu.edu/~fox/foxnet/people/cstone/papers/ic97.ps
An applicative module calculus
Judicaël Courant. 1997
https://link.springer.com/content/pdf/10.1007%2FBFb0030630.pdf
DOI: 10.1007/BFb0030630
Program fragments, linking, and modularization
Luca Cardelli. 1997
Type isomorphisms for module signatures
María-Virginia Aponte and Roberto Di Cosmo. 1996
http://www.dicosmo.org/Articles/1996-AponteDiCosmo-PLILP.pdf
An exploration of modular programs
Jan Nicklish and Simon Peyton Jones. 1996
https://www.microsoft.com/en-us/research/wp-content/uploads/1996/01/Nicklisch-modules.pdf
Using parameterized signatures to express modular structure
Mark P. Jones. 1996
Mixin modules
Dominic Duggan and Constantinos Sourelis. 1996
https://www.cs.tufts.edu/~nr/cs257/archive/dominic-duggan/Mixin%20Modules.pdf
From Hindley-Milner types to first-class structures
Mark P. Jones. 1995
Applicative functors and fully transparent higher-order modules
Xavier Leroy. 1995
Higher-order functors with transparent signatures
Sandip K. Biswas. 1995
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.14.9123&rep=rep1&type=pdf
Studying the ML module system in HOL
Savi Maharaj and Elsa Gunter. 1994
An implementation of higher-order functors
Pierre Crégut and David B. MacQueen. 1994
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.32.1516&rep=rep1&type=pdf
A semantics for higher-order functors
David B. MacQueen and Mads Tofte. 1994
https://rd.springer.com/content/pdf/10.1007%2F3-540-57880-3_27.pdf
Manifest types, modules, and separate compilation
Xavier Leroy. 1994
A type-theoretic approach to higher-order modules with sharing
Robert Harper and Mark Lillibridge. 1994
Extending record typing to type parametric modules with sharing
María Virginia Aponte. 1993
An extension of Standard ML modules with subtyping and inheritance
John C. Mitchell, Sigurd Meldal and Neel Madhav. 1991
DOI: 10.1145/99583.99620
Mixin-based inheritance
Gilad Bracha and William Cook. 1990
http://www.bracha.org/oopsla90.ps
DOI: 10.1145/97945.97982
Abstract types and the dot notation
Luca Cardelli and Xavier Leroy. 1990
https://xavierleroy.org/publi/abstract-types-dot-notation.pdf
Higher-order modules and the phase distinction
Robert Harper, John C. Mitchell and Eugenio Moggi. 1990
http://theory.stanford.edu/people/jcm/papers/harper-mm-90.pdf
DOI: 10.1145/96709.96744
Persistence and type abstraction
Luca Cardelli and David B. MacQueen. 1988. First appeared in 1985
http://lucacardelli.name/Papers/Persistence%20and%20Type%20Abstraction.pdf
A type discipline for program modules
Robert Harper, Robin Milner and Mads Tofte. 1987
https://link.springer.com/content/pdf/10.1007%2FBFb0014988.pdf
DOI: 10.1007/BFb0014988
Using dependent types to express modular structure
David B. MacQueen. 1986
Abstract types have existential types
John C. Mitchell and Gordon D. Plotkin. 1985
Modules for Standard ML
David B. MacQueen. 1984
A kernel language for abstract data types and modules
R. Burstall and B. Lampson. 1984
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/35-KernelModules.pdf
Types, abstraction and parametric polymorphism
J. C. Reynolds. 1983
Dissertation
OCaml modules: formalization, insights and improvements: Bringing the existential types into a generative subset
Clément Blaudeau. 2021
Backpack: Towards practical mix-in linking in Haskell
Edward Z. Yang. June 2017
Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types
Benoît Montagu. 2010
A true higher-order module system
George Kuan. 2010
A module system with applicative functors and recursive path references
Keiko Nakata. 2007
Certifying compilation for Standard ML in a type analysis framework
Leaf Eames Petersen. 2005
http://www.leafpetersen.com/leaf/publications/thesis/main.pdf
Understanding and evolving the ML module system
Derek Dreyer. 2005
Singleton kinds and singleton types
Christopher Stone. 2000
http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-153.pdf
Program modules, separate compilation, and intermodule optimisation
Martin Elsman. 1999
Type-theoretic methodology for practical programming languages
Karl Fredrick Crary. 1998
http://www.cs.cmu.edu/~crary/papers/1998/thesis/thesis.ps.gz
Translucent sums: A foundation for higher-order module systems
Mark Lillibridge. 1997
Type systems for modular programs and specifications
David R. Aspinall. 1997
A module system for LOOM
Leaf Eames Petersen. 1996
http://www.leafpetersen.com/leaf/publications/loom_thesis/thesis.pdf
The programming language JIGSAW: Mixins, modularity and multiple inheritance
Gilad Bracha. 1992
Operational semantics and polymorphic type inference
Mads Tofte. 1988
Technical report
Mechanizing the metatheory of Standard ML
Daniel K. Lee, Karl Crary and Robert Harper. 2006
http://www.cs.cmu.edu/~dklee/papers/tslf.pdf
Slides: https://www.seas.upenn.edu/~sweirich/wmm/wmm06/lee-talk.pdf
Practical type theory for recursive modules
Derek Dreyer. 2006
Path resolution for recursive modules
Keiko Nakata. 2006
Type generativity in higher-order module systems
Paul Govereau. 2005
https://dash.harvard.edu/bitstream/handle/1/23853816/tr-05-05.pdf
Toward a practical type theory for recursive modules
Derek Dreyer, Robert Harper and Karl Crary. 2001
Implementing the TILT internal language
Leaf Petersen, Perry Cheng, Robert Harper and Christopher Stone. 2000
http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-180.pdf
An interpretation of Standard ML in type theory
Robert Harper and Christopher Stone. 1997
Standard ML type generativity as existential quantification
Claudio V. Russo. 1996
Modularity meets inheritance
Gilad Bracha and Gary Lindstrom. 1991
On understanding types, data abstraction, and polymorphism
Luca Cardelli and P. Wegner. 1985
In book
A type-theoretic interpretation of Standard ML
Robert Harper and Christopher Stone. 2000
Manuscript
Reflections on existential types
Jonathan Sterling. 2022
https://www.jonmsterling.com/papers/sterling-2022-existentials.pdf
Backpack to work: Towards practical mixin linking for Haskell
Simon Peyton Jones, Edward Yang, Scott Kilpatrick and Derek Dreyer. March 2016
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/backpack-2016.pdf
Lazy modules: A lazy evaluation strategy for more recursive initialization patterns
Keiko Nakata. 2008
A logical account of type generativity: Abstract types have open existential types
Benoît Montagu and Didier Rémy. April 14, 2008
http://gallium.inria.fr/~remy/modules/oat.pdf
Slides: http://gallium.inria.fr/~remy/modules/fzip@msr2008.pdf
Towards a simpler account of modules and generativity: Abstract types have open existential types
Benoît Montagu and Didier Rémy. January 2008
Higher-order modules in System Fω and Haskell
Chung-chieh Shan. May 15, 2006
A proposal for recursive modules in Objective Caml
Xavier Leroy. 2003
http://caml.inria.fr/pub/papers/xleroy-recursive_modules-03.pdf
Phase distinctions in type theory
Luca Cardelli. 1988