diff --git a/cours/cours-04/.ocamlinit b/cours/cours-04/.ocamlinit
new file mode 100644
index 0000000..4cd5be5
--- /dev/null
+++ b/cours/cours-04/.ocamlinit
@@ -0,0 +1,8 @@
+open Cours04;;
+
+#install_printer Lang0.pp;;
+#install_printer Lang1.pp;;
+#install_printer Lang2.pp;;
+#install_printer Lang2.pp_value;;
+
+module R = Rewrite.Make(Lang1);;
diff --git a/cours/cours-04/Id.ml b/cours/cours-04/Id.ml
new file mode 100644
index 0000000..0bf736f
--- /dev/null
+++ b/cours/cours-04/Id.ml
@@ -0,0 +1,46 @@
+module S = struct
+  type t = string
+
+  let compare (x : t) y = Stdlib.compare x y
+
+  let pp = Fmt.string
+end
+
+include S
+
+let fresh, reset =
+  let r = ref 0 in
+  (fun () -> incr r; Printf.sprintf "_x%d" !r),
+  (fun () -> r := 0)
+
+type 'a subst = (t * 'a) list
+
+let pp_subst pp_val =
+  let pp_kv ff (x, v) = Format.fprintf ff "%a\\%a" pp x pp_val v in
+  Fmt.(box (list ~sep:comma pp_kv))
+
+let empty = []
+
+let extend x v xs = (x, v) :: xs
+
+let assoc = List.assoc
+
+let singleton x v = [(x, v)]
+
+let trim xs =
+  List.fold_right
+    (fun (x, v) xs -> (x, v) :: List.remove_assoc x xs)
+    xs
+    []
+
+let domain xs = trim xs |> List.map fst
+
+type 'a rel = 'a -> 'a -> bool
+
+let included r xs ys =
+  try List.for_all (fun (x, v) -> r v (List.assoc x ys)) (trim xs)
+  with Not_found -> false
+
+let equal_subst eq xs ys = included eq xs ys && included eq ys xs
+
+module Set = Set.Make(S)
diff --git a/cours/cours-04/Id.mli b/cours/cours-04/Id.mli
new file mode 100644
index 0000000..86463ff
--- /dev/null
+++ b/cours/cours-04/Id.mli
@@ -0,0 +1,31 @@
+type t = string
+
+val compare : t -> t -> int
+
+val pp : t Fmt.t
+
+val fresh : unit -> t
+
+type 'a subst = (t * 'a) list
+
+val pp_subst : 'a Fmt.t -> 'a subst Fmt.t
+
+val empty : 'a subst
+
+val extend : t -> 'a -> 'a subst -> 'a subst
+
+val assoc : t -> 'a subst -> 'a
+
+val singleton : t -> 'a -> 'a subst
+
+val domain : 'a subst -> t list
+
+type 'a rel = 'a -> 'a -> bool
+
+val included : 'a rel -> 'a subst rel
+
+val equal_subst : 'a rel -> 'a subst rel
+
+val reset : unit -> unit
+
+module Set : Set.S with type elt = t
diff --git a/cours/cours-04/Lang0.ml b/cours/cours-04/Lang0.ml
new file mode 100644
index 0000000..5c0d515
--- /dev/null
+++ b/cours/cours-04/Lang0.ml
@@ -0,0 +1,162 @@
+type t =
+  | Var of Id.t
+  | Lit of int
+  | Add of t * t
+  | Let of t * bound1
+
+and bound1 = { bound : Id.t; body : t; }
+
+let rec pp ff = function
+  | Var x ->
+     Id.pp ff x
+  | Lit n ->
+     Format.fprintf ff "%d" n
+  | Add (e1, e2) ->
+     Format.fprintf ff "@[@[%a@]@ + @[%a@]@]"
+       pp e1
+       pp e2
+  | Let (e1, e2) ->
+     Format.fprintf ff "let(@[@[%a@],@ @[%a@]@])"
+       pp e1
+       pp_bound1 e2
+
+and pp_bound1 ff { bound; body; } =
+  Format.fprintf ff "@[%a.@,@[%a@]@]"
+    Id.pp bound
+    pp body
+
+let pp_substitution ff xs =
+  Fmt.list ~sep:Fmt.comma
+    (fun ff (x, e) ->
+      Format.fprintf ff "%a\\@[%a@]" Id.pp x pp e)
+    ff xs
+
+module Build = struct
+  let v x = Var x
+  let l i = Lit i
+  let ( + ) e1 e2 = Add (e1, e2)
+  let ( let* ) e1 mk_e2 =
+    let bound = Id.fresh () in
+    Let (e1, { bound; body = mk_e2 (Var bound); })
+end
+
+let rec subst s = function
+  | Var x ->
+     begin try Id.assoc x s with Not_found -> Var x end
+  | Lit k ->
+     Lit k
+  | Add (e1, e2) ->
+     Add (subst s e1, subst s e2)
+  | Let (e1, e2) ->
+     Let (subst s e1, subst_bound1 s e2)
+
+and subst_bound1 s { bound = x; body; } =
+  let x' = Id.fresh () in
+  { bound = x'; body = subst (Id.extend x (Var x') s) body; }
+
+let%expect_test "subst" =
+  Id.reset ();
+  let print_subst e x e' =
+    Format.printf "@[(@[%a@])[%a\\@[%a@]]@ = @[%a@]@]@."
+      pp e
+      Id.pp x
+      pp e'
+      pp (subst [(x, e')] e)
+  in
+  let open Build in
+  print_subst (l 1 + v "x") "x" (v "y");
+  [%expect {| (1 + x)[x\y] = 1 + y |}];
+  print_subst (Let (l 2, { bound = "y"; body = l 1 + v "x" + v "y"; }))
+    "x" (v "y");
+  [%expect {| (let(2, y.1 + x + y))[x\y] = let(2, _x1.1 + y + _x1) |}];
+  ();;
+
+let rec equal e e' =
+  match e, e' with
+  | Var x, Var x' ->
+     x = x'
+  | Lit i, Lit i' ->
+     i = i'
+  | Add (e1, e2), Add (e1', e2') ->
+     equal e1 e1' && equal e2 e2'
+  | Let (e1, e2), Let (e1', e2') ->
+     equal e1 e1' && equal_bound1 e2 e2'
+  | _ ->
+     false
+
+and equal_bound1 { bound = x; body = e; } { bound = x'; body = e'; } =
+  let y = Id.fresh () in
+  equal
+    (subst Id.(singleton x (Var y)) e)
+    (subst Id.(singleton x' (Var y)) e')
+
+and equal_subst sub1 sub2 = Id.equal_subst equal sub1 sub2
+
+let%expect_test "equal" =
+  Id.reset ();
+  let print_equal e1 e2 =
+    Format.printf "@[@[%a@]@ = @[%a@]: %b@]@."
+      pp e1
+      pp e2
+      (equal e1 e2)
+  in
+  let open Build in
+  print_equal (let* x = l 1 in x) (let* y = l 1 in y);
+  [%expect {| let(1, _x2._x2) = let(1, _x1._x1): true |}];
+  print_equal (let* x = l 1 in x) (let* y = l 2 in y);
+  [%expect {| let(1, _x5._x5) = let(2, _x4._x4): false |}];
+  print_equal
+    (let* x = l 1 in let* k = l 2 in x + k)
+    (let* y = l 1 in let* k = l 2 in y + k);
+  [%expect {|
+    let(1, _x8.let(2, _x9._x8 + _x9)) = let(1, _x6.let(2, _x7._x6 + _x7)): true |}];
+  print_equal
+    (let* x = l 1 in let* k = l 2 in x + k)
+    (let* y = l 1 in let* k = l 2 in k + y);
+  [%expect {|
+    let(1, _x16.let(2, _x17._x16 + _x17))
+    = let(1, _x14.let(2, _x15._x15 + _x14)): false |}];;
+
+let rec free_vars : t -> Id.Set.t = function
+  | Var x -> Id.Set.singleton x
+  | Lit _ -> Id.Set.empty
+  | Add (e1, e2) -> Id.Set.union (free_vars e1) (free_vars e2)
+  | Let (e1, e2) -> Id.Set.union (free_vars e1) (free_vars_bound1 e2)
+
+and free_vars_bound1 { bound; body; } =
+  Id.Set.remove bound (free_vars body)
+
+let%expect_test "free_vars" =
+  Id.reset ();
+  let print_free_vars e =
+    Format.printf "@[free_vars (@[%a@])@ = {@[%a@]}@]@."
+      pp e
+      Fmt.(list ~sep:comma Id.pp) (free_vars e |> Id.Set.to_seq |> List.of_seq)
+  in
+  let open Build in
+  print_free_vars (l 1 + l 2);
+  [%expect {| free_vars (1 + 2) = {} |}];
+  print_free_vars (let* x = l 12 in l 1 + x + v "y");
+  [%expect {| free_vars (let(12, _x1.1 + _x1 + y)) = {y} |}];
+  print_free_vars (let* x = l 12 in let* y = v "z" in l 1 + x + y);
+  [%expect {| free_vars (let(12, _x2.let(z, _x3.1 + _x2 + _x3))) = {z} |}];
+  ()
+
+let close_with { bound; body; } e = subst Id.(singleton bound e) body
+
+let rec eval : t -> int =
+  function
+  | Var _ -> failwith "open term"
+  | Lit k -> k
+  | Add (e1, e2) -> eval e1 + eval e2
+  | Let (e, b) -> eval (close_with b e)
+
+(* Tests fixtures *)
+
+let e1, e2, e3, e4 =
+  Id.reset ();
+  let open Build in
+  (l 1 + l 1),
+  (let* x = l 1 + l 1 in x),
+  (let* x = l 1 + l 1 in l 40 + x),
+  (let* x = l 1 + l 1 in let* y = x + l 1 in let* x = l 3 in x + y)
diff --git a/cours/cours-04/Lang1.ml b/cours/cours-04/Lang1.ml
new file mode 100644
index 0000000..6e4cfb9
--- /dev/null
+++ b/cours/cours-04/Lang1.ml
@@ -0,0 +1,180 @@
+type t =
+  | Var of Id.t
+  | Lit of int
+  | Add of t * t
+  | Let of t * bound1
+  | Hole of t Id.subst
+
+and bound1 = B of Id.t * t
+
+let rec pp ff = function
+  | Var x ->
+     Id.pp ff x
+  | Lit n ->
+     Format.fprintf ff "%d" n
+  | Add (e1, e2) ->
+     Format.fprintf ff "add(@[@[%a@],@ @[%a@]@])"
+       pp e1
+       pp e2
+  | Let (e1, e2) ->
+     Format.fprintf ff "let(@[@[%a@],@ @[%a@]@])"
+       pp e1
+       pp_bound1 e2
+  | Hole s ->
+     Format.fprintf ff "[]{@[%a@]}"
+       pp_substitution s
+
+and pp_bound1 ff (B (x, e))  =
+  Format.fprintf ff "@[%a.@,@[%a@]@]"
+    Id.pp x
+    pp e
+
+and pp_substitution ff xs =
+  Fmt.list ~sep:Fmt.comma
+    (fun ff (x, e) ->
+      Format.fprintf ff "%a\\@[%a@]" Id.pp x pp e)
+    ff xs
+
+module Builder = struct
+  let v x = Var x
+  let l i = Lit i
+  let ( + ) e1 e2 = Add (e1, e2)
+  let ( let* ) e1 mk_e2 = let x = Id.fresh () in Let (e1, B (x, mk_e2 (Var x)))
+  let h = Hole []
+end
+
+let rec subst s = function
+  | Var x ->
+     begin try Id.assoc x s with Not_found -> Var x end
+  | Lit k ->
+     Lit k
+  | Add (e1, e2) ->
+     Add (subst s e1, subst s e2)
+  | Let (e1, e2) ->
+     Let (subst s e1, subst_bound1 s e2)
+  | Hole s' ->
+     Hole (compose s' s)
+
+and subst_bound1 s (B (x, e)) =
+  let x' = Id.fresh () in
+  B (x', subst (Id.extend x (Var x') s) e)
+
+and compose s1 s2 =
+  match s1 with
+  | [] -> s2
+  | (x, t) :: s1 -> (x, subst s2 t) :: compose s1 s2
+
+let rec equal e e' =
+  match e, e' with
+  | Var x, Var x' ->
+     x = x'
+  | Lit i, Lit i' ->
+     i = i'
+  | Add (e1, e2), Add (e1', e2') ->
+     equal e1 e1' && equal e2 e2'
+  | Let (e1, e2), Let (e1', e2') ->
+     equal e1 e1' && equal_bound1 e2 e2'
+  | Hole sub1, Hole sub2 ->
+     equal_subst sub1 sub2
+  | _ ->
+     false
+
+and equal_bound1 (B (x, e)) (B (x', e')) =
+  let y = Id.fresh () in
+  equal
+    (subst Id.(singleton x (Var y)) e)
+    (subst Id.(singleton x' (Var y)) e')
+
+and equal_subst sub1 sub2 = Id.equal_subst equal sub1 sub2
+
+let%expect_test "e1" =
+  Id.reset ();
+  let print e1 e2 =
+    Format.printf "@[@[%a@]@ = @[%a@]: %b@]@."
+      pp e1
+      pp e2
+      (equal e1 e2)
+  in
+  let open Builder in
+  print (let* x = l 1 in x) (let* y = l 1 in y);
+  [%expect {| let(1, _x2._x2) = let(1, _x1._x1): true |}];
+  print (let* x = l 1 in x) (let* y = l 2 in y);
+  [%expect {| let(1, _x5._x5) = let(2, _x4._x4): false |}];
+  print
+    (let* x = l 1 in let* k = l 2 in x + k)
+    (let* y = l 1 in let* k = l 2 in y + k);
+  [%expect {|
+    let(1, _x8.let(2, _x9.add(_x8, _x9)))
+    = let(1, _x6.let(2, _x7.add(_x6, _x7))): true |}];
+  print
+    (let* x = l 1 in let* k = l 2 in x + k)
+    (let* y = l 1 in let* k = l 2 in k + y);
+  [%expect {|
+    let(1, _x16.let(2, _x17.add(_x16, _x17)))
+    = let(1, _x14.let(2, _x15.add(_x15, _x14))): false |}];;
+
+let close_with (B (x, e)) e' = subst Id.(singleton x e') e
+
+let rec plug k e =
+  match k with
+  | (Var _ | Lit _) as k -> k
+  | Add (k1, k2) -> Add (plug k1 e, plug k2 e)
+  | Let (k1, k2) -> Let (plug k1 e, plug_bound1 k2 e)
+  | Hole s -> subst s e
+
+and plug_bound1 (B (x, k)) e = B (x, plug k e)
+
+let beta0 : t -> t option
+  = function
+  | Add (Lit k1, Lit k2) ->
+     Some (Lit (k1 + k2))
+  | Let (e1, e2) ->
+     Some (close_with e2 e1)
+  | _ ->
+     None
+
+let wrap f (k, e) = (f k, e)
+
+let rec decompose t =
+  Seq.cons (Hole [], t) (decompose_subterms t)
+
+and decompose_subterms = function
+  | Var _ | Lit _ | Hole _ ->
+     Seq.empty
+  | Add (e1, e2) ->
+     Seq.interleave
+       (decompose e1 |> Seq.map (wrap (fun k -> Add (k, e2))))
+       (decompose e2 |> Seq.map (wrap (fun k -> Add (e1, k))))
+  | Let (e1, B (x, e2)) ->
+     Seq.interleave
+       (decompose e1 |> Seq.map (wrap (fun k -> Let (k, B (x, e2)))))
+       (decompose e2 |> Seq.map (wrap (fun k -> Let (e1, B (x, k)))))
+
+let rewrite e =
+  decompose e
+  |> Seq.filter_map (fun (k, e) -> beta0 e |> Option.map (fun e -> (k, e)))
+  |> Seq.map (fun (k, e) -> plug k e)
+
+(* Test fixtures *)
+
+let e1, e2, e3, e4 =
+  Id.reset ();
+  let open Builder in
+  (l 1 + l 1),
+  (let* x = l 1 + l 1 in x),
+  (let* x = l 1 + l 1 in l 40 + x),
+  (let* x = l 1 + l 1 in let* y = x + l 1 in let* x = l 3 in x + y)
+
+let%expect_test "rew0" =
+  Id.reset ();
+  let e = Builder.(let* x = l 1 + l 1 in l 28 + l 12 + x) in
+  Format.printf "%a@." pp e;
+  [%expect {| let(add(1, 1), _x1.add(add(28, 12), _x1)) |}];
+  Format.printf "@[@[%a@]@ -> @[<hv 2>%a@]@]@."
+    pp e
+    Fmt.(list ~sep:comma pp) (rewrite e |> List.of_seq);
+  [%expect {|
+    let(add(1, 1), _x1.add(add(28, 12), _x1))
+    -> add(add(28, 12), add(1, 1)),
+         let(2, _x1.add(add(28, 12), _x1)),
+         let(add(1, 1), _x1.add(40, _x1)) |}]
diff --git a/cours/cours-04/Lang2.ml b/cours/cours-04/Lang2.ml
new file mode 100644
index 0000000..031360a
--- /dev/null
+++ b/cours/cours-04/Lang2.ml
@@ -0,0 +1,194 @@
+(** {2 Abstract Syntax Trees} *)
+
+type t = Var of Id.t           (* occurrence "x", "y", etc. *)
+       | Int of int            (* constante litérale "42", etc. *)
+       | Add of t * t          (* somme "e1 + e2" *)
+       | Bool of bool          (* booléen litéral "true", "false" *)
+       | If of t * t * t       (* conditionnelle *)
+       | Let of t * bound1     (* déf. locale "let e1 be x in e2" *)
+       | Fun of bound1         (* fonction anonyme "fun x -> e" *)
+       | App of t * t          (* application "e1 e2" *)
+       | Ref of t              (* allocation "ref e" *)
+       | Read of t             (* déréférencement "!e" *)
+       | Asgn of t * t         (* assignation "e1 := e2" *)
+       | Unit                  (* 0-uplet *)
+       | Seq of t * t          (* séquence "e1; e2" *)
+
+and bound1 = { bound : Id.t; body : t; }
+
+(** {2 Evaluation} *)
+
+type env = (Id.t * value) list
+
+and value =
+  | VInt of int
+  | VBool of bool
+  | VFun of bound1 * env
+  | VRef of value ref
+  | VUnit
+
+let rec eval env = function
+  | Var x -> List.assoc x env
+  | Int n -> VInt n
+  | Add (e1, e2) -> add_values (eval env e1) (eval env e2)
+  | Bool b -> VBool b
+  | If (e1, e2, e3) -> if_value (eval env e1) env e2 e3
+  | Let (e, b) -> eval_bound1 env b (eval env e)
+  | Fun b -> VFun (b, env)
+  | App (e1, e2) -> app_values (eval env e1) (eval env e2)
+  | Ref e -> VRef (ref (eval env e))
+  | Read e -> read_value (eval env e)
+  | Asgn (e1, e2) -> asgn_values (eval env e1) (eval env e2)
+  | Unit -> VUnit
+  | Seq (e1, e2) -> seq_value (eval env e1) env e2
+
+and eval_bound1 env { bound; body; } v =
+  eval ((bound, v) :: env) body
+
+and add_values v1 v2 =
+  match v1, v2 with
+  | VInt n1, VInt n2 -> VInt (n1 + n2)
+  | _ -> failwith "ill-typed"
+
+and if_value v1 env e2 e3 =
+  match v1 with
+  | VBool true -> eval env e2
+  | VBool false -> eval env e3
+  | _ -> failwith "ill-typed"
+
+and app_values v1 v2 =
+  match v1 with
+  | VFun (b, env) -> eval_bound1 env b v2
+  | _ -> failwith "ill-typed"
+
+and read_value v =
+  match v with VRef r -> !r | _ -> failwith "ill-typed"
+
+and asgn_values v1 v2 =
+  match v1 with VRef r -> r := v2; VUnit | _ -> failwith "ill-typed"
+
+and seq_value v1 env e2 =
+  match v1 with VUnit -> eval env e2 | _ -> failwith "ill-typed"
+
+(** {2 Pretty-printing} *)
+
+let rec pp ff =
+  let pp_maybe_paren ?(space = true) prefix pp ff e =
+    match e with
+    | Var _ | Int _ | Bool _ | Unit ->
+       Format.fprintf ff "@[%s%a@[%a@]@]"
+         prefix
+         Fmt.(if space then sp else nop) ()
+         pp e
+     | _ ->
+        Format.fprintf ff "@[%s(@[%a@])@]"
+          prefix
+          pp e
+  in
+  function
+  | Var x ->
+     Id.pp ff x
+  | Int n ->
+     Format.fprintf ff "%d" n
+  | Add (e1, e2) ->
+     Format.fprintf ff "(@[@[%a@] +@ @[%a@]@])"
+       pp e1
+       pp e2
+  | Bool b ->
+     Format.fprintf ff "%b" b
+  | If (e1, e2, e3) ->
+     Format.fprintf ff "if(@[@[%a@],@ @[%a@],@ @[%a@]@])"
+       pp e1
+       pp e2
+       pp e3
+  | Let (e1, e2) ->
+     Format.fprintf ff "let(@[@[%a@],@ @[%a@]@])"
+       pp e1
+       pp_bound1 e2
+  | Fun b ->
+     Format.fprintf ff "fun(@[%a@])"
+       pp_bound1 b
+  | App (e1, e2) ->
+     Format.fprintf ff "(@[@[%a@]@ @[%a@]@])"
+       pp e1
+       pp e2
+  | Ref e ->
+     pp_maybe_paren "ref" pp ff e
+  | Read e ->
+     pp_maybe_paren ~space:false "!" pp ff e
+  | Asgn (e1, e2) ->
+     Format.fprintf ff "(@[@[%a@]@ := @[%a@]@])"
+       pp e1
+       pp e2
+  | Unit ->
+     Format.fprintf ff "()"
+  | Seq (e1, e2) ->
+     Format.fprintf ff "(@[@[%a@];@ @[%a@]@])"
+       pp e1
+       pp e2
+
+and pp_bound1 ff { bound; body; } =
+  Format.fprintf ff "@[%a.@,@[%a@]@]"
+    Id.pp bound
+    pp body
+
+let rec pp_value ff = function
+  | VInt n ->
+     Format.fprintf ff "%d" n
+  | VBool b ->
+     Format.fprintf ff "%b" b
+  | VRef _ ->
+     Format.fprintf ff "ref(..)"
+  | VUnit ->
+     Format.fprintf ff "()"
+  | VFun (b, env) ->
+     Format.fprintf ff "@[<v 2>fun(@[%a@])@,[@[%a@]]@]"
+       pp_bound1 b
+       pp_env env
+
+and pp_env ff env =
+  let pp_binding ff (x, v) =
+    Format.fprintf ff "@[<hv 2>%a@ = @[%a@]@]"
+      Id.pp x
+      pp_value v
+  in
+  Fmt.(list ~sep:comma pp_binding) ff env
+
+(** {2 AST Building Helpers} *)
+
+module Build = struct
+  let fresh_bound1 mk =
+    let x = Id.fresh () in { bound = x; body = mk (Var x); }
+
+  let v x = Var x
+  let i n = Int n
+  let ( + ) e1 e2 = Add (e1, e2)
+  let b b = Bool b
+  let if_ e1 e2 e3 = If (e1, e2, e3)
+  let ( let* ) e1 mk_e2 = Let (e1, fresh_bound1 mk_e2)
+  let fun_ mk_body = Fun (fresh_bound1 mk_body)
+  let app f args = List.fold_left (fun f arg -> App (f, arg)) f args
+  let ref_ e = Ref e
+  let ( ! ) e = Read e
+  let ( := ) e1 e2 = Asgn (e1, e2)
+  let s = function
+    | [] -> Unit
+    | e :: es -> List.fold_left (fun e1 e2 -> Seq (e1, e2)) e es
+end
+
+(** {2 Tests} *)
+
+let print_eval e =
+  let v = eval [] e in
+  Format.printf "@[<hv 2>@[%a@]@ => @[%a@]@]@."
+    pp e
+    pp_value v
+
+let%expect_test "test" =
+  Id.reset ();
+  let open Build in
+  print_eval (i 1 + i 2);
+  [%expect {| (1 + 2) => 3 |}];
+  print_eval (let* x = ref_ (i 1) in
+              s [x := i 2; !x] + !x);
+  [%expect {| let(ref 1, _x1.(((_x1 := 2); !_x1) + !_x1)) => 3 |}]
diff --git a/cours/cours-04/Rewrite.ml b/cours/cours-04/Rewrite.ml
new file mode 100644
index 0000000..11f3259
--- /dev/null
+++ b/cours/cours-04/Rewrite.ml
@@ -0,0 +1,57 @@
+module type LANG = sig
+  type t
+  val pp : t Fmt.t
+  val equal : t -> t -> bool
+  val rewrite : t -> t Seq.t
+end
+
+module Make(L : LANG) = struct
+  type graph = (L.t * L.t) Seq.t
+
+  let rec reductions t =
+    let open Seq in
+    let* t' = L.rewrite t in
+    cons (t, t') (reductions t')
+
+  let is_normal t =
+    L.rewrite t |> Seq.uncons |> Option.is_none
+
+  let normal_forms t =
+    let open Seq in
+    reductions t |> map snd |> filter is_normal |> Seq.dedup L.equal
+
+  let to_graphviz g =
+    let b = Buffer.create 100 in
+    let ff = Format.formatter_of_buffer b in
+
+    (* Disable line breaks. *)
+    let ff_funs = Format.pp_get_formatter_out_functions ff () in
+    Format.pp_set_formatter_out_functions
+      ff
+      { ff_funs with
+        out_newline = (fun _ -> ());
+        out_indent = (fun _ -> ());
+        out_spaces = (fun _ -> ());
+      };
+
+    Format.fprintf ff "strict digraph {\n";
+    Format.fprintf ff "  overlap=scale;\n";
+    Format.fprintf ff "  splines=true;\n";
+    Format.fprintf ff "  rankdir=\"LR\";\n";
+    Seq.iter (fun (t, t') ->
+        Format.fprintf ff "\"%a\" -> \"%a\";\n"
+          L.pp t
+          L.pp t') g;
+    Format.fprintf ff "}@.";
+    Buffer.contents b
+
+  let display ?(verbose = false) ?(max = 20) g =
+    let gv_fn, oc = Filename.open_temp_file "red" ".dot" in
+    let pdf_fn = Filename.temp_file "graph" ".pdf" in
+    output_string oc @@ to_graphviz @@ Seq.take max g;
+    close_out oc;
+    if verbose then Printf.eprintf "Graph in %s, PDF in %s\n" gv_fn pdf_fn;
+    flush stderr;
+    ignore @@ Unix.system Printf.(sprintf "dot -Tpdf %s > %s" gv_fn pdf_fn);
+    ignore @@ Unix.system Printf.(sprintf "xdg-open %s" pdf_fn)
+end
diff --git a/cours/cours-04/Rewrite.mli b/cours/cours-04/Rewrite.mli
new file mode 100644
index 0000000..3af2ed8
--- /dev/null
+++ b/cours/cours-04/Rewrite.mli
@@ -0,0 +1,14 @@
+module type LANG = sig
+  type t
+  val pp : t Fmt.t
+  val equal : t -> t -> bool
+  val rewrite : t -> t Seq.t
+end
+
+module Make(L : LANG) : sig
+  type graph = (L.t * L.t) Seq.t
+  val reductions : L.t -> graph
+  val is_normal : L.t -> bool
+  val normal_forms : L.t -> L.t Seq.t
+  val display : ?verbose:bool -> ?max:int -> graph -> unit
+end
diff --git a/cours/cours-04/Seq.ml b/cours/cours-04/Seq.ml
new file mode 100644
index 0000000..8ea4166
--- /dev/null
+++ b/cours/cours-04/Seq.ml
@@ -0,0 +1,46 @@
+include Stdlib.Seq
+
+let hd xs = uncons xs |> Option.map fst
+let tl xs = uncons xs |> Option.map snd
+
+let rec const x () = cons x (const x) ()
+
+let rec nth : type a. int -> a t -> a option =
+  fun n xs ->
+  if n = 0 then hd xs else tl xs |> Option.map (nth (n - 1)) |> Option.join
+
+let join : type a. a t t -> a t =
+  let rec aux todo n k xss =
+    let continue () = aux [] (n + 1) n (append List.(to_seq @@ rev todo) xss) in
+    if k < 0 then continue ()
+    else
+      begin match uncons xss, todo with
+      | None, [] ->
+         empty
+      | None, _ :: _ ->
+         continue ()
+      | Some (xs, xss), _ ->
+         begin match uncons xs with
+         | None -> aux todo n (k - 1) xss
+         | Some (x, xs) -> fun () -> cons x (aux (xs :: todo) n (k - 1) xss) ()
+         end
+      end
+  in
+  fun xss () -> aux [] 1 0 xss ()
+
+let ( let* ) xs f = map f xs |> concat
+
+let rec combine f xs ys =
+  match uncons xs, uncons ys with
+  | Some (x, xs), Some (y, ys) -> fun () -> cons (f x y) (combine f xs ys) ()
+  | None, _ | _, None -> empty
+
+let rec dedup eq xs =
+  match uncons xs with
+  | None -> xs
+  | Some (x, xs) -> cons x (filter (fun x' -> not (eq x x')) (dedup eq xs))
+
+let rec nat : int t = fun () -> cons 0 (map ((+) 1) nat) ()
+
+let nats : (int * int) t t =
+  combine (fun x ys -> map (fun y -> (x, y)) ys) nat (const nat)
diff --git a/cours/cours-04/dune b/cours/cours-04/dune
new file mode 100644
index 0000000..26cb81f
--- /dev/null
+++ b/cours/cours-04/dune
@@ -0,0 +1,5 @@
+(library
+  (name cours04)
+  (libraries fmt unix)
+  (inline_tests)
+  (preprocess (pps ppx_expect)))
diff --git a/cours/cours-04/dune-project b/cours/cours-04/dune-project
new file mode 100644
index 0000000..929c696
--- /dev/null
+++ b/cours/cours-04/dune-project
@@ -0,0 +1 @@
+(lang dune 2.0)
diff --git a/cours/cours-interpretation.pdf b/cours/cours-interpretation.pdf
new file mode 100644
index 0000000..aba3e62
Binary files /dev/null and b/cours/cours-interpretation.pdf differ
diff --git a/cours/journal.org b/cours/journal.org
index 483e80c..ae059da 100644
--- a/cours/journal.org
+++ b/cours/journal.org
@@ -51,3 +51,16 @@
 
    - En cours : questions/réponses au sujet du jalon 1 et introduction à
      l'interprétation des programmes Hopix.
+* Cours 04 <2023-10-11>
+  On discute de la gestion de la syntaxe et en particulier des lieurs, voir les
+  [[file:cours-semantique.pdf][transparents]].
+* Cours 05 <2023-10-18>
+  On revient sur la gestion de la liaison, et de l'évaluation, voir les
+  [[file:cours-semantique.pdf][transparents]].
+* Cours 06 <2023-10-25>
+  On termine les transparents précédents sur l'écriture d'évaluateurs.
+
+  Attention : le fichier contenant les diapos a été renommé, c'est désormais
+  [[file:cours-interpretation.pdf][transparents]].
+
+  On décrit le jalon 2.
diff --git a/jalons/jalon-2.pdf b/jalons/jalon-2.pdf
index c3cd417..a78fe0b 100644
Binary files a/jalons/jalon-2.pdf and b/jalons/jalon-2.pdf differ