diff --git a/src/libraries/monads/list.ml b/src/libraries/monads/list.ml
new file mode 100644
index 0000000000000000000000000000000000000000..252a97bdaec00ddb1dc78cb1a5a3ec81eb019d4e
--- /dev/null
+++ b/src/libraries/monads/list.ml
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include Stdlib.List
+
+module Minimal = struct
+ type 'a t = 'a list
+ let return x = [ x ]
+ let map f xs = map f xs
+ let flatten xs = flatten xs
+ let product ls rs = combine ls rs
+end
+
+include Monad.Extend_Categoric_with_product (Minimal)
diff --git a/src/libraries/monads/list.mli b/src/libraries/monads/list.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b15e0d6144a8618e4e44bb5f647ba182633afcf2
--- /dev/null
+++ b/src/libraries/monads/list.mli
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+include module type of Stdlib.List
+include Monad.S_with_product with type 'a t = 'a list
diff --git a/src/libraries/monads/state_monad.ml b/src/libraries/monads/state_monad.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5747f0e8653d54d02e8aad4e8819ea70fe09a41a
--- /dev/null
+++ b/src/libraries/monads/state_monad.ml
@@ -0,0 +1,51 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(*************************************************************************)
+
+module Make (Env : Datatype.S_with_collections) = struct
+
+ module Cache = Env.Hashtbl
+ type 'a cache = 'a Cache.t
+ type env = Env.t
+
+ module Minimal = struct
+
+ type 'a t = ('a * env) cache option * (env -> 'a * env)
+ let return (x : 'a) : 'a t = (None, fun env -> x, env)
+
+ let compute ((cache, make) : 'a t) (env : env) : 'a * env =
+ match cache with
+ | None -> make env
+ | Some cache when Cache.mem cache env -> Cache.find cache env
+ | Some cache -> let r = make env in Cache.add cache env r ; r
+
+ let bind (f : 'a -> 'b t) (m : 'a t) : 'b t =
+ let make env = let a, env = compute m env in compute (f a) env in
+ (Some (Cache.create 13), make)
+
+ end
+
+ include Monad.Extend_Kleisli (Minimal)
+ let get_environment : env t = None, fun env -> env, env
+ let set_environment (env : env) : unit t = None, fun _ -> (), env
+ let resolve (m : 'a t) (env : env) : 'a * env = Minimal.compute m env
+
+end
diff --git a/src/libraries/monads/state_monad.mli b/src/libraries/monads/state_monad.mli
new file mode 100644
index 0000000000000000000000000000000000000000..02b28d4b431a7bb9939fa409d08972d5c5268f4e
--- /dev/null
+++ b/src/libraries/monads/state_monad.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2024 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Make (Env : Datatype.S_with_collections) : sig
+ include Monad.S
+ type env = Env.t
+ val get_environment : env t
+ val set_environment : env -> unit t
+ val resolve : 'a t -> env -> 'a * env
+end