diff --git a/CHANGELOG.md b/CHANGELOG.md
index fc289dd2dd9838e10798d814b4883f5aecfaa49b..688a091e46abcb87a5f88d75ed0f2738e3f9e71e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -43,14 +43,26 @@ API-breaking change is listed.
     strengthened to only require commutativity w.r.t. the operation being
     pulled out of the accumulator, not commutativity of
     the folded function itself.
-- Add string literal notation "my string" to `std_scope`, and no longer globally
-  open `string_scope`.
 - Add lemmas `Sorted_unique_strong` and `StronglySorted_unique_strong` that only
   require anti-symmetry for the elements that are in the list.
 - Rename `foldr_cons_permute` into `foldr_cons_permute_strong` and strengthen
   (a) from function `f : A → A → A` to `f : A → B → B`, and (b) to only require
   associativity/commutativity for the elements that are in the list.
 - Rename `foldr_cons_permute_eq` into `foldr_cons_permute`.
+- Various improvements to the support of strings:
+  + Add string literal notation "my string" to `std_scope`, and no longer
+    globally open `string_scope`.
+  + Move all definitions and lemmas about strings/ascii into the modules
+    `String`/`Ascii`, i.e., rename `string_rev_app` → `String.rev_app`,
+    `string_rev` → `String.rev`, `is_nat` → `Ascii.is_nat`,
+    `is_space` → `Ascii.is_space` and `words` → `String.words`.
+  + The file `std.strings` no longer exports the `String` module, it only
+    exports the `string` type, its constructors, induction principles, and
+    notations (in `string_scope`). Similar to the number types (`nat`, `N`,
+    `Z`), importing the `String` module yourself is discouraged, rather use
+    `String.function` and `String.lemma`.
+  + Add `String.le` and some theory about it (decidability, proof irrelevance,
+    total order).
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -109,6 +121,12 @@ s/\bmap_fold_ind2\b/map_fold_weak_ind/g
 # foldr_cons_permute
 s/\bfoldr_cons_permute\b/foldr_cons_permute_strong/g
 s/\bfoldr_cons_permute_eq\b/foldr_cons_permute/g
+# strings
+s/\bstring_rev_app\b/String.rev_app/g
+s/\bstring_rev\b/String.rev/g
+s/\bis_nat\b/Ascii.is_nat/g
+s/\bis_space\b/Ascii.is_space/g
+s/\bwords\b/String.words/g
 EOF
 ```
 
diff --git a/stdpp/pretty.v b/stdpp/pretty.v
index f5ea9a339c61a609c55a8806131ea2cebb2c46da..6efb0dd91c9a60fb2b2451fb849993e94da06e64 100644
--- a/stdpp/pretty.v
+++ b/stdpp/pretty.v
@@ -113,7 +113,7 @@ Proof. apply _. Qed.
 Global Instance pretty_Z : Pretty Z := λ x,
   match x with
   | Z0 => "0" | Zpos x => pretty x | Zneg x => "-" +:+ pretty x
-  end%string.
+  end.
 Global Instance pretty_Z_inj : Inj (=@{Z}) (=) pretty.
 Proof.
   unfold pretty, pretty_Z.
diff --git a/stdpp/strings.v b/stdpp/strings.v
index 7f63c3201143065118d26f5eda1d2438e579e49a..29064296c86f2748c8697f77a7796ce7e9bdd6c2 100644
--- a/stdpp/strings.v
+++ b/stdpp/strings.v
@@ -1,74 +1,27 @@
 From Coq Require Import Ascii.
-From Coq Require Export String.
+From Coq Require String.
 From stdpp Require Export list.
 From stdpp Require Import countable.
 From stdpp Require Import options.
 
-(** To avoid randomly ending up with [String.length] because this module is
-imported hereditarily somewhere. *)
-Notation length := List.length.
+(** We define the ascii/string methods in corresponding modules, similar to what
+is done for numbers. These modules should generally not be imported, e.g., use
+[Ascii.is_nat] instead. *)
 
-(** Enable the string literal and append notation in [stdpp_scope], making it
-possible to write string literals as "foo" instead of "foo"%string.
+(** To avoid poluting the global namespace, we export only the [string] data
+type (with its constructors and eliminators) and notations. *)
+Export String (string(..)).
+Export (notations) String.
+
+(** Enable the string literal and append notation in [stdpp_scope], making
+it possible to write string literals as "foo" instead of "foo"%string.
 One could also enable the string literal notation via [Open Scope string_scope]
-but that overrides various notations (e.g, [++] on [list], [=?] on [nat]) with
-the version for strings. *)
-String Notation string string_of_list_byte list_byte_of_string : stdpp_scope.
-Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
-Global Arguments String.append : simpl never.
-
-(** * Decision of equality *)
-Global Instance ascii_eq_dec : EqDecision ascii := ascii_dec.
-Global Instance string_eq_dec : EqDecision string.
-Proof. solve_decision. Defined.
-Global Instance string_app_inj s1 : Inj (=) (=) (String.append s1).
-Proof. intros ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
-
-Global Instance string_inhabited : Inhabited string := populate "".
-
-(* Reverse *)
-Fixpoint string_rev_app (s1 s2 : string) : string :=
-  match s1 with
-  | "" => s2
-  | String a s1 => string_rev_app s1 (String a s2)
-  end.
-Definition string_rev (s : string) : string := string_rev_app s "".
-
-Definition is_nat (x : ascii) : option nat :=
-  match x with
-  | "0" => Some 0
-  | "1" => Some 1
-  | "2" => Some 2
-  | "3" => Some 3
-  | "4" => Some 4
-  | "5" => Some 5
-  | "6" => Some 6
-  | "7" => Some 7
-  | "8" => Some 8
-  | "9" => Some 9
-  | _ => None
-  end%char.
-
-(* Break a string up into lists of words, delimited by white space *)
-Definition is_space (x : Ascii.ascii) : bool :=
-  match x with
-  | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
-  end%char.
-
-Fixpoint words_go (cur : option string) (s : string) : list string :=
-  match s with
-  | "" => option_list (string_rev <$> cur)
-  | String a s =>
-     if is_space a then option_list (string_rev <$> cur) ++ words_go None s
-     else words_go (Some (from_option (String a) (String a "") cur)) s
-  end.
-Definition words : string → list string := words_go None.
+but that overrides various notations (e.g, [=?] on [nat]) with the version for
+strings. *)
+String Notation string
+  String.string_of_list_byte String.list_byte_of_string : stdpp_scope.
 
-Ltac words s :=
-  match type of s with
-  | list string => s
-  | string => eval vm_compute in (words s)
-  end.
+Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
 
 (** * Encoding and decoding *)
 (** The [Countable] instance of [string] is particularly useful to allow strings
@@ -77,7 +30,11 @@ to be used as keys in [gmap].
 The encoding of [string] to [positive] is taken from
 https://github.com/xavierleroy/canonical-binary-tries/blob/v2/lib/String2pos.v.
 It avoids creating auxiliary data structures such as [list bool], thereby
-improving efficiency. *)
+improving efficiency.
+
+We first provide some [Local] helper functions and then define the [Countable]
+instances for encoding/decoding in the modules [Ascii] and [String]. End-users
+should always use these instances. *)
 Local Definition bool_cons_pos (b : bool) (p : positive) : positive :=
   if b then p~1 else p~0.
 Local Definition ascii_cons_pos (c : ascii) (p : positive) : positive :=
@@ -128,13 +85,122 @@ Defined.
 Local Lemma pos_to_string_string_to_pos s : pos_to_string (string_to_pos s) = s.
 Proof. induction s as [|[[][][][][][][][]]]; by f_equal/=. Qed.
 
-Global Program Instance string_countable : Countable string := {|
-  encode := string_to_pos; decode p := Some (pos_to_string p)
-|}.
-Solve Obligations with
-  naive_solver eauto using pos_to_string_string_to_pos with f_equal.
-
-Global Instance ascii_countable : Countable ascii :=
-  inj_countable (λ a, String a EmptyString)
-                (λ s, match s with String a _ => Some a | _ => None end)
-                (λ a, eq_refl).
+Module Ascii.
+  Global Instance eq_dec : EqDecision ascii := ascii_dec.
+
+  Global Program Instance countable : Countable ascii := {|
+    encode a := string_to_pos (String a EmptyString);
+    decode p := match pos_to_string p return _ with String a _ => Some a | _ => None end
+  |}.
+  Next Obligation. by intros [[] [] [] [] [] [] [] []]. Qed.
+
+  Definition is_nat (x : ascii) : option nat :=
+    match x with
+    | "0" => Some 0
+    | "1" => Some 1
+    | "2" => Some 2
+    | "3" => Some 3
+    | "4" => Some 4
+    | "5" => Some 5
+    | "6" => Some 6
+    | "7" => Some 7
+    | "8" => Some 8
+    | "9" => Some 9
+    | _ => None
+    end%char.
+
+  Definition is_space (x : ascii) : bool :=
+    match x with
+    | "009" | "010" | "011" | "012" | "013" | " " => true | _ => false
+    end%char.
+End Ascii.
+
+Module String.
+  (** Use a name that is consistent with [list]. *)
+  Notation app := String.append.
+
+  (** And obtain a proper behavior for [simpl]. *)
+  Global Arguments app : simpl never.
+
+  Global Instance eq_dec : EqDecision string.
+  Proof. solve_decision. Defined.
+
+  Global Instance inhabited : Inhabited string := populate "".
+
+  Global Program Instance countable : Countable string := {|
+    encode := string_to_pos;
+    decode p := Some (pos_to_string p)
+  |}.
+  Solve Obligations with
+    naive_solver eauto using pos_to_string_string_to_pos with f_equal.
+
+  Definition le (s1 s2 : string) : Prop := String.leb s1 s2.
+
+  Global Instance le_dec : RelDecision le.
+  Proof. intros s1 s2. apply _. Defined.
+  Global Instance le_pi s1 s2 : ProofIrrel (le s1 s2).
+  Proof. apply _. Qed.
+
+  Global Instance le_po : PartialOrder le.
+  Proof.
+    unfold le. split; [split|].
+    - intros s. unfold String.leb. assert ((s ?= s)%string = Eq) as ->; [|done].
+      induction s; simpl; [done|].
+      unfold Ascii.compare. by rewrite N.compare_refl.
+    - intros s1 s2 s3. unfold String.leb.
+      destruct (s1 ?= s2)%string eqn:Hs12; [..|done].
+      { by apply String.compare_eq_iff in Hs12 as ->. }
+      destruct (s2 ?= s3)%string eqn:Hs23; [..|done].
+      { apply String.compare_eq_iff in Hs23 as ->. by rewrite Hs12. }
+      assert ((s1 ?= s3)%string = Lt) as ->; [|done].
+      revert s2 s3 Hs12 Hs23.
+      induction s1 as [|a1 s1]; intros [|a2 s2] [|a3 s3] ??;
+        simplify_eq/=; [done..|].
+      destruct (Ascii.compare a1 a2) eqn:Ha12; simplify_eq/=.
+      { apply Ascii.compare_eq_iff in Ha12 as ->.
+        destruct (Ascii.compare a2 a3); simpl; eauto. }
+      destruct (Ascii.compare a2 a3) eqn:Ha23; simplify_eq/=.
+      { apply Ascii.compare_eq_iff in Ha23 as ->. by rewrite Ha12. }
+      assert (Ascii.compare a1 a3 = Lt) as ->; [|done].
+      apply N.compare_lt_iff. by etrans; apply N.compare_lt_iff.
+    - intros s1 s2 ?%Is_true_true ?%Is_true_true. by apply String.leb_antisym.
+  Qed.
+  Global Instance le_total : Total le.
+  Proof.
+    intros s1 s2. unfold le. destruct (String.leb_total s1 s2) as [->| ->]; auto.
+  Qed.
+
+  Global Instance app_inj s1 : Inj (=) (=) (app s1).
+  Proof. intros ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
+
+  Fixpoint rev_app (s1 s2 : string) : string :=
+    match s1 with
+    | "" => s2
+    | String a s1 => rev_app s1 (String a s2)
+    end.
+  Definition rev (s : string) : string := rev_app s "".
+
+  (* Break a string up into lists of words, delimited by white space *)
+  Fixpoint words_go (cur : option string) (s : string) : list string :=
+    match s with
+    | "" => option_list (rev <$> cur)
+    | String a s =>
+       if Ascii.is_space a
+       then option_list (rev <$> cur) ++ words_go None s
+       else words_go (Some (from_option (String a) (String a "") cur)) s
+    end.
+  Definition words : string → list string := words_go None.
+
+  Ltac words s :=
+    match type of s with
+    | list string => s
+    | string => eval vm_compute in (words s)
+    end.
+End String.
+
+Infix "≤" := String.le : string_scope.
+Notation "(≤)" := String.le (only parsing) : string_scope.
+Notation "x ≤ y ≤ z" := (x ≤ y ∧ y ≤ z)%string : string_scope.
+Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z')%string : string_scope.
+
+Global Hint Extern 0 (_ ≤ _)%string => reflexivity : core.
diff --git a/tests/ascii.ref b/tests/ascii.ref
new file mode 100644
index 0000000000000000000000000000000000000000..7be9366e465854c532e4c3c2f7f827c28a6c972e
--- /dev/null
+++ b/tests/ascii.ref
@@ -0,0 +1,8 @@
+"a"
+     : string
+"a"%char
+     : ascii
+"a"
+     : ascii
+"a"%stdpp
+     : string
diff --git a/tests/ascii.v b/tests/ascii.v
new file mode 100644
index 0000000000000000000000000000000000000000..54abf45a330874e317dafdc66991576a1b4ae5fb
--- /dev/null
+++ b/tests/ascii.v
@@ -0,0 +1,11 @@
+From stdpp Require Import strings.
+From Coq Require Import Ascii.
+
+Check "a". (* should be string *)
+
+Check "a"%char. (* should be ascii *)
+
+Open Scope char_scope.
+
+Check "a". (* should be ascii *)
+Check "a"%string. (* should be string *)
diff --git a/tests/pretty.v b/tests/pretty.v
index 6bb0768fce926b6a083e3a8f4b6abb633be0f69c..c154908a21664c96e8b99a6655ceaa511a3924d5 100644
--- a/tests/pretty.v
+++ b/tests/pretty.v
@@ -25,8 +25,8 @@ End N.
 Fixed by making the [wp_guard] in [pretty_N_go] proportional to the
 size of the input so that it blocks in case the input is an open term. *)
 Lemma test_no_stack_overflow p n :
-  get n (pretty (N.pos p)) ≠ Some "_"%char →
-  get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
+  String.get n (pretty (N.pos p)) ≠ Some "_"%char →
+  String.get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
 Proof. intros Hlem. apply Hlem. Qed.
 
 Section nat.
diff --git a/tests/strings.ref b/tests/strings.ref
index 9013eb935c0216264f283f27f7a87cb0d6955838..89e6579f3ef94f14538d9e7806951d31105cdd7a 100644
--- a/tests/strings.ref
+++ b/tests/strings.ref
@@ -1,8 +1,20 @@
+"foo"
+     : string
 "foo"
      : string
 10 =? 10
      : bool
 [10] ++ [12]
      : list nat
-"foo" +:+ "bar"
+("foo" =? "bar")%string
+     : bool
+String.app "foo" "bar"
      : string
+String.app
+     : string → string → string
+("a" ≤ "b")%string
+     : Prop
+     = true
+     : bool
+     = ["A"; "a"; "b"; "c"]
+     : list string
diff --git a/tests/strings.v b/tests/strings.v
index c88306aacfbd17dbdca7590f2e0c9285a33968d9..e1955dfc9b56e513d43b3bbaf4020fcf9f0f5739 100644
--- a/tests/strings.v
+++ b/tests/strings.v
@@ -1,13 +1,41 @@
-From stdpp Require Import strings.
+From stdpp Require Import strings sorting.
+From Coq Require Ascii.
 
 (** Check that the string notation works without [%string]. *)
 Check "foo".
 
+(** And also with [%string], which should not be pretty printed) *)
+Check "foo"%string.
+
 (** Check that importing [strings] does not override notations for [nat] and
 [list]. *)
 Check (10 =? 10).
 Check ([10] ++ [12]).
 
+Check ("foo" =? "bar")%string.
+
 (** Check that append on strings is pretty printed correctly, and not as
 [(_ ++ _)%string]. *)
 Check ("foo" +:+ "bar").
+
+(** Should print as [String.app] *)
+Check String.app.
+
+(** Test notations and type class instances for [≤] *)
+Check ("a" ≤ "b")%string.
+Compute bool_decide ("a" ≤ "b")%string.
+
+(** Make sure [merge_sort] computes (which implies the [Decision] instances
+are correct. *)
+Compute merge_sort (≤)%string ["b"; "a"; "c"; "A"].
+
+(** And that we can prove it actually sorts (which implies the order-related
+instances are correct. *)
+Lemma test_merge_sort l :
+  StronglySorted (≤)%string (merge_sort (≤)%string l) ∧
+  merge_sort (≤)%string l ≡ₚ l.
+Proof.
+  split.
+  - apply (StronglySorted_merge_sort _).
+  - apply merge_sort_Permutation.
+Qed.