diff --git a/Cslib.lean b/Cslib.lean
index 67b5d493..c4dbba7f 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -8,6 +8,7 @@ import Cslib.Computability.Automata.NFA
 import Cslib.Computability.Automata.NFAToDFA
 import Cslib.Computability.Languages.Language
 import Cslib.Computability.Languages.OmegaLanguage
+import Cslib.Computability.Languages.RegularLanguage
 import Cslib.Foundations.Control.Monad.Free
 import Cslib.Foundations.Control.Monad.Free.Effects
 import Cslib.Foundations.Control.Monad.Free.Fold
diff --git a/Cslib/Computability/Automata/DA.lean b/Cslib/Computability/Automata/DA.lean
index e7bb94ad..cb40f05b 100644
--- a/Cslib/Computability/Automata/DA.lean
+++ b/Cslib/Computability/Automata/DA.lean
@@ -6,19 +6,48 @@ Authors: Fabrizio Montesi
 
 import Cslib.Computability.Automata.NA
 
-
-
 /-! # Deterministic Automaton
 
 A Deterministic Automaton (DA) is an automaton defined by a transition function.
+
+## References
+
+* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
+  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
 namespace Cslib
 
-structure DA (State : Type _) (Symbol : Type _) where
+open List
+
+structure DA (State : Type*) (Symbol : Type*) where
   /-- The initial state of the automaton. -/
   start : State
   /-- The transition function of the automaton. -/
   tr : State → Symbol → State
 
+namespace DA
+
+variable {State State1 State2 : Type*} {Symbol : Type*}
+
+/-- Extended transition function. -/
+@[scoped grind =]
+def mtr (DA : DA State Symbol) (s : State) (xs : List Symbol) := xs.foldl DA.tr s
+
+@[simp, scoped grind =]
+theorem mtr_nil_eq {DA : DA State Symbol} {s : State} : DA.mtr s [] = s := rfl
+
+@[scoped grind =]
+def prod (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol where
+  start := (da1.start, da2.start)
+  tr := fun (s1, s2) x ↦ (da1.tr s1 x, da2.tr s2 x)
+
+@[simp, scoped grind =]
+theorem prod_mtr_eq (da1 : DA State1 Symbol) (da2 : DA State2 Symbol)
+    (s : State1 × State2) (xs : List Symbol) :
+    (da1.prod da2).mtr s xs = (da1.mtr s.fst xs, da2.mtr s.snd xs) := by
+  induction xs generalizing s <;> grind
+
+end DA
+
 end Cslib
diff --git a/Cslib/Computability/Automata/DFA.lean b/Cslib/Computability/Automata/DFA.lean
index 88c38b7f..64e6f782 100644
--- a/Cslib/Computability/Automata/DFA.lean
+++ b/Cslib/Computability/Automata/DFA.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fabrizio Montesi
+Authors: Fabrizio Montesi, Ching-Tsun Chou
 -/
 
 import Cslib.Computability.Automata.DA
@@ -11,19 +11,17 @@ import Cslib.Computability.Languages.Language
 
 A Deterministic Finite Automaton (DFA) is a finite-state machine that accepts or rejects
 a finite string.
-
-## References
-
-* [J. E. Hopcroft, R. Motwani, J. D. Ullman,
-  *Introduction to Automata Theory, Languages, and Computation*][Hopcroft2006]
 -/
 
 namespace Cslib
 
+open List Prod
+open scoped DA Language
+
 /-- A Deterministic Finite Automaton (DFA) consists of a labelled transition function
 `tr` over finite sets of states and labels (called symbols), a starting state `start` and a finite
 set of accepting states `accept`. -/
-structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
+structure DFA (State : Type*) (Symbol : Type*) extends DA State Symbol where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
@@ -33,18 +31,7 @@ structure DFA (State : Type _) (Symbol : Type _) extends DA State Symbol where
 
 namespace DFA
 
-variable {State : Type _} {Symbol : Type _}
-
-/-- Extended transition function.
-
-Implementation note: compared to [Hopcroft2006], the definition consumes the input list of symbols
-from the left (instead of the right), in order to match the way lists are constructed.
--/
-@[scoped grind =]
-def mtr (dfa : DFA State Symbol) (s : State) (xs : List Symbol) := xs.foldl dfa.tr s
-
-@[scoped grind =]
-theorem mtr_nil_eq {dfa : DFA State Symbol} {s : State} : dfa.mtr s [] = s := rfl
+variable {State State1 State2 : Type*} {Symbol : Type*}
 
 /-- A DFA accepts a string if there is a multi-step accepting derivative with that trace from
 the start state. -/
@@ -62,6 +49,71 @@ def language (dfa : DFA State Symbol) : Language Symbol :=
 theorem mem_language (dfa : DFA State Symbol) (xs : List Symbol) :
   xs ∈ dfa.language ↔ dfa.Accepts xs := Iff.rfl
 
+@[scoped grind =]
+def zero [Finite Symbol] : DFA Unit Symbol where
+  start := ()
+  tr := fun _ _ ↦ ()
+  accept := ∅
+  finite_state := by infer_instance
+  finite_symbol := by infer_instance
+
+@[simp, scoped grind =]
+theorem zero_lang [Finite Symbol] : zero.language = (0 : Language Symbol) := by
+  grind
+
+@[scoped grind =]
+def one [Finite Symbol] : DFA (Fin 2) Symbol where
+  start := 0
+  tr := fun _ _ ↦ 1
+  accept := {0}
+  finite_state := by infer_instance
+  finite_symbol := by infer_instance
+
+@[simp, scoped grind =]
+theorem one_lang [Finite Symbol] : one.language = (1 : Language Symbol) := by
+  ext xs ; constructor
+  · intro h ; by_contra h'
+    have := dropLast_append_getLast h'
+    grind
+  · grind [Language.mem_one]
+
+@[scoped grind =]
+def compl (dfa : DFA State Symbol) : DFA State Symbol :=
+  { dfa with accept := dfa.acceptᶜ }
+
+@[simp, scoped grind =]
+theorem compl_lang (dfa : DFA State Symbol) : dfa.compl.language = (dfa.language)ᶜ := by
+  grind
+
+@[scoped grind =]
+def prod (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) (acc : Set (State1 × State2))
+  : DFA (State1 × State2) Symbol where
+  toDA := DA.prod dfa1.toDA dfa2.toDA
+  accept := acc
+  finite_state := by
+    have := dfa1.finite_state
+    have := dfa2.finite_state
+    infer_instance
+  finite_symbol := dfa1.finite_symbol
+
+@[scoped grind =]
+def inf (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) :=
+    dfa1.prod dfa2 (fst ⁻¹' dfa1.accept ∩ snd ⁻¹' dfa2.accept)
+
+@[scoped grind =]
+def add (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) :=
+    dfa1.prod dfa2 (fst ⁻¹' dfa1.accept ∪ snd ⁻¹' dfa2.accept)
+
+@[simp, scoped grind =]
+theorem inf_lang (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) :
+    (dfa1.inf dfa2).language = dfa1.language ⊓ dfa2.language := by
+  ext xs ; grind
+
+@[simp, scoped grind =]
+theorem add_lang (dfa1 : DFA State1 Symbol) (dfa2 : DFA State2 Symbol) :
+    (dfa1.add dfa2).language = dfa1.language + dfa2.language := by
+  ext xs ; grind [Language.mem_add]
+
 end DFA
 
 end Cslib
diff --git a/Cslib/Computability/Automata/DFAToNFA.lean b/Cslib/Computability/Automata/DFAToNFA.lean
index 35602e71..25922bbc 100644
--- a/Cslib/Computability/Automata/DFAToNFA.lean
+++ b/Cslib/Computability/Automata/DFAToNFA.lean
@@ -11,9 +11,11 @@ import Cslib.Computability.Automata.NFA
 
 namespace Cslib
 
+open scoped DA
+
 namespace DFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section NFA
 
diff --git a/Cslib/Computability/Automata/EpsilonNFA.lean b/Cslib/Computability/Automata/EpsilonNFA.lean
index 69997dc1..86109f57 100644
--- a/Cslib/Computability/Automata/EpsilonNFA.lean
+++ b/Cslib/Computability/Automata/EpsilonNFA.lean
@@ -17,7 +17,7 @@ symbol type. The special symbol ε is represented by the `Option.none` case.
 Internally, ε (`Option.none`) is treated as the `τ` label of the underlying transition system,
 allowing for reusing the definitions and results on saturated transitions of `LTS` to deal with
 ε-closure. -/
-structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option Symbol) where
+structure εNFA (State : Type*) (Symbol : Type*) extends NA State (Option Symbol) where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
@@ -25,7 +25,7 @@ structure εNFA (State : Type _) (Symbol : Type _) extends NA State (Option Symb
   /-- The type of symbols (also called 'alphabet') is finite. -/
   finite_symbol : Finite Symbol
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 @[local grind =]
 private instance : HasTau (Option α) := ⟨.none⟩
diff --git a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean
index 445e14f4..f4ffc5c0 100644
--- a/Cslib/Computability/Automata/EpsilonNFAToNFA.lean
+++ b/Cslib/Computability/Automata/EpsilonNFAToNFA.lean
@@ -27,7 +27,7 @@ private lemma LTS.noε_saturate_tr
 
 namespace εNFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section NFA
 
@@ -41,7 +41,7 @@ def toNFA (enfa : εNFA State Symbol) : NFA State Symbol where
   finite_symbol := enfa.finite_symbol
 
 @[scoped grind =]
-lemma LTS.noε_saturate_mTr {s : State} {Label : Type _} {μs : List Label}
+lemma LTS.noε_saturate_mTr {s : State} {Label : Type*} {μs : List Label}
   {lts : LTS State (Option Label)} :
   lts.saturate.MTr s (μs.map (some ·)) = lts.saturate.noε.MTr s μs := by
   ext s'
diff --git a/Cslib/Computability/Automata/NA.lean b/Cslib/Computability/Automata/NA.lean
index 0c119cc1..a7b32a53 100644
--- a/Cslib/Computability/Automata/NA.lean
+++ b/Cslib/Computability/Automata/NA.lean
@@ -17,7 +17,7 @@ type `State → Symbol → Set State`; it gets automatically expanded to the for
 
 namespace Cslib
 
-structure NA (State : Type _) (Symbol : Type _) extends LTS State Symbol where
+structure NA (State : Type*) (Symbol : Type*) extends LTS State Symbol where
   /-- The set of initial states of the automaton. -/
   start : Set State
 
diff --git a/Cslib/Computability/Automata/NFA.lean b/Cslib/Computability/Automata/NFA.lean
index a83b9efb..dc34dc9d 100644
--- a/Cslib/Computability/Automata/NFA.lean
+++ b/Cslib/Computability/Automata/NFA.lean
@@ -11,7 +11,7 @@ namespace Cslib
 
 /-- A Nondeterministic Finite Automaton (NFA) is a nondeterministic automaton (NA)
 over finite sets of states and symbols. -/
-structure NFA (State : Type _) (Symbol : Type _) extends NA State Symbol where
+structure NFA (State : Type*) (Symbol : Type*) extends NA State Symbol where
   /-- The set of accepting states of the automaton. -/
   accept : Set State
   /-- The automaton is finite-state. -/
@@ -21,7 +21,7 @@ structure NFA (State : Type _) (Symbol : Type _) extends NA State Symbol where
 
 namespace NFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 /-- An NFA accepts a string if there is a multi-step accepting derivative with that trace from
 the start state. -/
diff --git a/Cslib/Computability/Automata/NFAToDFA.lean b/Cslib/Computability/Automata/NFAToDFA.lean
index 1536b662..f5207c3a 100644
--- a/Cslib/Computability/Automata/NFAToDFA.lean
+++ b/Cslib/Computability/Automata/NFAToDFA.lean
@@ -13,7 +13,7 @@ namespace Cslib
 
 namespace NFA
 
-variable {State : Type _} {Symbol : Type _}
+variable {State : Type*} {Symbol : Type*}
 
 section SubsetConstruction
 
@@ -41,7 +41,7 @@ original NA. -/
 @[scoped grind =]
 theorem toDFA_mem_mtr {nfa : NFA State Symbol} {S : Set State} {s' : State} {xs : List Symbol} :
   s' ∈ nfa.toDFA.mtr S xs ↔ ∃ s ∈ S, nfa.MTr s xs s' := by
-  simp only [NFA.toDFA, DFA.mtr]
+  simp only [NFA.toDFA, DA.mtr]
   /- TODO: Grind does not catch a useful rewrite in the subset construction for automata
 
     A very similar issue seems to occur in the proof of `NFA.toDFA_language_eq`.
diff --git a/Cslib/Computability/Languages/Language.lean b/Cslib/Computability/Languages/Language.lean
index 1cd97437..da1e95cf 100644
--- a/Cslib/Computability/Languages/Language.lean
+++ b/Cslib/Computability/Languages/Language.lean
@@ -20,7 +20,25 @@ namespace Language
 open Set List
 open scoped Computability
 
-variable {α : Type _} {l : Language α}
+variable {α : Type*} {l m : Language α}
+
+@[simp, scoped grind =]
+theorem mem_inf (x : List α) : x ∈ l ⊓ m ↔ x ∈ l ∧ x ∈ m :=
+  Iff.rfl
+
+@[simp]
+theorem mem_biInf {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
+    (x ∈ ⨅ i ∈ s, l i) ↔ ∀ i ∈ s, x ∈ l i :=
+  mem_iInter₂
+
+@[simp]
+theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
+    (x ∈ ⨆ i ∈ s, l i) ↔ ∃ i ∈ s, x ∈ l i := by
+  constructor <;> intro h
+  · have := mem_iUnion₂.mp h
+    grind
+  · apply mem_iUnion₂.mpr
+    grind
 
 -- This section will be removed once the following PR gets into mathlib:
 -- https://github.com/leanprover-community/mathlib4/pull/30913
diff --git a/Cslib/Computability/Languages/OmegaLanguage.lean b/Cslib/Computability/Languages/OmegaLanguage.lean
index cb6d0239..dc646fd7 100644
--- a/Cslib/Computability/Languages/OmegaLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaLanguage.lean
@@ -59,7 +59,7 @@ open scoped Computability
 
 universe v
 
-variable {α β γ : Type _}
+variable {α β γ : Type*}
 
 /-- An ω-language is a set of strings over an alphabet. -/
 def ωLanguage (α) :=
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
new file mode 100644
index 00000000..a566e4d4
--- /dev/null
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2025 Ching-Tsun Chou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ching-Tsun Chou
+-/
+
+import Cslib.Computability.Automata.DFAToNFA
+import Cslib.Computability.Automata.NFAToDFA
+import Mathlib.Computability.DFA
+import Mathlib.Tactic
+
+/-!
+# Regular languages
+-/
+
+open Set Function
+open scoped Computability
+
+namespace Language
+
+variable {Symbol : Type*} [Finite Symbol]
+
+/-- A characterization of Language.IsRegular using Cslib.DFA -/
+theorem IsRegular.iff_cslib_dfa {l : Language Symbol} :
+    l.IsRegular ↔ ∃ State : Type, ∃ dfa : Cslib.DFA State Symbol, dfa.language = l := by
+  constructor
+  · rintro ⟨State, h_State, dfa, rfl⟩
+    let dfa' : Cslib.DFA State Symbol := {
+      start := dfa.start
+      tr := dfa.step
+      accept := dfa.accept
+      finite_state := Fintype.finite h_State
+      finite_symbol := by infer_instance }
+    use State, dfa'
+    rfl
+  · rintro ⟨State, dfa, rfl⟩
+    let dfa' : DFA Symbol State := {
+      start := dfa.start
+      step := dfa.tr
+      accept := dfa.accept }
+    have := dfa.finite_state
+    use State, (Fintype.ofFinite State), dfa'
+    rfl
+
+/-- A characterization of Language.IsRegular using Cslib.NFA -/
+theorem IsRegular.iff_cslib_nfa {l : Language Symbol} :
+    l.IsRegular ↔ ∃ State : Type, ∃ nfa : Cslib.NFA State Symbol, nfa.language = l := by
+  rw [IsRegular.iff_cslib_dfa] ; constructor
+  · rintro ⟨State, dfa, rfl⟩
+    use State, dfa.toNFA
+    exact Cslib.DFA.toNFA_language_eq
+  · rintro ⟨State, nfa, rfl⟩
+    use (Set State), nfa.toDFA
+    exact Cslib.NFA.toDFA_language_eq
+
+-- From this point onward we will use only automata from Cslib in the proofs.
+open Cslib
+
+@[simp]
+theorem IsRegular.compl {l : Language Symbol} (h : l.IsRegular) : (lᶜ).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa] at h ⊢
+  obtain ⟨State, dfa, rfl⟩ := h
+  use State, dfa.compl
+  simp
+
+@[simp]
+theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa]
+  use Unit, DFA.zero
+  simp
+
+@[simp]
+theorem IsRegular.one : (1 : Language Symbol).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa]
+  use Fin 2, DFA.one
+  simp
+
+@[simp]
+theorem IsRegular.top : (⊤ : Language Symbol).IsRegular := by
+  have : (⊥ᶜ : Language Symbol).IsRegular := IsRegular.compl <| IsRegular.zero (Symbol := Symbol)
+  rwa [← compl_bot]
+
+@[simp]
+theorem IsRegular.inf {l1 l2 : Language Symbol}
+    (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 ⊓ l2).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa] at h1 h2 ⊢
+  obtain ⟨State1, dfa1, rfl⟩ := h1
+  obtain ⟨State2, dfa2, rfl⟩ := h2
+  use (State1 × State2), (dfa1.inf dfa2)
+  simp
+
+@[simp]
+theorem IsRegular.add {l1 l2 : Language Symbol}
+    (h1 : l1.IsRegular) (h2 : l2.IsRegular) : (l1 + l2).IsRegular := by
+  rw [IsRegular.iff_cslib_dfa] at h1 h2 ⊢
+  obtain ⟨State1, dfa1, rfl⟩ := h1
+  obtain ⟨State2, dfa2, rfl⟩ := h2
+  use (State1 × State2), (dfa1.add dfa2)
+  simp
+
+@[simp]
+theorem IsRegular.iInf {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}
+    (h : ∀ i ∈ s, (l i).IsRegular) : (⨅ i ∈ s, l i).IsRegular := by
+  generalize h_n : s.ncard = n
+  induction n generalizing s
+  case zero =>
+    obtain ⟨rfl⟩ := (ncard_eq_zero (s := s)).mp h_n
+    simp
+  case succ n h_ind =>
+    obtain ⟨i, t, h_i, rfl, rfl⟩ := (ncard_eq_succ (s := s)).mp h_n
+    rw [iInf_insert]
+    grind [IsRegular.inf]
+
+@[simp]
+theorem IsRegular.iSup {I : Type*} [Finite I] {s : Set I} {l : I → Language Symbol}
+    (h : ∀ i ∈ s, (l i).IsRegular) : (⨆ i ∈ s, l i).IsRegular := by
+  generalize h_n : s.ncard = n
+  induction n generalizing s
+  case zero =>
+    obtain ⟨rfl⟩ := (ncard_eq_zero (s := s)).mp h_n
+    simp only [mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot]
+    exact IsRegular.zero
+  case succ n h_ind =>
+    obtain ⟨i, t, h_i, rfl, rfl⟩ := (ncard_eq_succ (s := s)).mp h_n
+    rw [iSup_insert]
+    apply IsRegular.add <;> grind
+
+end Language