diff --git a/metadata/entries/Binary_Code_Imprimitive.toml b/metadata/entries/Binary_Code_Imprimitive.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Binary_Code_Imprimitive.toml
@@ -0,0 +1,38 @@
+title = "Binary codes that do not preserve primitivity"
+date = 2023-01-03
+topics = [
+  "Computer science/Automata and formal languages",
+]
+abstract = """
+A code $X$ is not primitivity preserving if there is a primitive list $\\mathtt{ws} \\in \\mathtt{lists} \\ X$ whose concatenation is imprimitive. We formalize a full characterization of such codes in the binary case in the proof assistant Isabelle/HOL. Part of the formalization, interesting on its own, is a description of $\\{x,y\\}$-interpretations of the square $xx$ if $\\mathtt{length}\\ y \\leq \\mathtt{length} \\ x$. We also provide a formalized parametric solution of the related equation $x^jy^k = z^\\ell$.
+
+The core of the theory is an investigation of imprimitive words which are concatenations of copies of two noncommuting words (such a pair of words is called a binary code). We follow the article <a href=”https://dx.doi.org/10.1016/0304-3975(85)90060-X”>[Barbin-Le Rest, Le Rest, 85]</a> (mainly Théorème 2.1 and Lemme 3.1), while substantially optimizing the proof. See also [J.-C. Spehner. Quelques problèmes d’extension, de conjugaison et de présentation des sous-monoïdes d’un monoïde libre. PhD thesis, Université Paris VII, 1976] for an earlier result on this question, and <a href=”https://dx.doir.org/10.46298/dmtcs.279”>[Maňuch, 01]</a> for another proof."""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.holub]
+email = "holub_email"
+
+[authors.raska]
+
+[contributors]
+
+[notify]
+holub = "holub_email"
+starosta = "starosta_email"
+
+[history]
+
+[extra]
+
+[related]
+dois = [
+  "10.1016/0304-3975(85)90060-X",
+  "10.46298/dmtcs.279",
+]
+pubs = [
+  "J.-C. Spehner. Quelques problèmes d’extension, de conjugaison et de présentation des sous-monoïdes d’un monoïde libre. PhD thesis, Université Paris VII, 1976",
+  "<a href=\"https://gitlab.com/formalcow/combinatorics-on-words-formalized\">Development repository</a>",
+]
diff --git a/metadata/entries/Two_Generated_Word_Monoids_Intersection.toml b/metadata/entries/Two_Generated_Word_Monoids_Intersection.toml
new file mode 100644
--- /dev/null
+++ b/metadata/entries/Two_Generated_Word_Monoids_Intersection.toml
@@ -0,0 +1,41 @@
+title = "Intersection of two monoids generated by two element codes"
+date = 2023-01-03
+topics = [
+  "Computer science/Automata and formal languages",
+]
+abstract = """
+This article provides a formalization of the classification of intersection
+\\( \\{x,y\\}^* \\cap \\{u,v\\}^*\\) of two monoids generated by two element codes.
+Namely, the intersection has one of the following forms
+\\( \\{\\beta,\\gamma\\}^* \\quad \\text{ or } \\quad \\left(\\beta_0 + \\beta(\\gamma(1+\\delta+ \\cdots + \\delta^t))^*\\epsilon\\right)^*.\\)
+Note that it can be infinitely generated.
+
+The result is due to <a href=”https://doi.org/10.1007/BFb0036924”>[Karhumäki, 84]</a>. Our proof uses the terminology of morphisms which allows us to formulate the result in a shorter and more transparent way."""
+license = "bsd"
+note = ""
+
+[authors]
+
+[authors.holub]
+email = "holub_email"
+
+[authors.starosta]
+email = "starosta_email"
+
+[contributors]
+
+[notify]
+holub = "holub_email"
+starosta = "starosta_email"
+
+[history]
+
+[extra]
+
+[related]
+dois = [
+  "10.1007/BFb0036924",
+]
+pubs = [
+  "<a href=\"https://gitlab.com/formalcow/combinatorics-on-words-formalized\">Development repository</a>",
+]