diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index a4bccb1803dfd29de9060d2b9d405777c316653c..0229fbb0fb6518ad1cfe1f6201767505bbff86a5 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -1681,10 +1681,10 @@ logic_def:
     { LDaxiomatic($2,$4) }
 | MODULE push_module_identifier LBRACE logic_decls RBRACE
     { pop_module_types () ; LDmodule($2,$4) }
-| IMPORT mId = LONGIDENT SEMICOLON
-    { LDimport(mId,None) }
-| IMPORT mId = LONGIDENT AS asId = identifier SEMICOLON
-    { LDimport(mId,Some asId) }
+| IMPORT drv = module_driver mId = LONGIDENT SEMICOLON
+    { LDimport(drv,mId,None) }
+| IMPORT drv = module_driver mId = LONGIDENT AS asId = identifier SEMICOLON
+    { LDimport(drv,mId,Some asId) }
 | TYPE poly_id_type_add_typename EQUAL typedef SEMICOLON
         { let (id,tvars) = $2 in
           exit_type_variables_scope ();
@@ -1692,6 +1692,11 @@ logic_def:
         }
 ;
 
+module_driver:
+| identifier_or_typename_full COMMA { Some $1 }
+| { None }
+;
+
 push_module_identifier:
 | LONGIDENT { Stack.push $1 module_stack ; $1 }
 ;
diff --git a/src/kernel_services/ast_printing/logic_print.ml b/src/kernel_services/ast_printing/logic_print.ml
index 7e70ab64e6dc845feda50c42c0fc1b3b88b91f35..0da54ea252c1a05f32c8a96fc8b30e20013bb850 100644
--- a/src/kernel_services/ast_printing/logic_print.ml
+++ b/src/kernel_services/ast_printing/logic_print.ml
@@ -401,10 +401,12 @@ let rec print_decl fmt d =
         ignore @@ Stack.pop module_prefix ;
         raise err
     end
-  | LDimport (s,None) ->
-    fprintf fmt "@[<2>import@ %s;@]@\n}" s
-  | LDimport (s,Some a) ->
-    fprintf fmt "@[<2>import@ %s \\as %s;@]@\n}" s a
+  | LDimport (drv,mId,asId) ->
+    fprintf fmt "@[<2>import" ;
+    Option.iter (fprintf fmt "@ %s:") drv ;
+    fprintf fmt "@ %s" mId ;
+    Option.iter (fprintf fmt "@ \\as %s") asId ;
+    fprintf fmt ";@]@\n}"
   | LDinvariant (s,e) ->
     fprintf fmt "@[<2>invariant@ %s:@ %a;@]" s print_lexpr e
   | LDtype_annot ty -> print_type_annot fmt ty
diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 5b75815f9c2bc165e44e407e5c74764a7b86222e..0bbfb97d37301875456f98048c0fffb22a407893 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -73,6 +73,7 @@ type extension_common = {
   plugin: string;
   is_same_ext: extension_same;
 }
+type module_loader = typing_context -> location -> string list -> unit
 
 let default_printer printer fmt = function
   | Ext_id i -> Format.fprintf fmt "%d" i
@@ -132,6 +133,9 @@ module Extensions = struct
   (*hash table for status, preprocessor and typer of block extensions*)
   let ext_block_tbl = Hashtbl.create 5
 
+  (*hash table for module loader*)
+  let ext_module_loader = Hashtbl.create 5
+
   let find_single name :extension_single =
     try Hashtbl.find ext_single_tbl name with Not_found ->
       Kernel.fatal ~current:true "unsupported clause of name '%s'" name
@@ -144,6 +148,10 @@ module Extensions = struct
     try Hashtbl.find ext_block_tbl name with Not_found ->
       Kernel.fatal ~current:true "unsupported clause of name '%s'" name
 
+  let find_loader name :module_loader =
+    try Hashtbl.find ext_module_loader name with Not_found ->
+      Kernel.fatal ~current:true "unsupported module loader '%s'" name
+
   (* [Logic_lexer] can ask for something that is not a category, which is not
      a fatal error. *)
   let category name = (Hashtbl.find ext_tbl name).category
@@ -184,6 +192,14 @@ module Extensions = struct
         Hashtbl.add ext_tbl name info2
       end
 
+  let register_loader name loader =
+    if Hashtbl.mem ext_module_loader name then
+      Kernel.warning ~wkey:Kernel.wkey_acsl_extension
+        "Trying to register module loader %s twice. Ignoring second loader"
+        name
+    else
+      Hashtbl.add ext_module_loader name loader
+
   let preprocess name = (find_single name).preprocessor
 
   let preprocess_block name = (find_block name).preprocessor
@@ -264,6 +280,8 @@ let register_code_annot_next_loop =
   Extensions.register (Ext_code_annot Ext_next_loop)
 let register_code_annot_next_both =
   Extensions.register (Ext_code_annot Ext_next_both)
+let register_module_loader =
+  Extensions.register_loader
 
 (* Setup global references *)
 
@@ -278,7 +296,8 @@ let () =
   Logic_typing.set_extension_handler
     ~is_extension: Extensions.is_extension
     ~typer: Extensions.typing
-    ~typer_block: Extensions.typing_block ;
+    ~typer_block: Extensions.typing_block
+    ~loader: Extensions.find_loader;
   Cil.set_extension_handler
     ~visit: Extensions.visit ;
   Cil_printer.set_extension_handler
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index 05fc80c89312da72e64f2edaedacae7a9aefd5c9..db0021845def0c7b50161d9c0773c2a127ecfff8 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -153,3 +153,6 @@ val register_code_annot_next_loop: register_extension
 
 (** Registers extension both for code and loop annotations. *)
 val register_code_annot_next_both: register_extension
+
+type module_loader = typing_context -> location -> string list -> unit
+val register_module_loader : string -> module_loader -> unit
diff --git a/src/kernel_services/ast_queries/logic_typing.ml b/src/kernel_services/ast_queries/logic_typing.ml
index 466937fa3acab0ad8810efabdec2c7b32f567f4a..8f13fd8082004d2106ecf633c1992393a7634d88 100644
--- a/src/kernel_services/ast_queries/logic_typing.ml
+++ b/src/kernel_services/ast_queries/logic_typing.ml
@@ -524,6 +524,9 @@ type typing_context = {
     accept_formal:bool ->
     Lenv.t ->
     Logic_ptree.assigns -> Cil_types.assigns;
+  add_logic_type: location -> logic_type_info -> unit;
+  add_logic_ctor: location -> logic_ctor_info -> unit;
+  add_logic_function: location -> logic_info -> unit;
   error: 'a 'b. location -> ('a,Format.formatter,unit,'b) format4 -> 'a;
   on_error: 'a 'b. ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
 }
@@ -533,12 +536,14 @@ module Extensions = struct
   let ref_is_extension = ref (fun _ -> assert false)
   let ref_typer = ref (fun _ _ _ _ -> assert false)
   let ref_typer_block = ref (fun _ _ _ _ -> assert false)
+  let ref_loader = ref (fun _ _ _ _ -> assert false)
 
-  let set_handler ~is_extension ~typer ~typer_block =
+  let set_handler ~is_extension ~typer ~typer_block ~loader =
     assert (not !initialized) ;
     ref_is_extension := is_extension ;
     ref_typer := typer ;
     ref_typer_block := typer_block;
+    ref_loader := loader ;
     initialized := true
 
   let is_extension name = !ref_is_extension name
@@ -546,13 +551,17 @@ module Extensions = struct
   let typer name ~typing_context:typing_context ~loc =
     !ref_typer name typing_context loc
 
-  let typer_block name ~typing_context:typing_context ~loc =
-    !ref_typer_block name typing_context loc
+  let typer_block name ~typing_context:typing_context ~loc mId =
+    !ref_typer_block name typing_context loc mId
+
+  let loader name ~typing_context:typing_context ~loc =
+    !ref_loader name typing_context loc
 
 end
 let set_extension_handler = Extensions.set_handler
 let get_typer = Extensions.typer
 let get_typer_block = Extensions.typer_block
+let get_loader = Extensions.loader
 
 let rec arithmetic_conversion ty1 ty2 =
   match unroll_type ty1, unroll_type ty2 with
@@ -754,29 +763,6 @@ struct
           | [] -> None | ls -> Some (Lfun ls)
         end f
 
-  let make_typing_context ~pre_state ~post_state ~assigns_env
-      ~logic_type ~type_predicate ~type_term ~type_assigns = {
-    silent = false;
-    is_loop = C.is_loop;
-    pre_state=pre_state;
-    post_state=post_state;
-    assigns_env=assigns_env;
-    logic_type= logic_type;
-    type_predicate= type_predicate;
-    type_term= type_term;
-    type_assigns = type_assigns;
-    anonCompFieldName = C.anonCompFieldName;
-    conditionalConversion = C.conditionalConversion;
-    find_macro = C.find_macro;
-    find_var = C.find_var;
-    find_enum_tag = C.find_enum_tag;
-    find_comp_field = C.find_comp_field;
-    find_type = C.find_type ;
-    find_label = C.find_label;
-    error = C.error;
-    on_error = C.on_error;
-  }
-
   let rollback = Queue.create ()
 
   let start_transaction () = Queue.clear rollback
@@ -805,6 +791,14 @@ struct
       add_rollback_action (Logic_env.remove_logic_info_gen eq) li
     end
 
+  let add_logic_ctor loc ct =
+    try
+      ignore (Logic_env.find_logic_ctor ct.ctor_name);
+      C.error loc "logic type constructor %s is already defined" ct.ctor_name
+    with Not_found ->
+      Logic_env.add_logic_ctor ct.ctor_name ct;
+      add_rollback_action Logic_env.remove_logic_ctor ct.ctor_name
+
   let add_logic_type loc info =
     try
       ignore (Logic_env.find_logic_type info.lt_name);
@@ -813,6 +807,32 @@ struct
       Logic_env.add_logic_type info.lt_name info;
       add_rollback_action Logic_env.remove_logic_type info.lt_name
 
+  let make_typing_context ~pre_state ~post_state ~assigns_env
+      ~logic_type ~type_predicate ~type_term ~type_assigns = {
+    silent = false;
+    is_loop = C.is_loop;
+    pre_state=pre_state;
+    post_state=post_state;
+    assigns_env=assigns_env;
+    logic_type= logic_type;
+    type_predicate= type_predicate;
+    type_term= type_term;
+    type_assigns = type_assigns;
+    anonCompFieldName = C.anonCompFieldName;
+    conditionalConversion = C.conditionalConversion;
+    find_macro = C.find_macro;
+    find_var = C.find_var;
+    find_enum_tag = C.find_enum_tag;
+    find_comp_field = C.find_comp_field;
+    find_type = C.find_type ;
+    find_label = C.find_label;
+    add_logic_function ;
+    add_logic_type ;
+    add_logic_ctor ;
+    error = C.error;
+    on_error = C.on_error;
+  }
+
   let check_non_void_ptr loc ty =
     if Logic_utils.isLogicVoidPointerType ty then
       C.error loc "Cannot use a pointer to void here"
@@ -4268,7 +4288,14 @@ struct
       ignore (Logic_env.Modules.memo ~change (fun _ -> loc) name);
       Some (Dmodule(name,l,[],loc))
 
-    | LDimport(name,alias) ->
+    | LDimport(drv,name,alias) ->
+      Option.iter
+        begin fun drv ->
+          let typing_context = base_ctxt (Lenv.empty ()) in
+          Extensions.loader drv ~typing_context ~loc
+          @@ List.filter (fun s -> s <> "")
+          @@ String.split_on_char ':' name
+        end drv ;
       open_scope ~name ?alias () ; None
 
     | LDtype(name,l,def) ->
diff --git a/src/kernel_services/ast_queries/logic_typing.mli b/src/kernel_services/ast_queries/logic_typing.mli
index efa53b3e7e9adb05126979816b70a520c786ee9e..e2a347f574d5f800b53b3546c4f4e89c364d646c 100644
--- a/src/kernel_services/ast_queries/logic_typing.mli
+++ b/src/kernel_services/ast_queries/logic_typing.mli
@@ -77,7 +77,6 @@ module Lenv : sig
   val find_type_var: string -> t -> Cil_types.logic_type
   val find_logic_info: string -> t -> Cil_types.logic_info
   val find_logic_label: string -> t -> Cil_types.logic_label
-
 end
 
 type type_namespace = Typedef | Struct | Union | Enum
@@ -128,6 +127,9 @@ type typing_context = {
     typing_context ->
     accept_formal:bool ->
     Lenv.t -> Logic_ptree.assigns -> assigns;
+  add_logic_type: location -> logic_type_info -> unit;
+  add_logic_ctor: location -> logic_ctor_info -> unit;
+  add_logic_function: location -> logic_info -> unit;
   error: 'a 'b. location -> ('a,Format.formatter,unit,'b) format4 -> 'a;
 
   on_error: 'a 'b. ('a -> 'b) -> ((location * string) -> unit) -> 'a -> 'b
@@ -295,10 +297,10 @@ val set_extension_handler:
   is_extension:(string -> bool) ->
   typer:(string -> typing_context -> location -> Logic_ptree.lexpr list ->
          (bool * acsl_extension_kind)) ->
-  typer_block:(string -> typing_context ->
-               Filepath.position * Filepath.position ->
+  typer_block:(string -> typing_context -> location ->
                string * Logic_ptree.extended_decl list ->
                bool * Cil_types.acsl_extension_kind) ->
+  loader:(string -> typing_context -> location -> string list -> unit) ->
   unit
 (** Used to setup references related to the handling of ACSL extensions.
     If your name is not [Acsl_extension], do not call this
@@ -308,7 +310,7 @@ val set_extension_handler:
 val get_typer :
   string ->
   typing_context:typing_context ->
-  loc:Filepath.position * Filepath.position ->
+  loc:location ->
   Logic_ptree.lexpr list -> bool * Cil_types.acsl_extension_kind
 
 val get_typer_block:
@@ -317,3 +319,9 @@ val get_typer_block:
   loc:Logic_ptree.location ->
   string * Logic_ptree.extended_decl list ->
   bool * Cil_types.acsl_extension_kind
+
+val get_loader:
+  string ->
+  typing_context:typing_context ->
+  loc:Logic_ptree.location ->
+  string list -> unit
diff --git a/src/kernel_services/parsetree/logic_ptree.ml b/src/kernel_services/parsetree/logic_ptree.ml
index d982b1aa692fac36614998057d3eaac7dfdc4e94..a7a300f5c487ad73a27bff923e679e3dc9298cbb 100644
--- a/src/kernel_services/parsetree/logic_ptree.ml
+++ b/src/kernel_services/parsetree/logic_ptree.ml
@@ -247,9 +247,10 @@ and decl_node =
   | LDmodule of string * decl list
   (** [LDaxiomatic(id,decls)]
       represents a module of axiomatic definitions.*)
-  | LDimport of string * string option
-  (** [LDimport(id,alias)]
-      imports symbols from module, with optional alias.*)
+  | LDimport of string option * string * string option
+  (** [LDimport(driver,module,alias)]
+      imports symbols from module using the specified driver,
+      with optional alias.*)
   | LDinvariant of string * lexpr (** global invariant. *)
   | LDtype_annot of type_annot    (** type invariant. *)
   | LDmodel_annot of model_annot    (** model field. *)