Types for Modules

No abstract is available for this paper.

• Publication year

  2004

• Venue

  Electronical Notes in Theoretical Computer Science

• Publication date

  2004-04-01

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1016/S1571-0661(05)82621-0
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• A modular module system

  2000cited by this paper
• First-Class Structures for Standard ML

  2000cited by this paper
• Program modules, separate compilation, and intermodule optimisation

  1999cited by this paper
• A Module Calculus for Pure Type Systems

  1997cited by this paper
• Foundations for Programming Languages by John C. Mitchell, MIT Press, 1996.

  1997cited by this paper
• Translucent Sums: A Foundation for Higher-Order Module Systems

  1997cited by this paper
• The Definition of Extended ML: A Gentle Introduction

  1997cited by this paper
• An Interpretation of Standard ML in Type Theory

  1997influential reference
• An Applicative Module Calculus

  1997cited by this paper
• A syntactic theory of type generativity and sharing

  1996influential reference
• Using parameterized signatures to express modular structure

  1996cited by this paper
• An Exploration of Modular Programs

  1996cited by this paper
• Standard ML Type Generativity as Existential Quantification

  1996cited by this paper
• A Type-Theoretic Account of Standard ML 1996 (Version 1).

  1996influential reference
• Generic functional programming with types and relations

  1996cited by this paper
• Applicative functors and fully transparent higher-order modules

  1995cited by this paper
• Implémentation d'un système de modules évolué en Caml-Light

  1995cited by this paper
• Higher-order functors with transparent signatures

  1995influential reference
• Studying the ML Module System in HOL

  1994influential reference
• A type-theoretic approach to higher-order modules with sharing

  1994influential reference
• Type classes in Haskell

  1994cited by this paper
• A Semantics for Higher-Order Functors

  1994influential reference
• Principal signatures for higher-order program modules

  1994cited by this paper
• The Quest Language and System

  1994cited by this paper
• Manifest types, modules, and separate compilation

  1994influential reference
• Pure Type Systems Formalized

  1993cited by this paper
• On the type structure of standard ML

  1993influential reference
• Extending record typing to type parametric modules with sharing

  1993cited by this paper
• BOOK REVIEW: ML for the Working Programmer by Laurence C. Paulson: (Cambridge University Press, 429 pp., 1991)

  1992cited by this paper
• Unification Under a Mixed Prefix

  1992cited by this paper
• An algorithm for testing conversion in type theory

  1991influential reference
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification

  1991cited by this paper
• Type theory and functional programming

  1991cited by this paper
• A semantic basis for quest

  1990cited by this paper
• Commentary on standard ML

  1990cited by this paper
• An extended calculus of constructions

  1990cited by this paper
• Abstract Types and the Dot Notation

  1990cited by this paper
• Definition of standard ML

  1990influential reference
• ECC, an extended calculus of constructions

  1989cited by this paper
• Typeful Programming

  1989cited by this paper
• Higher-order modules and the phase distinction

  1989cited by this paper
• Phase Distinctions in Type Theory

  1988cited by this paper
• Abstract types have existential type

  1988influential reference
• Pebble, a Kernel Language for Modules and Abstract Data Types

  1988cited by this paper
• Operational Semantics and Polymorphic Type Inference

  1988influential reference
• Impredicative Strong Existential Equivalent to Type:Type

  1986cited by this paper
• Using dependent types to express modular structure

  1986influential reference
• Programming in Modula-2

  1985cited by this paper
• A Kernel Language for Abstract Data Types and Modules

  1984cited by this paper
• Type assignment in programming languages

  1984cited by this paper
• Principles of programming languages

  1981cited by this paper
• A Theory of Type Polymorphism in Programming

  1978influential reference
• Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem

  1972cited by this paper
• The formulae-as-types notion of construction

  1969cited by this paper
• A Machine-Oriented Logic Based on the Resolution Principle

  1965cited by this paper
• Combinatory Logic, Volume I

  1959cited by this paper

• Avoiding Signature Avoidance in ML Modules with Zippers

  2025influential citation
• The existential fragment of second-order propositional intuitionistic logic is undecidable

  2024influential citation
• Fulfilling OCaml Modules with Transparency

  2024cites this paper
• Fulfilling OCaml modules with transparent existentials

  2023cites this paper
• Fulfilling OCaml modules with transparent existentials

  2023cites this paper
• A focused solution to the avoidance problem

  2020influential citation
• The history of Standard ML

  2020cites this paper
• Fully abstract module compilation

  2019cites this paper
• Hygienic Source-Code Generation Using Functors - (Extended Abstract)

  2018cites this paper
• 1ML – Core and modules united

  2018influential citation
• Modules, abstraction, and parametric polymorphism

  2017cites this paper
• 1ML with Special Effects - F-ing Generativity Polymorphism

  2016cites this paper
• 1ML – core and modules united (F-ing first-class modules)

  2015influential citation
• Backpack: retrofitting Haskell with interfaces

  2014cites this paper
• Mixin’ Up the ML Module System

  2013cites this paper
• Foundations of Algebraic Specification and Formal Software Development

  2012cites this paper
• F-ing applicative functors

  2012cites this paper
• A Flattening Strategy for SML Module Compilation and Its Implementation

  2010cites this paper
• Programming with first-class modules in a core language with subtyping, singleton kinds and open existential types. (Programmer avec des modules de première classe dans un langage noyau pourvu de sous-typage, sortes singletons et types existentiels ouverts)

  2010cites this paper
• Développement modulaire de théories et gestion de l'espace de nom pour l'assistant de preuve Coq. (Modular development of theories and name-space management for the Coq proof assistant)

  2010cites this paper
• Engineering Higher-Order Modules in SML/NJ

  2009influential citation
• On the Decidability of Subtyping with Bounded Existential Types and Implementation Constraints

  2009cites this paper
• Modeling abstract types in modules with open existential types

  2009influential citation
• True Higher-Order Modules , Separate Compilation , and Signature Calculi ∗

  2009cites this paper
• A syntactic account of singleton types via hereditary substitution

  2009cites this paper
• A Framework for Cut-Off Incremental Recompilation and Inter-Module Optimization

  2008cites this paper
• Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions

  2008cites this paper
• Mixin' up the ML module system

  2008cites this paper
• Towards a Simpler Account of Modules and Generativity : Abstract Types have Open Existential Types

  2008cites this paper
• Dynamic Translucency with Abstraction Kinds

  2008cites this paper
• Towards a Simpler Account of Modules and Generativity : Abstract Types have Open Existential Types . Benoı̂t Montagu INRIA

  2008cites this paper
• Mei-A Module System for Mechanized Mathematics Systems

  2008cites this paper
• Abstract types in distributed systems A partial translation of my Ph.D. dissertation

  2008cites this paper
• ML Modules and Haskell Type Classes: A Constructive Comparison

  2008cites this paper
• A Logical Account of Type Generativity : Abstract types have open existential types

  2008cites this paper
• Typed open programming: a higher-order, typed approach to dynamic modularity and distribution

  2007cites this paper
• Lightweight Static Capabilities

  2007cites this paper
• Principal Type Schemes for Modular Programs

  2007influential citation
• A type system for recursive modules

  2007cites this paper
• Application of Category-Theory Methods to the Design of a System of Modules for a Functional Programming Language

  2006cites this paper
• $\mathcal{MC}_2$ A module calculus for Pure Type Systems

  2006cites this paper
• Practical Type Theory for Recursive Modules

  2006cites this paper
• Type Generativity in Higher-Order Module Systems

  2005cites this paper
• Understanding and evolving the ml module system

  2005influential citation
• Trends in Functional Programming

  2005cites this paper
• Understanding and Evolving the ML Module System ( Thesis Summary )

  2005influential citation
• Higher-order modules in System F ω and

  2004influential citation
• Advanced Topics In Types And Programming Languages

  2004cites this paper
• Theories of information hiding in lambda-calculus : logical relations and bisimulations for encryption and type abstraction

  2004cites this paper
• PROGRAMMING LANGUAGE ABSTRACTIONS FOR EXTENSIBLE SOFTWARE COMPONENTS

  2004cites this paper
• Alice through the looking glass

  2004influential citation
• Generativity and dynamic opacity for abstract types

  2003influential citation
• Environment classifiers

  2003cites this paper
• Generativity and dynamic opacity for abstract types (extended version)

  2003cites this paper
• Environment Classifiers Extended

  2003cites this paper
• Typed operational semantics for higher-order subtyping

  2003cites this paper
• The Extension of ML with Hypothetical Views for Discovery Science: Formalization and Implementation

  2003cites this paper
• A type system for higher-order modules

  2003cites this paper
• A reduction semantics for call-by-value mixin modules

  2002cites this paper
• Dynamic opacity for abstract types

  2002cites this paper
• VM lambda: a Functional Calculus for Scientific Discovery

  2002cites this paper
• Type-Safe Prototype-Based Component Evolution

  2002cites this paper
• A calculus of module systems

  2002cites this paper
• First class modules for Haskell

  2002cites this paper
• Thesis Proposal: Effective Type Theory for Modularity

  2002cites this paper
• Nested Types

  2001cites this paper
• Modules, abstract types, and distributed versioning

  2001cites this paper
• Notes on Programming Standard ML of New Jersey (version 110.0.6)

  2001cites this paper
• Recursive structures for standard ML

  2001cites this paper
• Named Instances for Haskell Type Classes

  2001cites this paper
• Abstract machines for dynamic computation

  2001cites this paper
• Recursive structures for standard ML

  2001cites this paper
• Programming Languages and Systems

  2000cites this paper
• First-Class Structures for Standard ML

  2000influential citation
• Using, Understanding, and Unraveling the OCaml Language. From Practice to Theory and Vice Versa

  2000cites this paper
• Equational Reasoning for Linking with First-Class Primitive Modules

  2000cites this paper
• Moscow ML Owner's Manual

  2000cites this paper
• An Introduction to Dependent Type Theory

  2000cites this paper
• Relating Cryptography and Polymorphism

  2000cites this paper
• A modular module system

  2000cites this paper
• Non-dependent Types for Standard ML Modules

  1999influential citation
• Program modules, separate compilation, and intermodule optimisation

  1999cites this paper
• Title: Non-dependent Types for Standard Ml Modules Non-dependent Types for Standard Ml Modules

  1999cites this paper
• TransparentModuleswith Fully SyntacticSignatures

  1999cites this paper
• Static interpretation of modules

  1999cites this paper
• Transparent modules with fully syntatic signatures

  1999cites this paper
• First-Class Structures for Standard ML ( Extended Summary )

  1999influential citation
• Algebraic Specification and Program Development by Stepwise Refinement

  1999cites this paper
• Type Systems, Software Architecture and Testing

  1998cites this paper
• Applicative Notions in ML-like Programs

  1998cites this paper
• Progress Report of the Max Planck Institute for Software Systems (mpi-sws)

  year unknowncites this paper
• Evolving the ML Module System

  year unknowncites this paper
• Under Consideration for Publication in J. Functional Programming a Module Calculus for Pure Type Systems

  year unknowninfluential citation
• Under Consideration for Publication in J. Functional Programming F-ing Modules

  year unknowninfluential citation
• Fulfilling OCaml modules with transparency

  year unknowninfluential citation