diff --git a/docs/codeql/ql-language-reference/ql-language-specification.rst b/docs/codeql/ql-language-reference/ql-language-specification.rst
index 71dcbdce571..32244023c21 100644
--- a/docs/codeql/ql-language-reference/ql-language-specification.rst
+++ b/docs/codeql/ql-language-reference/ql-language-specification.rst
@@ -199,24 +199,37 @@ Kinds of modules
 
 A module may be:
 
+-  A *declared module*, if it is defined by the ``module`` or ``ql`` grammar rules.
+-  A *non-declared module*, if it is not a *declared module*.
+
+A *declared module* may be:
+
 -  A *file module*, if it is defined implicitly by a QL file or a QLL file.
 -  A *query module*, if it is defined implicitly by a QL file.
 -  A *library module*, if it is not a query module.
 
+A *non-declared module* may be:
+
+-  A *built-in module*.
+-  An *instantiated module* (see :ref:`Parameterized modules`).
+-  An *instantiation-nested module*  (see :ref:`Parameterized modules`).
+
 A query module must contain one or more queries.
 
 Import directives
 ~~~~~~~~~~~~~~~~~
 
-An import directive refers to a module identifier:
+An import directive refers to a module expression:
 
 ::
 
    import ::= annotations "import" importModuleExpr ("as" modulename)?
 
-   qualId ::= simpleId | qualId "." simpleId
+   importModuleExpr ::= importModuleId arguments?
 
-   importModuleExpr ::= qualId | importModuleExpr "::" modulename arguments?
+   importModuleId ::= qualId | importModuleExpr "::" modulename
+
+   qualId ::= simpleId | qualId "." simpleId
 
    arguments ::= "<" argument ("," argument)* ">"
 
@@ -249,6 +262,73 @@ For qualified identifiers (``a.b``):
 
 A qualified module identifier is only valid within an import.
 
+Module expressions contain a module identifier and optional arguments. If arguments are present, the module expression instantiates the module that the identifier resolves to (see :ref:`Parameterized modules`).
+
+Module expressions cannot refer to :ref:`Parameterized modules`. Instead, parameterized modules must always be fully instantiated when they are referenced.
+
+.. _Parameterized modules:
+
+Parameterized modules
+~~~~~~~~~~~~~~~~~~~~~
+
+Modules with parameters are called *parameterized modules*. A *declared module* has parameters if and only if it is a *library module* and its declaration uses the ``parameters`` syntax.
+
+*Parameterized modules* can be instantiated with arguments that match the signatures of the parameters:
+
+- Given a type signature, the corresponding argument must be a type that transitively extends the specified ``extends`` types and is a transitive subtype of the specified ``instanceof`` types.
+- Given a predicate signature, the corresponding argument must be a predicate with exactly matching relational types.
+- Given a module signature, the corresponding argument must be a module that exports all the specified type and predicate members. Furthermore, the module must be declared as matching the module signature via the ``implements`` syntax.
+
+The result of instantiating a *parameterized module* is an *instantiated module*. The parameterized module is called the *underlying module* of the *instantiated module*.
+
+Instantiation-relative and instantiation-nested entities
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Given an *instantiated module*, every entity has a corresponding entity called the *instantiation-relative* entity, which is determined as follows:
+
+- If the entity is the *underlying module*, its *instantiation-relative* entity is the *instantiated module*.
+- If the entity is a parameter of the *underlying module*, its *instantiation-relative* entity is the corresponding argument.
+- If the entity is declared inside the *underlying module* or its nested modules, its *instantiation-relative* entity is an *instantiation-nested* entity that is generated by the module instantiation. Parameters of any modules that are nested inside the *underlying module* are considered declared inside the module for this purpose.
+- Otherwise, the entity's *instantiation-relative* entity is the initial entity itself.
+
+When the *instantiation-relative* entity of an entity is an *instantiation-nested* entity, then the initial entity is called the *underlying nested* entity of the *instantiation-nested* entity*, the *instantiated module* is called the *instantiation root* of the *instantiation-nested* entity, and the *underlying module* is called the *underlying root* of the *instantiation-nested* entity.
+
+The components of an *instantiation-nested* entity are the *instantiation-relative* entities of the components of its *underlying nested* entity. Among other things, this applies to:
+
+- values in the exported environments of *instantiation-nested* modules,
+- relational types of *instantiation-nested* predicates and predicate signatures,
+- required signatures of *instantiation-nested* parameters,
+- parameters of an *instantiation-nested* *parameterized module*,
+- fields and member predicates of *instantiation-nested* dataclasses.
+
+Given an *instantiated module*, any alias in the program has a corresponding alias called the *instantiation-relative* alias, which targets the *instantiation-relative* entity.
+
+Applicative instantiation
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Every entity has an *underlying completely uninstantiated* entity that is determined as follows:
+
+- If the entity is an *instantiated module*, its *underlying completely uninstantiated* entity is the *underlying completely uninstantiated* entity of the *underlying module*.
+- If the entity is an *instantiation-nested* entity, its *underlying completely uninstantiated* entity is the *underlying completely uninstantiated* entity of the *underlying nested* entity.
+- Otherwise, its *underlying completely uninstantiated* entity is the entity itself.
+
+An entity is called *completely uninstantiated* entity if it is its own *underlying completely uninstantiated* entity.
+
+Every *completely uninstantiated* entity has a *relevant set of parameters*, which is the set of all parameters of all the modules that the entity is transitively nested inside. For entities that are not nested inside any modules, the *relevant set of parameters* is empty.
+
+Note that the *relevant set of parameters* by construction contains only *completely uninstantiated* parameters.
+
+For a *completely uninstantiated* parameter, the *bottom-up instantiation-resolution* relative to an entity is defined as:
+
+- If the entity is an *instantiated module* or an *instantiation-nested* entity, the *bottom-up instantiation-resolution* is the *instantiation-relative* entity of the *bottom-up instantiation-resolution* relative to the *underlying module*.
+- Otherwise, the *bottom-up instantiation-resolution* is the parameter itself.
+
+An entity is called *fully instantiated* if none of the *bottom-up instantiation-resolutions* of the parameters in the *relevant set of parameters* of the entity's *underlying completely uninstantiated* entity are parameters.
+
+Two *instantiated modules* or two *instantiation-nested* entities are considered *equivalent* if they have the same *underlying completely uninstantiated* entity and each parameter in its *relevant set of parameters* has the same *bottom-up instantiation-resolution* relative to either *instantiated module*.
+
+Module instantiation is applicative, meaning that *equivalent* *instantiated modules* and *equivalent* *instantiation-nested* entities are indistinguishable.
+
 Module references and active modules
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -268,7 +348,7 @@ QL is a typed language. This section specifies the kinds of types available, the
 Kinds of types
 ~~~~~~~~~~~~~~
 
-Types in QL are either *primitive* types, *database* types, *class* types, *character* types or *class domain* types.
+Types in QL are either *primitive* types, *database* types, *class* types, *character* types, *class domain* types, type *parameters*, or *instantiation-nested* types.
 
 The primitive types are ``boolean``, ``date``, ``float``, ``int``, and ``string``.
 
@@ -289,7 +369,9 @@ With the exception of class domain types and character types (which cannot be re
 
    type ::= (moduleExpr "::")? classname | dbasetype | "boolean" | "date" | "float" | "int" | "string"
 
-   moduleExpr ::= modulename arguments? | moduleExpr "::" modulename arguments?
+   moduleExpr ::= moduleId arguments?
+
+   moduleId ::= modulename | moduleExpr "::" modulename
 
 A type reference is resolved to a type as follows:
 
@@ -1960,7 +2042,7 @@ Stratification
 
 A QL program can be *stratified* to a sequence of *layers*. A layer is a set of predicates and types.
 
-A valid stratification must include each predicate and type in the QL program. It must not include any other predicates or types.
+A valid stratification must include each predicate and type in the QL program that is *fully instantiated*. It must not include any other predicates or types.
 
 A valid stratification must not include the same predicate in multiple layers.