modules
modules copied to clipboard
elpinal
Implementations of F-ing modules and 1ML, as well as bibliography of (mainly ML-style) modules
Modules
Type-theoretic analysis of ML-style modules.
This repository contains
- An implementation (RRD2014.hs) of F-ing modules (Rossberg et al. 2014),
- An interpreter (Ros2018.hs) of 1MLex(Rossberg 2018), and
- A bibliography of modules and data abstraction, which is given below.
See also
- elpinal/modules-rs contains another implementation of F-ing modules in Rust (with more bugs fixed than Haskell implementation here).
1ML interpreter
stack install installs 1mlex, which is an interpreter of 1ML without type inference.
Status: All parts of [Rossberg 2018], except type inference, are implemented. There are few known bugs.
- elpinal/1ml-vim is a Vim plugin providing syntax highlighting for 1ML.
Bibliography of Modules and Data Abstraction
DISCLAIMER: There is no warranty of accuracy.
Types, abstraction and parametric polymorphism
J. C. Reynolds
Information Processing, pp. 513–523, 1983
Available at https://www.cs.cmu.edu/afs/cs/user/jcr/ftp/typesabpara.pdf
A kernel language for abstract data types and modules
R. Burstall and B. Lampson
Semantics of Data Types, pp. 1–50, 1984
Available at https://www.microsoft.com/en-us/research/wp-content/uploads/2016/11/35-KernelModules.pdf
Modules for Standard ML
David B. MacQueen
ACM Conference on LISP and Functional Programming, pp. 198–207, 1984
Modules for Standard ML
David B. MacQueen
Polymorphism Newsletter, II(2), pp. 35–71, 1985
Available at http://lucacardelli.name/Papers/Polymorphism%20Vol%20II,%20No%202.pdf
Abstract types have existential types
John C. Mitchell and Gordon D. Plotkin
POPL, pp. 37–51, 1985
On understanding types, data abstraction, and polymorphism
Luca Cardelli and P. Wegner
Brown University, CS-85-14, 1985
Available at http://lucacardelli.name/Papers/OnUnderstanding.A4.pdf
Representation independence and data abstraction
John C. Mitchell
POPL, pp. 263–276, 1986
Using dependent types to express modular structure
David B. MacQueen
POPL, pp. 277–286, 1986
A type discipline for program modules
Robert Harper, Robin Milner and Mads Tofte
TAPSOFT, pp. 308–319, 1987
DOI: 10.1007/BFb0014988
Available at https://link.springer.com/content/pdf/10.1007%2FBFb0014988.pdf
Operational semantics and polymorphic type inference
Mads Tofte
PhD dissertation, University of Edinburgh, 1988
Available at https://era.ed.ac.uk/handle/1842/6606
Persistence and type abstraction
Luca Cardelli and David B. MacQueen
Data types and persistence, pp. 31–41, 1988. First appeared in 1985
DOI: 10.1007/978-3-642-61556-6_3
Available at http://lucacardelli.name/Papers/Persistence%20and%20Type%20Abstraction.pdf
Abstract types have existential type
John C. Mitchell and Gordon D. Plotkin
ACM Transactions on Programming Languages and Systems, 10(3), pp. 470–502, 1988
DOI: 10.1145/44501.45065
Available at https://theory.stanford.edu/~jcm/papers/mitch-plotkin-88.pdf
Phase distinctions in type theory
Luca Cardelli
Manuscript, 1988
Available at http://lucacardelli.name/Papers/PhaseDistinctions.A4.pdf
A category-theoretic account of program modules
Eugenio Moggi
Category Theory and Computer Science, pp. 101–117, 1989
DOI: 10.1007/BFb0018347
Higher-order modules and the phase distinction
Robert Harper, John C. Mitchell and Eugenio Moggi
POPL, pp. 341–354, 1990
DOI: 10.1145/96709.96744
Available at http://theory.stanford.edu/people/jcm/papers/harper-mm-90.pdf
Technical Report: http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-112/ECS-LFCS-90-112.pdf
Abstract types and the dot notation
Luca Cardelli and Xavier Leroy
IFIP TC2 working conference on programming concepts and methods, pp. 479–504, 1990
Available at https://xavierleroy.org/publi/abstract-types-dot-notation.pdf
Mixin-based inheritance
Gilad Bracha and William Cook
OOPSLA/ECOOP, pp. 303–311, 1990
DOI: 10.1145/97945.97982
Available at http://www.bracha.org/oopsla90.ps
A category-theoretic account of program modules
Eugenio Moggi
Mathematical Structures in Computer Science, 1(1), pp. 103–139, 1991
DOI: 10.1017/S0960129500000074
Available at https://www.disi.unige.it/person/MoggiE/ftp/mscs91.pdf
Typeful programming
Luca Cardelli
Formal Description of Programming Concepts, 1991
Available at http://lucacardelli.name/Papers/TypefulProg.A4.pdf
An extension of Standard ML modules with subtyping and inheritance
John C. Mitchell, Sigurd Meldal and Neel Madhav
POPL, pp. 270–278, 1991
DOI: 10.1145/99583.99620
Available at https://www.researchgate.net/publication/2815527_An_extension_of_Standard_ML_modules_with_subtyping_and_inheritance
Modularity meets inheritance
Gilad Bracha and Gary Lindstrom
University of Utah, UUCS-91-017, 1991
Available at http://www.bracha.org/modularity-meets-inheritance.ps
Modularity meets inheritance
Gilad Bracha and Gary Lindstrom
International Conference on Computer Languages, pp. 282–290, 1992
The programming language JIGSAW: Mixins, modularity and multiple inheritance
Gilad Bracha
PhD dissertation, University of Utah, 1992
Available at http://www.bracha.org/jigsaw.pdf
Principal signatures for higher-order program modules
Mads Tofte
POPL, pp. 189–199, 1992
Extending record typing to type parametric modules with sharing
María Virginia Aponte
POPL, pp. 465–478, 1993
Available at https://www.researchgate.net/publication/2416181_Extending_Record_typing_to_type_parametric_modules_with_sharing
On the type structure of Standard ML
Robert Harper and John C. Mitchell
ACM Transactions on Programming Languages and Systems, 15(2), pp. 211–252, 1993
Available at https://crypto.stanford.edu/~jcm/papers/harper-mitch-TOPLAS-93.pdf
A type-theoretic approach to higher-order modules with sharing
Robert Harper and Mark Lillibridge
POPL, pp. 123–137, 1994
Available at https://www.cs.cmu.edu/~rwh/papers/sharing/popl94.pdf
Manifest types, modules, and separate compilation
Xavier Leroy
POPL, pp. 109–122, 1994
Available at https://xavierleroy.org/publi/manifest-types-popl.pdf
A semantics for higher-order functors
David B. MacQueen and Mads Tofte
Programming Languages and Systems – ESOP ’94, pp. 409–423, 1994
Available at https://rd.springer.com/content/pdf/10.1007%2F3-540-57880-3_27.pdf
Principal signatures for higher-order program modules
Mads Tofte
Journal of Functional Programming, 4(3), pp. 285–335, 1994
An implementation of higher-order functors
Pierre Crégut and David B. MacQueen
ACM SIGPLAN Workshop on ML and its Applications, 1994
Available at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.32.1516&rep=rep1&type=pdf
Studying the ML module system in HOL
Savi Maharaj and Elsa Gunter
Higher Order Logic Theorem Proving and Its Applications, pp. 346–361, 1994
Available at http://www.cs.stir.ac.uk/~sma/publications/HOLML.ps
Studying the ML module system in HOL
Elsa Gunter and Savi Maharaj
The Computer Journal, 38(2), pp. 142–151, 1995
Available at http://www.cs.stir.ac.uk/~sma/publications/CJ.ps
Higher-order functors with transparent signatures
Sandip K. Biswas
POPL, pp. 154–163, 1995
Available at http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.14.9123&rep=rep1&type=pdf
Applicative functors and fully transparent higher-order modules
Xavier Leroy
POPL, pp. 142–153, 1995
Available at https://xavierleroy.org/publi/applicative-functors.pdf
From Hindley-Milner types to first-class structures
Mark P. Jones
The Haskell workshop, 1995
Available at http://web.cecs.pdx.edu/~mpj/pubs/haskwork95.pdf
Mixin modules
Dominic Duggan and Constantinos Sourelis
ICFP, pp. 262–273, 1996
Available at https://www.cs.tufts.edu/~nr/cs257/archive/dominic-duggan/Mixin%20Modules.pdf
Using parameterized signatures to express modular structure
Mark P. Jones
POPL, pp. 66–78, 1996
Available at https://web.cecs.pdx.edu/~mpj/pubs/paramsig.pdf
A syntactic theory of type generativity and sharing
Xavier Leroy
Journal of Functional Programming, 6(5), pp. 667–698, 1996
DOI: 10.1017/S0956796800001933
Available at https://xavierleroy.org/publi/syntactic-generativity.pdf
An exploration of modular programs
Jan Nicklish and Simon Peyton Jones
Glasgow Workshop on Functional Programming, 1996
Available at https://www.microsoft.com/en-us/research/wp-content/uploads/1996/01/Nicklisch-modules.pdf
Type isomorphisms for module signatures
María-Virginia Aponte and Roberto Di Cosmo
Programming Languages Implementation and Logic Programming, pp. 334–346, 1996
Available at http://www.dicosmo.org/Articles/1996-AponteDiCosmo-PLILP.pdf
Standard ML type generativity as existential quantification
Claudio V. Russo
University of Edinburgh, ECS-LFCS-96-344, 1996
Available at http://www.dcs.ed.ac.uk/home/cvr/ECS-LFCS-96-344.pdf
A module system for LOOM
Leaf Eames Petersen
Undergraduate dissertation, Williams College, 1996
Available at http://www.leafpetersen.com/leaf/publications/loom_thesis/thesis.pdf
Type systems for modular programs and specifications
David R. Aspinall
PhD dissertation, Edinburgh University, Edinburgh, Scotland, 1997
Available at https://www.era.lib.ed.ac.uk/handle/1842/11587
Program fragments, linking, and modularization
Luca Cardelli
POPL, pp. 266–277, 1997
Available at http://lucacardelli.name/Papers/Linking.A4.pdf
An applicative module calculus
Judicaël Courant
TAPSOFT, 1997
DOI: 10.1007/BFb0030630
Available at https://link.springer.com/content/pdf/10.1007%2FBFb0030630.pdf
Translucent sums: A foundation for higher-order module systems
Mark Lillibridge
PhD dissertation, Carnegie Mellon University, 1997
Available at https://www.cs.cmu.edu/Groups/fox/papers/mdl-thesis.ps
An interpretation of Standard ML in type theory
Robert Harper and Christopher Stone
Carnegie Mellon University, CMU-CS-97-147, 1997
Available at https://www.cs.cmu.edu/Groups/fox/papers/sml96-v3.ps
Elaboration and phase-splitting in the TIL/ML compiler
Christopher Stone
IC Research Symposium, 1997
Available at http://www.cs.cmu.edu/~fox/foxnet/people/cstone/papers/ic97.ps
An algebra of mixin modules
Davide Ancona and Elena Zucca
International Workshop on Algebraic Development Techniques, pp. 92–106, 1997
Types for modules
Claudio V. Russo
PhD dissertation, University of Edinburgh, UK, 1998
Available at http://www.dcs.ed.ac.uk/home/cvr/ECS-LFCS-98-389.pdf
Typed cross-module compilation
Zhong Shao
ICFP, pp. 141–152, 1998
Available at http://flint.cs.yale.edu/flint/publications/tcc.pdf
Technical Report: http://flint.cs.yale.edu/flint/publications/tcc-tr.pdf
Parameterized modules, recursive modules and mixin modules
Dominic Duggan and Constantinos Sourelis
ACM SIGPLAN Workshop on ML, pp. 87–96, 1998
Type-theoretic methodology for practical programming languages
Karl Fredrick Crary
PhD dissertation, Cornell University, 1998
Available at http://www.cs.cmu.edu/~crary/papers/1998/thesis/thesis.ps.gz
Programming language semantics in foundational type theory
Karl Crary
International Conference on Programming Concepts and Methods, pp. 107–125, 1998
DOI: 10.1007/978-0-387-35358-6_11
Available at http://www.cs.cmu.edu/~crary/papers/1998/tt-semant/tt-semant.ps.gz
Technical Report: http://www.cs.cmu.edu/~crary/papers/1998/tt-semant/tt-semant-tr.ps.gz
Modular object-oriented programming with units and mixins
Robert Bruce Findler and Matthew Flatt
ICFP, pp. 94–104, 1998
Available at https://www2.ccs.neu.edu/racket/pubs/icfp98-ff.pdf
Units: Cool modules for HOT languages
Matthew Flatt and Matthias Felleisen
PLDI, pp. 236–248, 1998
Available at http://www.ccs.neu.edu/scheme/pubs/pldi98-ff.ps.gz
A theory of mixin modules: Basic and derived operators
Davide Ancona and Elena Zucca
Mathematical Structures in Computer Science, 8(4), pp. 401–446, 1998
A primitive calculus for module systems
Davide Ancona and Elena Zucca
Principles and Practice of Declarative Programming, pp. 62–79, 1999
DOI: 10.1007/10704567_4
What is a recursive module?
Karl Crary, Robert Harper and Sidd Puri
PLDI, pp. 50–63, 1999
Available at http://www.cs.cmu.edu/~crary/papers/1999/recmod/recmod.ps.gz
Non-dependent types for Standard ML modules
Claudio V. Russo
Principles and Practice of Declarative Programming, pp. 80–97, 1999
DOI: 10.1007/10704567_5
Available at https://www.microsoft.com/en-us/research/wp-content/uploads/1999/09/Non-Dependent-Types-for-Standard-ML-Modules.pdf
Transparent modules with fully syntactic signatures
Zhong Shao
ICFP, pp. 220–232, 1999
Available at http://flint.cs.yale.edu/flint/publications/fullsig.pdf
Technical Report: http://flint.cs.yale.edu/flint/publications/fullsig-tr.pdf
Program modules, separate compilation, and intermodule optimisation
Martin Elsman
PhD dissertation, Department of Computer Science, University of Copenhagen, 1999
Available at https://elsman.com/pdf/phd.pdf
Static interpretation of modules
Martin Elsman
ICFP, pp. 208–219, 1999
Available at https://elsman.com/pdf/icfp99.pdf
Equational reasoning for linking with first-class primitive modules
J. B. Wells and René Vestergaard
Programming Languages and Systems, pp. 412–428, 2000
Deciding type equivalence in a language with singleton kinds
Christopher Stone and Robert Harper
POPL, pp. 214–227, 2000
Available at http://www.cs.cmu.edu/~rwh/papers/singletons/popl99.pdf
Technical Report (1999): http://reports-archive.adm.cs.cmu.edu/anon/1999/CMU-CS-99-155.pdf
Sound and complete elimination of singleton kinds
Karl Crary
Workshop on Types in Compilation, pp. 1–25, 2000
Available at http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-161D.pdf
Technical Report: http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-104.pdf
Singleton kinds and singleton types
Christopher Stone
PhD dissertation, Carnegie Mellon University, 2000
Available at http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-153.pdf
Implementing the TILT internal language
Leaf Petersen, Perry Cheng, Robert Harper and Christopher Stone
Carnegie Mellon University, CMU-CS-00-180, 2000
Available at http://reports-archive.adm.cs.cmu.edu/anon/2000/CMU-CS-00-180.pdf
A type-theoretic interpretation of Standard ML
Robert Harper and Christopher Stone
Proof, language, and interaction: Essays in honor of robin milner, MIT Press, 2000
Available at https://www.cs.cmu.edu/~rwh/papers/ttisml/ttisml.pdf
A modular module system
Xavier Leroy
Journal of Functional Programming, 10(3), pp. 269–303, 2000
DOI: 10.1017/S0956796800003683
Available at https://xavierleroy.org/publi/modular-modules-jfp.pdf
First-class structures for Standard ML
Claudio V. Russo
European Symposium on Programming, pp. 336–350, 2000
Available at https://link.springer.com/content/pdf/10.1007%2F3-540-46425-5_22.pdf
Recursive structures for Standard ML
Claudio V. Russo
ICFP, pp. 50–61, 2001
Available at https://www.microsoft.com/en-us/research/wp-content/uploads/2001/09/Recursive-Structures-for-Standard-ML.pdf
Toward a practical type theory for recursive modules
Derek Dreyer, Robert Harper and Karl Crary
Carnegie Mellon University, School of Computer Science, CMU-CS-01-112, 2001
Available at https://www.cs.cmu.edu/~rwh/papers/ttrm/rmtr.pdf
Modules, abstract types, and distributed versioning
Peter Sewell
POPL, pp. 236–247, 2001
Available at https://www.cl.cam.ac.uk/~pes20/versions-popl.pdf
Mixin modules in a call-by-value setting
Tom Hirschowitz and Xavier Leroy
European Symposium on Programming, pp. 6–20, 2002
Available at https://xavierleroy.org/publi/mixins-cbv-esop2002.pdf
A calculus of module systems
Davide Ancona and Elena Zucca
Journal of Functional Programming, 12(2), pp. 91–132, 2002
First-class modules for Haskell
Mark Shields and Simon Peyton Jones
Foundations of Object-Oriented Languages, 2002
Available at https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/first_class_modules.pdf
A formal specification of the Haskell 98 module system
Iavor S. Diatchki, Mark P. Jones and Thomas Hallgren
ACM SIGPLAN 2002 Haskell Workshop, pp. 17–28, 2002
Available at http://web.cecs.pdx.edu/~mpj/pubs/hsmods.pdf
Mixin modules and computational effects
Davide Ancona, Sonia Fagorzi, Eugenio Moggi and Elena Zucca
ICALP, pp. 224–238, 2003
Available at https://www.disi.unige.it/person/MoggiE/ftp/icalp03.pdf
A proposal for recursive modules in Objective Caml
Xavier Leroy
Manuscript, 2003
Available at http://caml.inria.fr/pub/papers/xleroy-recursive_modules-03.pdf
A type system for higher-order modules
Derek Dreyer, Karl Crary and Robert Harper
POPL, pp. 236–249, 2003
Available at http://www.cs.cmu.edu/~crary/papers/2003/thoms/thoms.pdf
Technical Report: http://www.cs.cmu.edu/~crary/papers/2003/thoms/thoms-tr.pdf
Types for modules
Claudio V. Russo
Electronic Notes in Theoretical Computer Science, 60, 2003
DOI: 10.1016/S1571-0661(05)82621-0
Available at https://www.microsoft.com/en-us/research/wp-content/uploads/1998/03/Types-for-Modules.pdf
A type system for well-founded recursion
Derek Dreyer
POPL, pp. 293–305, 2004
Available at https://people.mpi-sws.org/~dreyer/papers/recursion/popl.pdf
Technical Report (with Robert Harper and Karl Crary, 2003): https://people.mpi-sws.org/~dreyer/papers/recursion/tr/main.pdf
Understanding and evolving the ML module system
Derek Dreyer
PhD dissertation, Carnegie Mellon University, Pittsburgh, Pennsylvania, 2005
Available at https://people.mpi-sws.org/~dreyer/thesis/main.pdf
Recursive type generativity
Derek Dreyer
ICFP, pp. 41–53, 2005
Available at https://people.mpi-sws.org/~dreyer/papers/dps/main.pdf
Type generativity in higher-order module systems
Paul Govereau
Harvard Computer Science Group, TR-05-05, 2005
Available at https://dash.harvard.edu/bitstream/handle/1/23853816/tr-05-05.pdf
An expressive language of signatures
Norman Ramsey, Kathleen Fisher and Paul Govereau
ICFP, pp. 27–40, 2005
Available at https://www.cs.tufts.edu/~nr/pubs/els.pdf
Recursive object-oriented modules
Keiko Nakata, Akira Ito and Jacques Garrigue
Foundations of Object-Oriented Languages, 2005
Available at http://www.math.nagoya-u.ac.jp/~garrigue/papers/fool_2005.pdf
Extended version: http://www.kurims.kyoto-u.ac.jp/~keiko/papers/room_ext.pdf
Recursion for structured modules
Keiko Nakata
JSSST Workshop on Programming and Programming Languages, 2005
Available at http://www.kurims.kyoto-u.ac.jp/~keiko/papers/ppl05.pdf
Type inference, principal typings, and let-polymorphism for first-class mixin modules
Henning Makholm and J. B. Wells
ICFP, pp. 156–167, 2005
Available at http://henning.makholm.net/papers/icfp2005.pdf
Mixin modules in a call-by-value setting
Tom Hirschowitz and Xavier Leroy
ACM Transactions on Programming Languages and Systems, 27(5), pp. 857–881, 2005
Available at https://xavierleroy.org/publi/mixins-cbv-toplas.pdf
Certifying compilation for Standard ML in a type analysis framework
Leaf Eames Petersen
PhD dissertation, Carnegie Mellon University, 2005
Available at http://www.leafpetersen.com/leaf/publications/thesis/main.pdf
Path resolution for recursive modules
Keiko Nakata
Kyoto University, RIMS-1545, 2006
Available at http://www.kurims.kyoto-u.ac.jp/preprint/file/RIMS1545.pdf
Recursive modules for programming
Keiko Nakata and Jacques Garrigue
ICFP, pp. 74–86, 2006
Available at http://www.math.nagoya-u.ac.jp/~garrigue/papers/nakata-icfp2006.pdf
Technical Report: http://www.kurims.kyoto-u.ac.jp/preprint/file/RIMS1546.pdf
From structures and functors to modules and units
Scott Owens and Matthew Flatt
ICFP, pp. 87–98, 2006
Available at http://www.cs.utah.edu/plt/publications/icfp06-of.pdf
Practical type theory for recursive modules
Derek Dreyer
University of Chicago, Department of Computer Science, TR-2006-07, 2006
Available at https://people.mpi-sws.org/~dreyer/papers/bimod/main.pdf
Higher-order modules in System Fω and Haskell
Chung-chieh Shan
Manuscript, May 15, 2006
Available at http://homes.soic.indiana.edu/ccshan/xlate/xlate.pdf
Extensional equivalence and singleton types
Christopher Stone and Robert Harper
Transactions on Computational Logic, 7(4), pp. 676–722, 2006
Available at http://www.cs.cmu.edu/~rwh/papers/singletons/tocl.pdf
Mechanizing the metatheory of Standard ML
Daniel K. Lee, Karl Crary and Robert Harper
Carnegie Mellon University, School of Computer Science, CMU-CS-06-138, 2006
Available at http://www.cs.cmu.edu/~dklee/papers/tslf.pdf
Slides: https://www.seas.upenn.edu/~sweirich/wmm/wmm06/lee-talk.pdf
Towards a mechanized metatheory of Standard ML
Daniel K. Lee, Karl Crary and Robert Harper
POPL, pp. 173–184, 2007
Available at http://www.cs.cmu.edu/~dklee/papers/tslf-popl.pdf
Sound and complete elimination of singleton kinds
Karl Crary
Transactions on Computational Logic, 8(2), 2007
Available at https://www.cs.cmu.edu/~crary/papers/2005/singelim.pdf
A type system for recursive modules
Derek Dreyer
ICFP, pp. 289–302, 2007
Available at https://people.mpi-sws.org/~dreyer/papers/recmod/main-short.pdf
Technical Report: https://people.mpi-sws.org/~dreyer/papers/recmod/main-long.pdf
Recursive type generativity
Derek Dreyer
Journal of Functional Programming, 17(4&5), pp. 433–471, 2007
DOI: 10.1017/S0956796807006429
Available at https://people.mpi-sws.org/~dreyer/papers/dps/jfp.pdf
Principal type schemes for modular programs
Derek Dreyer and Matthias Blume
European Symposium on Programming, pp. 441–457, 2007
DOI: 10.1007/978-3-540-71316-6_30
Available at https://people.mpi-sws.org/~dreyer/papers/infmod/main-short.pdf
Technical Report: https://people.mpi-sws.org/~dreyer/papers/infmod/main-long.pdf
Modular type classes
Derek Dreyer, Robert Harper and Manuel M. T. Chakravarty
POPL, pp. 63–70, 2007
DOI: https://doi.org/10.1145/1190216.1190229
Available at https://people.mpi-sws.org/~dreyer/papers/mtc/main-short.pdf
Technical Report (with Gabriele Keller, 2006): https://newtraell.cs.uchicago.edu/files/tr_authentic/TR-2006-09.pdf
A module system with applicative functors and recursive path references
Keiko Nakata
PhD dissertation, Kyoto University, 2007
Available at http://www.kurims.kyoto-u.ac.jp/preprint/file/RIMS1583.pdf
Path resolution for recursive nested modules is undecidable
Keiko Nakata and Jacques Garrigue
9th International Workshop on Termination, 2007
Available at http://www.math.nagoya-u.ac.jp/~garrigue/papers/wst2007.pdf
Mixin’ up the ML module system
Derek Dreyer and Andreas Rossberg
ICFP, pp. 307–320, 2008
Available at https://people.mpi-sws.org/~rossberg/mixml/mixml-icfp08.pdf
Technical Report: https://people.mpi-sws.org/~rossberg/mixml/mixml-icfp08-extended.pdf
Towards a simpler account of modules and generativity: Abstract types have open existential types
Benoît Montagu and Didier Rémy
Manuscript, January 2008
Available at http://gallium.inria.fr/~remy/modules/fzip.pdf
A logical account of type generativity: Abstract types have open existential types
Benoît Montagu and Didier Rémy
Manuscript, April 14, 2008
Available at http://gallium.inria.fr/~remy/modules/oat.pdf
Slides: http://gallium.inria.fr/~remy/modules/[email protected]
Lazy mixins and disciplined effects
Keiko Nakata
Manuscript, 2008
Available at http://cs.ioc.ee/~keiko/papers/Lyre08.pdf
Lazy modules: A lazy evaluation strategy for more recursive initialization patterns
Keiko Nakata
Manuscript, 2008
Available at http://cs.ioc.ee/~keiko/papers/OsanLong.pdf
Modeling abstract types in modules with open existential types
Benoît Montagu and Didier Rémy
POPL, pp. 354–365, 2009
Available at http://gallium.inria.fr/~remy/modules/Montagu-Remy@popl09:fzip.pdf
A syntactic account of singleton types via hereditary substitution
Karl Crary
Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pp. 21–29, 2009
Available at https://www.cs.cmu.edu/~crary/papers/2009/synsing.pdf
Engineering higher-order modules in SML/NJ
George Kuan and David B. MacQueen
Implementation and Application of Functional Languages, pp. 218–235, 2009
A true higher-order module system
George Kuan
PhD dissertation, University of Chicago, 2010
Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types
Benoît Montagu
PhD dissertation, Ecole Polytechnique X, 2010
Available at https://pastel.archives-ouvertes.fr/tel-00550331/document
A flattening strategy for SML module compilation and its implementation
Liu Bochao and Atsushi Ohori
Information and Media Technologies, 5(1), pp. 58–76, 2010
DOI: 10.11185/imt.5.58
Available at https://www.jstage.jst.go.jp/article/imt/5/1/5_1_58/_pdf/-char/en
F-ing modules
Andreas Rossberg, Claudio V. Russo and Derek Dreyer
Types in Language Design and Implementation, pp. 89–102, 2010
Available at https://people.mpi-sws.org/~rossberg/f-ing/f-ing.pdf
First-class modules and composable signatures in Objective Caml 3.12
Alain Frisch and Jacques Garrigue
ML Workshop, 2010
Available at http://www.math.nagoya-u.ac.jp/~garrigue/papers/ml2010.pdf
Slides: http://www.math.nagoya-u.ac.jp/~garrigue/papers/ml2010-show.pdf
A syntactic type system for recursive modules
Hyeonseung Im, Keiko Nakata, Jacques Garrigue and Sungwoo Park
Object-oriented Programming, Systems, Languages, and Applications, 2011
Available at http://www.math.nagoya-u.ac.jp/~garrigue/papers/oopsla2011.pdf
Path resolution for nested recursive modules
Jacques Garrigue and Keiko Nakata
Higher-Order and Symbolic Computation, 24(3), pp. 207–237, 2012
DOI: 10.1007/s10990-012-9083-6
Available at http://www.math.nagoya-u.ac.jp/~garrigue/papers/path-resolution-1205.pdf
Mixin’ up the ML module system
Andreas Rossberg and Derek Dreyer
ACM Transactions on Programming Languages and Systems, 35(1), 2013
Available at https://people.mpi-sws.org/~rossberg/mixml/mixml-toplas.pdf
Contractive signatures with recursive types, type parameters, and abstract types
Hyeonseung Im, Keiko Nakata and Sungwoo Park
ICALP, pp. 299–311, 2013
DOI: 10.1007/978-3-642-39212-2_28
Available at http://pl.postech.ac.kr/~gla/paper/icalp2013.pdf
F-ing modules
Andreas Rossberg, Claudio V. Russo and Derek Dreyer
Journal of Functional Programming, 24(5), 2014
DOI: 10.1017/S0956796814000264
Available at https://people.mpi-sws.org/~rossberg/f-ing/f-ing-jfp.pdf
Backpack: Retrofitting Haskell with interfaces
Scott Kilpatrick, Derek Dreyer, Simon Peyton Jones and Simon Marlow
POPL, pp. 19–31, 2014
Available at https://people.mpi-sws.org/~dreyer/papers/backpack/paper.pdf
Slides: https://plv.mpi-sws.org/backpack/backpack-popl.pdf
Appendix: https://people.mpi-sws.org/~dreyer/papers/backpack/appendix.pdf
Type-level module aliases: independent and equal
Jacques Garrigue and Leo P. White
ML Family Workshop, 2014
Available at http://www.math.nagoya-u.ac.jp/~garrigue/papers/modalias.pdf
Slides: http://www.math.nagoya-u.ac.jp/~garrigue/papers/modalias-show.pdf
1ML — Core and modules united (F-ing first-class modules)
Andreas Rossberg
ICFP, pp. 35–47, 2015
Available at https://people.mpi-sws.org/~rossberg/1ml/1ml.pdf
Technical Report: https://people.mpi-sws.org/~rossberg/1ml/1ml-extended.pdf
1ML with special effects (F-ing generativity polymorphism)
Andreas Rossberg
WadlerFest, 2016
DOI: 10.1007/978-3-319-30936-1_18
Available at https://people.mpi-sws.org/~rossberg/1ml/1ml-effects.pdf
Slides: https://events.inf.ed.ac.uk/wf2016/slides/rossberg.pdf
Backpack to work: Towards practical mixin linking for Haskell
Simon Peyton Jones, Edward Yang, Scott Kilpatrick and Derek Dreyer
Manuscript, March 2016
Available at https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/backpack-2016.pdf
Backpack: Towards practical mix-in linking in Haskell
Edward Z. Yang
PhD dissertation, Stanford University, June 2017
Available at https://github.com/ezyang/thesis/releases
Extending OCaml's open (extended abstract)
Runhang Li and Jeremy Yallop
The OCaml Users and Developers Workshop, 2017
Available at https://www.cl.cam.ac.uk/~jdy22/papers/extending-ocamls-open.pdf
Modules, abstraction, and parametric polymorphism
Karl Crary
POPL, pp. 100–113, 2017
Available at http://www.cs.cmu.edu/~crary/papers/2017/mapp.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
ICFP, pp. 1–30, 2018
DOI: 10.1145/3236792
Available at https://futhark-lang.org/publications/icfp18.pdf
1ML — Core and modules united
Andreas Rossberg
Journal of Functional Programming, 28, e22, 2018
DOI: 10.1017/S0956796818000205
Available at https://people.mpi-sws.org/~rossberg/papers/Rossberg%20-%201ML%20--%20Core%20and%20modules%20united%20[JFP].pdf
Fully abstract module compilation
Karl Crary
POPL, 3(POPL), pp. 10:1–10:29, 2019
DOI: 10.1145/3290323
Available at https://dl.acm.org/ft_gateway.cfm?id=3290323
Slides: https://popl19.sigplan.org/event/popl-2019-research-papers-fully-abstract-module-compilation
Characterising renaming within OCaml’s module system: Theory and implementation
Reuben N. S. Rowe, Hugo Férée, Simon J. Thompson and Scott Owens
PLDI, pp. 950–965, 2019
Available at https://www.cs.kent.ac.uk/people/staff/rnsr/docs/renaming-pldi2019.pdf
Extending OCaml's open
Runhang Li and Jeremy Yallop
ML & OCaml 2017 post-proceedings, pp. 1–14, 2019
DOI: 10.4204/EPTCS.294.1
Available at https://www.cl.cam.ac.uk/~jdy22/papers/extending-ocamls-open-draft.pdf
A focused solution to the avoidance problem
Karl Crary
Journal of Functional Programming, 30, e24, 2020
DOI: 10.1017/S0956796820000222
Available at http://www.cs.cmu.edu/~crary/papers/2020/exsig.pdf
A metalanguage for multi-phase modularity
Jonathan Sterling and Robert Harper
ML Family Workshop, 2021
Available at https://www.jonmsterling.com/papers/sterling-harper-2021-mlw.pdf
Slides: https://www.jonmsterling.com/slides/sterling-harper-2021-mlw.pdf
Logical relations as types: Proof-relevant parametricity for program modules
Jonathan Sterling and Robert Harper
Journal of the ACM, 68(6), pp. 1–47, 2021
DOI: 10.1145/3474834
Available at https://www.jonmsterling.com/papers/sterling-harper-2021.pdf
Slides 1: https://www.cs.cmu.edu/~rwh/talks/paramstr.pdf
Slides 2: https://www.jonmsterling.com/slides/sterling-2021-au-ccs.pdf
OCaml modules: formalization, insights and improvements: Bringing the existential types into a generative subset
Clément Blaudeau
Master dissertation, École polytechnique fédérale de Lausanne, 2021
Available at https://hal.inria.fr/hal-03526068/file/main.pdf
Reflections on existential types
Jonathan Sterling
Manuscript, 2022
Available at https://www.jonmsterling.com/papers/sterling-2022-existentials.pdf
Retrofitting OCaml modules: Fixing signature avoidance in the generative case
Clément Blaudeau, Didier Rémy and Gabriel Radanne
Journées Francophones des Langages Applicatifs, pp. 59–100, 2023
Available at https://hal.inria.fr/hal-03936636v2/file/main.pdf
elpinal