diff --git a/src/ide/.merlin b/src/ide/.merlin
new file mode 100644
index 0000000000000000000000000000000000000000..6006efed3b5cce345d5880ff7baf2112fcf3cdee
--- /dev/null
+++ b/src/ide/.merlin
@@ -0,0 +1,5 @@
+PKG js_of_ocaml js_of_ocaml.ppx
+EXT lwt
+EXT js
+PKG why3
+B ../../lib/why3
diff --git a/src/session/itp_communication.ml b/src/session/itp_communication.ml
new file mode 100644
index 0000000000000000000000000000000000000000..d4ff0024f80220757a600f861cafd68f8b246408
--- /dev/null
+++ b/src/session/itp_communication.ml
@@ -0,0 +1,88 @@
+(* Information that the IDE may want to have *)
+type prover = string
+type transformation = string
+type strategy = string
+
+
+type node_ID = int
+let root_node : node_ID = 0
+
+
+type global_information =
+    {
+     provers         : prover list;
+     transformations : transformation list;
+     strategies      : strategy list;
+     commands        : string list;
+     (* hidden_provers       : string list; *)
+     (* session_time_limit   : int; *)
+     (* session_mem_limit    : int; *)
+     (* session_nb_processes : int; *)
+     (* session_cntexample   : bool; *)
+     (* main_dir             : string *)
+    }
+
+type message_notification =
+  | Proof_error           of node_ID * string
+  | Transf_error          of node_ID * string
+  | Strat_error           of node_ID * string
+  | Replay_Info           of string
+  | Query_Info            of node_ID * string
+  | Query_Error           of node_ID * string
+  | Help                  of string
+  | Information           of string
+  | Task_Monitor          of int * int * int
+  | Error                 of string
+  | Open_File_Error       of string
+
+type node_type =
+  | NRoot
+  | NFile
+  | NTheory
+  | NTransformation
+  | NGoal
+  | NProofAttempt
+
+type update_info =
+  | Proved of bool
+  | Proof_status_change of
+      Controller_itp.proof_attempt_status
+      * bool   (* obsolete or not *)
+      * Call_provers.resource_limit
+
+type notification =
+  | New_node     of node_ID * node_ID * node_type * string * bool
+  (* Notification of creation of new_node:
+     New_node (new_node, parent_node, node_type, name, detached). *)
+  | Node_change  of node_ID * update_info
+  (* inform that the data of the given node changed *)
+  | Remove       of node_ID
+  (* the given node was removed *)
+  | Initialized  of global_information
+  (* initial global data *)
+  | Saved
+  (* the session was saved on disk *)
+  | Message      of message_notification
+  (* an informative message, can be an error message *)
+  | Dead         of string
+  (* server exited *)
+  | Task         of node_ID * string
+  (* the node_ID's task *)
+
+type ide_request =
+  | Command_req       of node_ID * string
+  | Prove_req         of node_ID * prover * Call_provers.resource_limit
+  | Transform_req     of node_ID * transformation * string list
+  | Strategy_req      of node_ID * strategy
+  | Open_session_req  of string
+  | Add_file_req      of string
+  | Set_max_tasks_req of int
+  | Get_task          of node_ID
+  | Remove_subtree    of node_ID
+  | Copy_paste        of node_ID * node_ID
+  | Copy_detached     of node_ID
+  | Get_Session_Tree_req
+  | Save_req
+  | Reload_req
+  | Replay_req
+  | Exit_req
diff --git a/src/session/itp_communication.mli b/src/session/itp_communication.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b8c38491c67fb48a6589a4f26f69df07cb431ce0
--- /dev/null
+++ b/src/session/itp_communication.mli
@@ -0,0 +1,92 @@
+type prover = string
+type transformation = string
+type strategy = string
+
+type node_ID = int
+val root_node : node_ID
+
+(* --------------------------- types to be expanded if needed --------------------------------- *)
+
+(* Global information known when server process has started and that can be
+   shared with the IDE through communication *)
+type global_information =
+    {
+     provers         : prover list;
+     transformations : transformation list;
+     strategies      : strategy list;
+     commands        : string list
+     (* hidden_provers       : string list; *)
+     (* session_time_limit   : int; *)
+     (* session_mem_limit    : int; *)
+     (* session_nb_processes : int; *)
+     (* session_cntexample   : bool; *)
+     (* main_dir             : string *)
+    }
+
+type message_notification =
+  | Proof_error           of node_ID * string
+  | Transf_error          of node_ID * string
+  | Strat_error           of node_ID * string
+  | Replay_Info           of string
+  | Query_Info            of node_ID * string
+  | Query_Error           of node_ID * string
+  | Help                  of string
+  (* General information *)
+  | Information           of string
+  (* Number               of task scheduled, running, etc *)
+  | Task_Monitor          of int * int * int
+  (* An error happened that could not be identified in server *)
+  | Error                 of string
+  | Open_File_Error       of string
+
+type node_type =
+  | NRoot
+  | NFile
+  | NTheory
+  | NTransformation
+  | NGoal
+  | NProofAttempt
+
+type update_info =
+  | Proved of bool
+  | Proof_status_change of
+      Controller_itp.proof_attempt_status
+      * bool   (* obsolete or not *)
+      * Call_provers.resource_limit
+
+type notification =
+  | New_node     of node_ID * node_ID * node_type * string * bool
+  (* Notification of creation of new_node:
+     New_node (new_node, parent_node, node_type, name, detached). *)
+  | Node_change  of node_ID * update_info
+  (* inform that the data of the given node changed *)
+  | Remove       of node_ID
+  (* the given node was removed *)
+  | Initialized  of global_information
+  (* initial global data *)
+  | Saved
+  (* the session was saved on disk *)
+  | Message      of message_notification
+  (* an informative message, can be an error message *)
+  | Dead         of string
+  (* server exited *)
+  | Task         of node_ID * string
+  (* the node_ID's task *)
+
+type ide_request =
+  | Command_req       of node_ID * string
+  | Prove_req         of node_ID * prover * Call_provers.resource_limit
+  | Transform_req     of node_ID * transformation * string list
+  | Strategy_req      of node_ID * strategy
+  | Open_session_req  of string
+  | Add_file_req      of string
+  | Set_max_tasks_req of int
+  | Get_task          of node_ID
+  | Remove_subtree    of node_ID
+  | Copy_paste        of node_ID * node_ID
+  | Copy_detached     of node_ID
+  | Get_Session_Tree_req
+  | Save_req
+  | Reload_req
+  | Replay_req
+  | Exit_req