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 1ML_ex(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

DOI: 10.1007/3-540-13346-1_1

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

DOI: 10.1145/800055.802036

Available at https://www.researchgate.net/profile/David_Macqueen/publication/221252232_Modules_for_Standard_ML/links/0f317532689526bea1000000/Modules-for-Standard-ML.pdf

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

DOI: 10.1145/318593.318606

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

DOI: 10.1145/512644.512669

Using dependent types to express modular structure

David B. MacQueen

POPL, pp. 277–286, 1986

DOI: 10.1145/512644.512670

Available at https://www.researchgate.net/profile/David_Macqueen/publication/2385295_Using_Dependent_Types_to_Express_Modular_Structure/links/09e415148bbf0d4470000000.pdf

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

The essence of ML

John C. Mitchell and Robert Harper

POPL, pp. 28–46, 1988

DOI: 10.1145/73560.73563

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

DOI: 10.1109/ICCL.1992.185492

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

DOI: 10.1145/143165.143206

Extending record typing to type parametric modules with sharing

María Virginia Aponte

POPL, pp. 465–478, 1993

DOI: 10.1145/158511.158704

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

DOI: 10.1145/169701.169696

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

DOI: 10.1145/174675.176927

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

DOI: 10.1145/174675.176926

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

DOI: 10.1007/3-540-57880-3_27

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

DOI: 10.1017/S0956796800001088

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

DOI: 10.1007/3-540-58450-1_53

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

DOI: 10.1093/comjnl/38.2.142

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

DOI: 10.1145/199448.199478

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

DOI: 10.1145/199448.199476

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

DOI: 10.1145/232627.232654

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

DOI: 10.1145/237721.237731

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

DOI: 10.1007/3-540-61756-6_95

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

DOI: 10.1145/263699.263735

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

DOI: 10.1007/3-540-64299-4_28

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

DOI: 10.1145/289423.289436

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

DOI: 10.1145/289423.289432

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

DOI: 10.1145/277650.277730

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

DOI: 10.1017/S0960129598002576

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

DOI: 10.1145/301618.301641

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

DOI: 10.1145/317636.317801

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

DOI: 10.1145/317636.317800

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

DOI: 10.1007/3-540-46425-5_27

Available at http://www.macs.hw.ac.uk/~jbw/papers/Wells+Vestergaard:Equational-Reasoning-for-Linking-with-First-Class-Primitive-Modules:ESOP-2000.ps.gz

Deciding type equivalence in a language with singleton kinds

Christopher Stone and Robert Harper

POPL, pp. 214–227, 2000

DOI: 10.1145/325694.325724

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

DOI: 10.1007/3-540-45332-6

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

DOI: 10.1007/3-540-46425-5_22

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

DOI: 10.1145/507635.507644

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

DOI: 10.1145/360204.360225

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

DOI: 10.1007/3-540-45927-8_2

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

DOI: 10.1017/S0956796801004257

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

DOI: 10.1145/581690.581692

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

DOI: 10.1007/3-540-45061-0_20

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

DOI: 10.1145/604131.604151

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

DOI: 10.1145/964001.964026

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

DOI: 10.1145/1086365.1086372

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

DOI: 10.1145/1086365.1086371

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

DOI: 10.1145/1086365.1086386

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

DOI: 10.1145/1086642.1086644

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

DOI: 10.1145/1159803.1159813

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

DOI: 10.1145/1159803.1159815

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

DOI: 10.1145/1183278.1183281

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

DOI: 10.1145/1190216.1190245

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

DOI: 10.1145/1227839.1227840

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

DOI: 10.1145/1291151.1291196

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

DOI: 10.1145/1411204.1411248

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/fzip@msr2008.pdf

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

DOI: 10.1145/1480881.1480926

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

DOI: 10.1145/1577824.1577829

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

DOI: 10.1007/978-3-642-16478-1_13

Available at https://www.researchgate.net/profile/David_Macqueen/publication/226219412_Engineering_Higher-Order_Modules_in_SMLNJ/links/0912f50a29752482c0000000.pdf

A true higher-order module system

George Kuan

PhD dissertation, University of Chicago, 2010

Available at http://smlnj-gforge.cs.uchicago.edu/scm/viewvc.php/*checkout*/papers/hofsem/dissertation/kuan-dissertation.pdf?root=smlnj

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

DOI: 10.1145/1708016.1708028

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

DOI: 10.1145/2048066.2048141

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

DOI: 10.1145/2450136.2450137

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

DOI: 10.1145/2535838.2535884

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

DOI: 10.1145/2784731.2784738

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

DOI: 10.1145/3009837.3009892

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

DOI: 10.1145/3314221.3314600

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