diff --git a/Strata.lean b/Strata.lean
index dc39e7b69..fd9ead31c 100644
--- a/Strata.lean
+++ b/Strata.lean
@@ -11,9 +11,9 @@ import Strata.DDM.Integration.Lean
 import Strata.DDM.Ion
 
 /- Dialect Library -/
-import Strata.DL.SMT.SMT
-import Strata.DL.Lambda.Lambda
-import Strata.DL.Imperative.Imperative
+import Strata.Dialects.SMT.SMT
+import Strata.Dialects.Lambda.Lambda
+import Strata.Dialects.Imperative.Imperative
 
 /- Boogie -/
 import Strata.Languages.Boogie.Examples.Examples
diff --git a/Strata/Backends/CBMC/BoogieToCBMC.lean b/Strata/Backends/CBMC/BoogieToCBMC.lean
index cd975a809..0216723f8 100644
--- a/Strata/Backends/CBMC/BoogieToCBMC.lean
+++ b/Strata/Backends/CBMC/BoogieToCBMC.lean
@@ -8,7 +8,7 @@ import Lean.Data.Json
 import Strata.Languages.Boogie.Env
 import Strata.Languages.Boogie.DDMTransform.Parse
 import Strata.Languages.Boogie.DDMTransform.Translate
-import Strata.DL.Util.Map
+import Strata.Dialects.Util.Map
 import Strata.Languages.Boogie.Boogie
 import Strata.Backends.CBMC.Common
 
diff --git a/Strata/Backends/CBMC/Common.lean b/Strata/Backends/CBMC/Common.lean
index 1fc9bebdf..1e2a2a6cb 100644
--- a/Strata/Backends/CBMC/Common.lean
+++ b/Strata/Backends/CBMC/Common.lean
@@ -5,7 +5,7 @@
 -/
 
 import Lean.Data.Json
-import Strata.DL.Util.Map
+import Strata.Dialects.Util.Map
 
 -------------------------------------------------------------------------------
 
diff --git a/Strata/Backends/CBMC/StrataToCBMC.lean b/Strata/Backends/CBMC/StrataToCBMC.lean
index 1685faded..989d57870 100644
--- a/Strata/Backends/CBMC/StrataToCBMC.lean
+++ b/Strata/Backends/CBMC/StrataToCBMC.lean
@@ -5,7 +5,7 @@
 -/
 
 import Lean.Data.Json
-import Strata.DL.Util.Map
+import Strata.Dialects.Util.Map
 import Strata.Languages.C_Simp.C_Simp
 import Strata.Languages.C_Simp.Verify
 import Strata.Backends.CBMC.Common
diff --git a/Strata/DL/Imperative/Imperative.lean b/Strata/DL/Imperative/Imperative.lean
deleted file mode 100644
index a219be614..000000000
--- a/Strata/DL/Imperative/Imperative.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
-import Strata.DL.Imperative.PureExpr
-import Strata.DL.Imperative.HasVars
-import Strata.DL.Imperative.MetaData
-
-import Strata.DL.Imperative.CmdEval
-import Strata.DL.Imperative.CmdType
-import Strata.DL.Imperative.CmdSemantics
-import Strata.DL.Imperative.StmtSemantics
-import Strata.DL.Imperative.StmtSemanticsSmallStep
-
-import Strata.DL.Imperative.NondetStmt
-import Strata.DL.Imperative.NondetStmtSemantics
-
-import Strata.DL.Imperative.SemanticsProps
-
-import Strata.DL.Imperative.SMTUtils
diff --git a/Strata/DL/SMT/SMT.lean b/Strata/DL/SMT/SMT.lean
deleted file mode 100644
index f78491cad..000000000
--- a/Strata/DL/SMT/SMT.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
-import Strata.DL.SMT.Basic
-import Strata.DL.SMT.CexParser
-import Strata.DL.SMT.Encoder
-import Strata.DL.SMT.Factory
-import Strata.DL.SMT.Function
-import Strata.DL.SMT.Op
-import Strata.DL.SMT.Solver
-import Strata.DL.SMT.Term
-import Strata.DL.SMT.TermType
diff --git a/Strata/DL/Imperative/Cmd.lean b/Strata/Dialects/Imperative/Cmd.lean
similarity index 97%
rename from Strata/DL/Imperative/Cmd.lean
rename to Strata/Dialects/Imperative/Cmd.lean
index 2073321cf..a98a24241 100644
--- a/Strata/DL/Imperative/Cmd.lean
+++ b/Strata/Dialects/Imperative/Cmd.lean
@@ -4,10 +4,10 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.PureExpr
-import Strata.DL.Imperative.MetaData
-import Strata.DL.Imperative.HasVars
-import Strata.DL.Lambda.LExpr
+import Strata.Dialects.Imperative.PureExpr
+import Strata.Dialects.Imperative.MetaData
+import Strata.Dialects.Imperative.HasVars
+import Strata.Dialects.Lambda.LExpr
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/DL/Imperative/CmdEval.lean b/Strata/Dialects/Imperative/CmdEval.lean
similarity index 97%
rename from Strata/DL/Imperative/CmdEval.lean
rename to Strata/Dialects/Imperative/CmdEval.lean
index 2005abd55..5f662004b 100644
--- a/Strata/DL/Imperative/CmdEval.lean
+++ b/Strata/Dialects/Imperative/CmdEval.lean
@@ -6,8 +6,8 @@
 
 
 
-import Strata.DL.Imperative.Cmd
-import Strata.DL.Imperative.EvalContext
+import Strata.Dialects.Imperative.Cmd
+import Strata.Dialects.Imperative.EvalContext
 
 namespace Imperative
 open Std (ToFormat Format format)
diff --git a/Strata/DL/Imperative/CmdSemantics.lean b/Strata/Dialects/Imperative/CmdSemantics.lean
similarity index 98%
rename from Strata/DL/Imperative/CmdSemantics.lean
rename to Strata/Dialects/Imperative/CmdSemantics.lean
index 3aa6a1b77..51e0d2bd4 100644
--- a/Strata/DL/Imperative/CmdSemantics.lean
+++ b/Strata/Dialects/Imperative/CmdSemantics.lean
@@ -4,10 +4,10 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.Stmt
-import Strata.DL.Imperative.HasVars
-import Strata.DL.Util.Map
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Imperative.Stmt
+import Strata.Dialects.Imperative.HasVars
+import Strata.Dialects.Util.Map
+import Strata.Dialects.Util.ListUtils
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/DL/Imperative/CmdType.lean b/Strata/Dialects/Imperative/CmdType.lean
similarity index 96%
rename from Strata/DL/Imperative/CmdType.lean
rename to Strata/Dialects/Imperative/CmdType.lean
index 29b421d08..b756f69c8 100644
--- a/Strata/DL/Imperative/CmdType.lean
+++ b/Strata/Dialects/Imperative/CmdType.lean
@@ -6,8 +6,8 @@
 
 
 
-import Strata.DL.Imperative.Cmd
-import Strata.DL.Imperative.TypeContext
+import Strata.Dialects.Imperative.Cmd
+import Strata.Dialects.Imperative.TypeContext
 
 namespace Imperative
 open Std (ToFormat Format format)
diff --git a/Strata/DL/Imperative/EvalContext.lean b/Strata/Dialects/Imperative/EvalContext.lean
similarity index 95%
rename from Strata/DL/Imperative/EvalContext.lean
rename to Strata/Dialects/Imperative/EvalContext.lean
index 1f5540dcc..03b321f57 100644
--- a/Strata/DL/Imperative/EvalContext.lean
+++ b/Strata/Dialects/Imperative/EvalContext.lean
@@ -6,11 +6,11 @@
 
 
 
-import Strata.DL.Imperative.Cmd
-import Strata.DL.Imperative.EvalError
-import Strata.DL.Imperative.MetaData
-import Strata.DL.Util.ListMap
-import Strata.DL.Util.Maps
+import Strata.Dialects.Imperative.Cmd
+import Strata.Dialects.Imperative.EvalError
+import Strata.Dialects.Imperative.MetaData
+import Strata.Dialects.Util.ListMap
+import Strata.Dialects.Util.Maps
 
 namespace Imperative
 open Std (ToFormat Format format)
diff --git a/Strata/DL/Imperative/EvalError.lean b/Strata/Dialects/Imperative/EvalError.lean
similarity index 97%
rename from Strata/DL/Imperative/EvalError.lean
rename to Strata/Dialects/Imperative/EvalError.lean
index e9de28ead..171e9e09b 100644
--- a/Strata/DL/Imperative/EvalError.lean
+++ b/Strata/Dialects/Imperative/EvalError.lean
@@ -6,7 +6,7 @@
 
 
 
-import Strata.DL.Imperative.PureExpr
+import Strata.Dialects.Imperative.PureExpr
 
 namespace Imperative
 open Std (ToFormat Format format)
diff --git a/Strata/DL/Imperative/HasVars.lean b/Strata/Dialects/Imperative/HasVars.lean
similarity index 97%
rename from Strata/DL/Imperative/HasVars.lean
rename to Strata/Dialects/Imperative/HasVars.lean
index ef4dff3a1..d5e715f77 100644
--- a/Strata/DL/Imperative/HasVars.lean
+++ b/Strata/Dialects/Imperative/HasVars.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.PureExpr
+import Strata.Dialects.Imperative.PureExpr
 
 -- open Imperative Boogie
 namespace Imperative
diff --git a/Strata/Dialects/Imperative/Imperative.lean b/Strata/Dialects/Imperative/Imperative.lean
new file mode 100644
index 000000000..b5dafad59
--- /dev/null
+++ b/Strata/Dialects/Imperative/Imperative.lean
@@ -0,0 +1,22 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Dialects.Imperative.PureExpr
+import Strata.Dialects.Imperative.HasVars
+import Strata.Dialects.Imperative.MetaData
+
+import Strata.Dialects.Imperative.CmdEval
+import Strata.Dialects.Imperative.CmdType
+import Strata.Dialects.Imperative.CmdSemantics
+import Strata.Dialects.Imperative.StmtSemantics
+import Strata.Dialects.Imperative.StmtSemanticsSmallStep
+
+import Strata.Dialects.Imperative.NondetStmt
+import Strata.Dialects.Imperative.NondetStmtSemantics
+
+import Strata.Dialects.Imperative.SemanticsProps
+
+import Strata.Dialects.Imperative.SMTUtils
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/Dialects/Imperative/MetaData.lean
similarity index 98%
rename from Strata/DL/Imperative/MetaData.lean
rename to Strata/Dialects/Imperative/MetaData.lean
index e27866997..ef78a15bc 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/Dialects/Imperative/MetaData.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.PureExpr
-import Strata.DL.Util.DecidableEq
+import Strata.Dialects.Imperative.PureExpr
+import Strata.Dialects.Util.DecidableEq
 
 namespace Imperative
 
diff --git a/Strata/DL/Imperative/NondetStmt.lean b/Strata/Dialects/Imperative/NondetStmt.lean
similarity index 96%
rename from Strata/DL/Imperative/NondetStmt.lean
rename to Strata/Dialects/Imperative/NondetStmt.lean
index 2eb88f87e..34e353829 100644
--- a/Strata/DL/Imperative/NondetStmt.lean
+++ b/Strata/Dialects/Imperative/NondetStmt.lean
@@ -6,9 +6,9 @@
 
 
 
-import Strata.DL.Imperative.MetaData
-import Strata.DL.Imperative.Stmt
-import Strata.DL.Imperative.HasVars
+import Strata.Dialects.Imperative.MetaData
+import Strata.Dialects.Imperative.Stmt
+import Strata.Dialects.Imperative.HasVars
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/DL/Imperative/NondetStmtSemantics.lean b/Strata/Dialects/Imperative/NondetStmtSemantics.lean
similarity index 94%
rename from Strata/DL/Imperative/NondetStmtSemantics.lean
rename to Strata/Dialects/Imperative/NondetStmtSemantics.lean
index ba01e3fe5..a27092e1f 100644
--- a/Strata/DL/Imperative/NondetStmtSemantics.lean
+++ b/Strata/Dialects/Imperative/NondetStmtSemantics.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.CmdSemantics
-import Strata.DL.Imperative.NondetStmt
+import Strata.Dialects.Imperative.CmdSemantics
+import Strata.Dialects.Imperative.NondetStmt
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/DL/Imperative/PureExpr.lean b/Strata/Dialects/Imperative/PureExpr.lean
similarity index 100%
rename from Strata/DL/Imperative/PureExpr.lean
rename to Strata/Dialects/Imperative/PureExpr.lean
diff --git a/Strata/DL/Imperative/SMTUtils.lean b/Strata/Dialects/Imperative/SMTUtils.lean
similarity index 98%
rename from Strata/DL/Imperative/SMTUtils.lean
rename to Strata/Dialects/Imperative/SMTUtils.lean
index 832238382..877114fcf 100644
--- a/Strata/DL/Imperative/SMTUtils.lean
+++ b/Strata/Dialects/Imperative/SMTUtils.lean
@@ -4,9 +4,9 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.SMT.SMT
-import Strata.DL.Imperative.PureExpr
-import Strata.DL.Imperative.EvalContext
+import Strata.Dialects.SMT.SMT
+import Strata.Dialects.Imperative.PureExpr
+import Strata.Dialects.Imperative.EvalContext
 
 namespace Imperative
 open Std (ToFormat Format format)
diff --git a/Strata/DL/Imperative/SemanticsProps.lean b/Strata/Dialects/Imperative/SemanticsProps.lean
similarity index 98%
rename from Strata/DL/Imperative/SemanticsProps.lean
rename to Strata/Dialects/Imperative/SemanticsProps.lean
index 196709db4..40f877f17 100644
--- a/Strata/DL/Imperative/SemanticsProps.lean
+++ b/Strata/Dialects/Imperative/SemanticsProps.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.CmdSemantics
-import Strata.DL.Imperative.StmtSemantics
+import Strata.Dialects.Imperative.CmdSemantics
+import Strata.Dialects.Imperative.StmtSemantics
 
 namespace Imperative
 
diff --git a/Strata/DL/Imperative/Stmt.lean b/Strata/Dialects/Imperative/Stmt.lean
similarity index 99%
rename from Strata/DL/Imperative/Stmt.lean
rename to Strata/Dialects/Imperative/Stmt.lean
index fb9c20d79..4d2f57bed 100644
--- a/Strata/DL/Imperative/Stmt.lean
+++ b/Strata/Dialects/Imperative/Stmt.lean
@@ -6,7 +6,7 @@
 
 
 
-import Strata.DL.Imperative.Cmd
+import Strata.Dialects.Imperative.Cmd
 
 namespace Imperative
 ---------------------------------------------------------------------
diff --git a/Strata/DL/Imperative/StmtSemantics.lean b/Strata/Dialects/Imperative/StmtSemantics.lean
similarity index 99%
rename from Strata/DL/Imperative/StmtSemantics.lean
rename to Strata/Dialects/Imperative/StmtSemantics.lean
index d9c0dca3d..3b397dbcd 100644
--- a/Strata/DL/Imperative/StmtSemantics.lean
+++ b/Strata/Dialects/Imperative/StmtSemantics.lean
@@ -6,7 +6,7 @@
 
 
 
-import Strata.DL.Imperative.CmdSemantics
+import Strata.Dialects.Imperative.CmdSemantics
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/DL/Imperative/StmtSemanticsSmallStep.lean b/Strata/Dialects/Imperative/StmtSemanticsSmallStep.lean
similarity index 99%
rename from Strata/DL/Imperative/StmtSemanticsSmallStep.lean
rename to Strata/Dialects/Imperative/StmtSemanticsSmallStep.lean
index 028f5f579..85df16394 100644
--- a/Strata/DL/Imperative/StmtSemanticsSmallStep.lean
+++ b/Strata/Dialects/Imperative/StmtSemanticsSmallStep.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.CmdSemantics
+import Strata.Dialects.Imperative.CmdSemantics
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/DL/Imperative/ToCProverGOTO.lean b/Strata/Dialects/Imperative/ToCProverGOTO.lean
similarity index 99%
rename from Strata/DL/Imperative/ToCProverGOTO.lean
rename to Strata/Dialects/Imperative/ToCProverGOTO.lean
index 675c7f1dc..f7c0381f2 100644
--- a/Strata/DL/Imperative/ToCProverGOTO.lean
+++ b/Strata/Dialects/Imperative/ToCProverGOTO.lean
@@ -5,7 +5,7 @@
 -/
 
 import Strata.Backends.CBMC.GOTO.Program
-import Strata.DL.Imperative.Imperative
+import Strata.Dialects.Imperative.Imperative
 
 open Std (ToFormat Format format)
 
diff --git a/Strata/DL/Imperative/TypeContext.lean b/Strata/Dialects/Imperative/TypeContext.lean
similarity index 95%
rename from Strata/DL/Imperative/TypeContext.lean
rename to Strata/Dialects/Imperative/TypeContext.lean
index 84189606e..5853807f8 100644
--- a/Strata/DL/Imperative/TypeContext.lean
+++ b/Strata/Dialects/Imperative/TypeContext.lean
@@ -6,7 +6,7 @@
 
 
 
-import Strata.DL.Imperative.Cmd
+import Strata.Dialects.Imperative.Cmd
 
 namespace Imperative
 open Std (ToFormat Format format)
diff --git a/Strata/DL/Lambda/Factory.lean b/Strata/Dialects/Lambda/Factory.lean
similarity index 96%
rename from Strata/DL/Lambda/Factory.lean
rename to Strata/Dialects/Lambda/Factory.lean
index 00e091277..b9a83e0fd 100644
--- a/Strata/DL/Lambda/Factory.lean
+++ b/Strata/Dialects/Lambda/Factory.lean
@@ -4,21 +4,21 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprWF
-import Strata.DL.Lambda.LTy
-import Strata.DL.Util.ListMap
+import Strata.Dialects.Lambda.LExprWF
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.Util.ListMap
 
 /-!
 ## Lambda's Factory
 
 This module formalizes Lambda's _factory_, which is a mechanism to extend the
-type checker (see `Strata.DL.Lambda.LExprT`) and partial evaluator (see
-`Strata.DL.Lambda.LExprEval`) by providing a map from operations to their types
+type checker (see `Strata.Dialects.Lambda.LExprT`) and partial evaluator (see
+`Strata.Dialects.Lambda.LExprEval`) by providing a map from operations to their types
 and optionally, denotations. The factory allows adding type checking and
 evaluation support for new operations without modifying the implementation of
 either or any core ASTs.
 
-Also see `Strata.DL.Lambda.IntBoolFactory` for a concrete example of a factory.
+Also see `Strata.Dialects.Lambda.IntBoolFactory` for a concrete example of a factory.
 -/
 
 
diff --git a/Strata/DL/Lambda/Identifiers.lean b/Strata/Dialects/Lambda/Identifiers.lean
similarity index 98%
rename from Strata/DL/Lambda/Identifiers.lean
rename to Strata/Dialects/Lambda/Identifiers.lean
index 3f1b24354..fed43f8d2 100644
--- a/Strata/DL/Lambda/Identifiers.lean
+++ b/Strata/Dialects/Lambda/Identifiers.lean
@@ -6,8 +6,8 @@
 
 
 
-import Strata.DL.Lambda.LTy
-import Strata.DL.Util.Map
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.Util.Map
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/DL/Lambda/IntBoolFactory.lean b/Strata/Dialects/Lambda/IntBoolFactory.lean
similarity index 98%
rename from Strata/DL/Lambda/IntBoolFactory.lean
rename to Strata/Dialects/Lambda/IntBoolFactory.lean
index 558f2c775..f789ef3fa 100644
--- a/Strata/DL/Lambda/IntBoolFactory.lean
+++ b/Strata/Dialects/Lambda/IntBoolFactory.lean
@@ -4,11 +4,11 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LState
+import Strata.Dialects.Lambda.LState
 
 /-! ## A Minimal Factory with Support for Unbounded Integer and Boolean Operations
 
-See also `Strata.DL.Lambda.Factory`.
+See also `Strata.Dialects.Lambda.Factory`.
 -/
 
 ---------------------------------------------------------------------
diff --git a/Strata/DL/Lambda/LExpr.lean b/Strata/Dialects/Lambda/LExpr.lean
similarity index 99%
rename from Strata/DL/Lambda/LExpr.lean
rename to Strata/Dialects/Lambda/LExpr.lean
index 19bc6939c..5523d81d1 100644
--- a/Strata/DL/Lambda/LExpr.lean
+++ b/Strata/Dialects/Lambda/LExpr.lean
@@ -4,15 +4,15 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LTy
-import Strata.DL.Lambda.Identifiers
-import Strata.DL.Lambda.MetaData
-import Strata.DL.Util.DecidableEq
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.Lambda.Identifiers
+import Strata.Dialects.Lambda.MetaData
+import Strata.Dialects.Util.DecidableEq
 
 /-! ## Lambda Expressions with Quantifiers
 
 Lambda expressions are formalized by the inductive type `LExpr`. Type
-formalization is described in `Strata.DL.Lambda.LTy`.
+formalization is described in `Strata.Dialects.Lambda.LTy`.
 -/
 
 ---------------------------------------------------------------------
diff --git a/Strata/DL/Lambda/LExprEval.lean b/Strata/Dialects/Lambda/LExprEval.lean
similarity index 99%
rename from Strata/DL/Lambda/LExprEval.lean
rename to Strata/Dialects/Lambda/LExprEval.lean
index 2f805345f..d09d5fa40 100644
--- a/Strata/DL/Lambda/LExprEval.lean
+++ b/Strata/Dialects/Lambda/LExprEval.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprWF
-import Strata.DL.Lambda.LState
+import Strata.Dialects.Lambda.LExprWF
+import Strata.Dialects.Lambda.LState
 
 /-! ## Partial evaluator for Lambda expressions
 
diff --git a/Strata/DL/Lambda/LExprT.lean b/Strata/Dialects/Lambda/LExprT.lean
similarity index 99%
rename from Strata/DL/Lambda/LExprT.lean
rename to Strata/Dialects/Lambda/LExprT.lean
index eb42bfb32..240fa637d 100644
--- a/Strata/DL/Lambda/LExprT.lean
+++ b/Strata/Dialects/Lambda/LExprT.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprTypeEnv
-import Strata.DL.Lambda.LExprWF
+import Strata.Dialects.Lambda.LExprTypeEnv
+import Strata.Dialects.Lambda.LExprWF
 
 /-! ## Type Inference Transform for Lambda Expressions.
 
diff --git a/Strata/DL/Lambda/LExprType.lean b/Strata/Dialects/Lambda/LExprType.lean
similarity index 51%
rename from Strata/DL/Lambda/LExprType.lean
rename to Strata/Dialects/Lambda/LExprType.lean
index 2f68063d3..e795ba9d8 100644
--- a/Strata/DL/Lambda/LExprType.lean
+++ b/Strata/Dialects/Lambda/LExprType.lean
@@ -4,5 +4,5 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprTypeSpec
-import Strata.DL.Lambda.LExprT
+import Strata.Dialects.Lambda.LExprTypeSpec
+import Strata.Dialects.Lambda.LExprT
diff --git a/Strata/DL/Lambda/LExprTypeEnv.lean b/Strata/Dialects/Lambda/LExprTypeEnv.lean
similarity index 99%
rename from Strata/DL/Lambda/LExprTypeEnv.lean
rename to Strata/Dialects/Lambda/LExprTypeEnv.lean
index 20aba1226..04de50f5d 100644
--- a/Strata/DL/Lambda/LExprTypeEnv.lean
+++ b/Strata/Dialects/Lambda/LExprTypeEnv.lean
@@ -4,16 +4,16 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprWF
-import Strata.DL.Lambda.LTyUnify
-import Strata.DL.Lambda.Factory
-import Strata.DL.Lambda.TypeFactory
-import Strata.DL.Util.Maps
+import Strata.Dialects.Lambda.LExprWF
+import Strata.Dialects.Lambda.LTyUnify
+import Strata.Dialects.Lambda.Factory
+import Strata.Dialects.Lambda.TypeFactory
+import Strata.Dialects.Util.Maps
 
 /-! ## Type Environment
 
 Data structures and utilities for type inference/checking of Lambda expressions.
-Also see `Strata.DL.Lambda.LExprT`.
+Also see `Strata.Dialects.Lambda.LExprT`.
 -/
 
 ---------------------------------------------------------------------
diff --git a/Strata/DL/Lambda/LExprTypeSpec.lean b/Strata/Dialects/Lambda/LExprTypeSpec.lean
similarity index 98%
rename from Strata/DL/Lambda/LExprTypeSpec.lean
rename to Strata/Dialects/Lambda/LExprTypeSpec.lean
index c48cc2313..55bf3e37c 100644
--- a/Strata/DL/Lambda/LExprTypeSpec.lean
+++ b/Strata/Dialects/Lambda/LExprTypeSpec.lean
@@ -4,12 +4,12 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprTypeEnv
-import Strata.DL.Lambda.LExprWF
+import Strata.Dialects.Lambda.LExprTypeEnv
+import Strata.Dialects.Lambda.LExprWF
 
 /-! ## Typing Relation for Lambda Expressions
 
-Specification of Lambda's type inference. See `Strata.DL.Lambda.LExprT` for the
+Specification of Lambda's type inference. See `Strata.Dialects.Lambda.LExprT` for the
 implementation.
 
 The inductive relation `HasType` characterizes well-typed `LExpr`s. We
diff --git a/Strata/DL/Lambda/LExprWF.lean b/Strata/Dialects/Lambda/LExprWF.lean
similarity index 99%
rename from Strata/DL/Lambda/LExprWF.lean
rename to Strata/Dialects/Lambda/LExprWF.lean
index 0fbedf2cc..e9f4922c9 100644
--- a/Strata/DL/Lambda/LExprWF.lean
+++ b/Strata/Dialects/Lambda/LExprWF.lean
@@ -6,12 +6,12 @@
 
 
 
-import Strata.DL.Lambda.LExpr
+import Strata.Dialects.Lambda.LExpr
 
 /-! ## Well-formedness of Lambda Expressions
 
 See the definition `Lambda.LExpr.WF`. Also see theorem `HasType.regularity` in
-`Strata.DL.Lambda.LExprTypeSpec`.
+`Strata.Dialects.Lambda.LExprTypeSpec`.
 -/
 
 ---------------------------------------------------------------------
diff --git a/Strata/DL/Lambda/LState.lean b/Strata/Dialects/Lambda/LState.lean
similarity index 97%
rename from Strata/DL/Lambda/LState.lean
rename to Strata/Dialects/Lambda/LState.lean
index bae92916b..0d2071358 100644
--- a/Strata/DL/Lambda/LState.lean
+++ b/Strata/Dialects/Lambda/LState.lean
@@ -4,12 +4,12 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.Factory
-import Strata.DL.Lambda.Scopes
+import Strata.Dialects.Lambda.Factory
+import Strata.Dialects.Lambda.Scopes
 
 /-! ## State for (Partial) Evaluation of Lambda Expressions
 
-See `Strata.DL.Lambda.LExprEval` for the partial evaluator.
+See `Strata.Dialects.Lambda.LExprEval` for the partial evaluator.
 -/
 
 namespace Lambda
diff --git a/Strata/DL/Lambda/LTy.lean b/Strata/Dialects/Lambda/LTy.lean
similarity index 99%
rename from Strata/DL/Lambda/LTy.lean
rename to Strata/Dialects/Lambda/LTy.lean
index ea047d6db..0e81a0c01 100644
--- a/Strata/DL/Lambda/LTy.lean
+++ b/Strata/Dialects/Lambda/LTy.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Util.Map
+import Strata.Dialects.Util.Map
 import Lean.Elab.Term
 
 /-! ## Formalization of Mono- and Poly- Types in Lambda
diff --git a/Strata/DL/Lambda/LTyUnify.lean b/Strata/Dialects/Lambda/LTyUnify.lean
similarity index 99%
rename from Strata/DL/Lambda/LTyUnify.lean
rename to Strata/Dialects/Lambda/LTyUnify.lean
index d411dd460..fa1768605 100644
--- a/Strata/DL/Lambda/LTyUnify.lean
+++ b/Strata/Dialects/Lambda/LTyUnify.lean
@@ -4,9 +4,9 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LTy
-import Strata.DL.Util.List
-import Strata.DL.Util.Maps
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.Util.List
+import Strata.Dialects.Util.Maps
 
 /-!
 ## Type Substitution and Unification
diff --git a/Strata/DL/Lambda/Lambda.lean b/Strata/Dialects/Lambda/Lambda.lean
similarity index 74%
rename from Strata/DL/Lambda/Lambda.lean
rename to Strata/Dialects/Lambda/Lambda.lean
index 3821639c7..b3fdac04f 100644
--- a/Strata/DL/Lambda/Lambda.lean
+++ b/Strata/Dialects/Lambda/Lambda.lean
@@ -4,12 +4,12 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprEval
-import Strata.DL.Lambda.LExprType
-import Strata.DL.Lambda.LExpr
-import Strata.DL.Lambda.Semantics
-import Strata.DL.Lambda.TypeFactory
-import Strata.DL.Lambda.Reflect
+import Strata.Dialects.Lambda.LExprEval
+import Strata.Dialects.Lambda.LExprType
+import Strata.Dialects.Lambda.LExpr
+import Strata.Dialects.Lambda.Semantics
+import Strata.Dialects.Lambda.TypeFactory
+import Strata.Dialects.Lambda.Reflect
 
 namespace Lambda
 
@@ -23,10 +23,10 @@ extensible partial evaluator that is parameterized by an (optional) map from
 operator names to their specific evaluations. This allows adding evaluation
 support for new operators without changing the core logic or extending the AST.
 
-See module `Strata.DL.Lambda.LExpr` for the formalization of expressions,
-`Strata.DL.Lambda.LTy` for the formalization of mono- and poly-types,
-`Strata.DL.Lambda.LExprT` for the type inference implementation, and
-`Strata.DL.Lambda.LExprEval` for the partial evaluator.
+See module `Strata.Dialects.Lambda.LExpr` for the formalization of expressions,
+`Strata.Dialects.Lambda.LTy` for the formalization of mono- and poly-types,
+`Strata.Dialects.Lambda.LExprT` for the type inference implementation, and
+`Strata.Dialects.Lambda.LExprEval` for the partial evaluator.
 -/
 
 variable {T: LExprParams} [ToString T.IDMeta] [DecidableEq T.IDMeta] [ToFormat T.IDMeta] [HasGen T.IDMeta] [ToFormat (LFunc T)] [Inhabited (LExpr T.mono)] [BEq T.Metadata] [Traceable LExpr.EvalProvenance T.Metadata]
diff --git a/Strata/DL/Lambda/MetaData.lean b/Strata/Dialects/Lambda/MetaData.lean
similarity index 100%
rename from Strata/DL/Lambda/MetaData.lean
rename to Strata/Dialects/Lambda/MetaData.lean
diff --git a/Strata/DL/Lambda/Reflect.lean b/Strata/Dialects/Lambda/Reflect.lean
similarity index 97%
rename from Strata/DL/Lambda/Reflect.lean
rename to Strata/Dialects/Lambda/Reflect.lean
index c467562f4..a18933672 100644
--- a/Strata/DL/Lambda/Reflect.lean
+++ b/Strata/Dialects/Lambda/Reflect.lean
@@ -4,10 +4,10 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExpr
-import Strata.DL.Lambda.LState
-import Strata.DL.Lambda.LTy
-import Strata.DL.Lambda.LExprTypeEnv
+import Strata.Dialects.Lambda.LExpr
+import Strata.Dialects.Lambda.LState
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.Lambda.LExprTypeEnv
 import Lean.Elab.Term
 import Lean.Meta
 
@@ -172,7 +172,7 @@ info: Lean.Expr.forallE
   `x
   (Lean.Expr.const `Int [])
   (Lean.Expr.forallE
-    (Lean.Name.mkNum (Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkNum `x.«_@».Strata.DL.Lambda.Reflect 1611904336) "_hygCtx") "_hyg") 8)
+    (Lean.Name.mkNum (Lean.Name.mkStr (Lean.Name.mkStr (Lean.Name.mkNum `x.«_@».Strata.Dialects.Lambda.Reflect 1611904336) "_hygCtx") "_hyg") 8)
     (Lean.Expr.const `Int [])
     (Lean.Expr.app
       (Lean.Expr.app
diff --git a/Strata/DL/Lambda/Scopes.lean b/Strata/Dialects/Lambda/Scopes.lean
similarity index 98%
rename from Strata/DL/Lambda/Scopes.lean
rename to Strata/Dialects/Lambda/Scopes.lean
index 91d94f0d6..57621fc51 100644
--- a/Strata/DL/Lambda/Scopes.lean
+++ b/Strata/Dialects/Lambda/Scopes.lean
@@ -6,8 +6,8 @@
 
 
 
-import Strata.DL.Lambda.LExprWF
-import Strata.DL.Util.Maps
+import Strata.Dialects.Lambda.LExprWF
+import Strata.Dialects.Util.Maps
 
 namespace Lambda
 
diff --git a/Strata/DL/Lambda/Semantics.lean b/Strata/Dialects/Lambda/Semantics.lean
similarity index 96%
rename from Strata/DL/Lambda/Semantics.lean
rename to Strata/Dialects/Lambda/Semantics.lean
index 40d18eb7f..fee984255 100644
--- a/Strata/DL/Lambda/Semantics.lean
+++ b/Strata/Dialects/Lambda/Semantics.lean
@@ -4,10 +4,10 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExpr
-import Strata.DL.Lambda.LExprEval
-import Strata.DL.Lambda.LExprWF
-import Strata.DL.Lambda.LState
+import Strata.Dialects.Lambda.LExpr
+import Strata.Dialects.Lambda.LExprEval
+import Strata.Dialects.Lambda.LExprWF
+import Strata.Dialects.Lambda.LState
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/DL/Lambda/TypeFactory.lean b/Strata/Dialects/Lambda/TypeFactory.lean
similarity index 99%
rename from Strata/DL/Lambda/TypeFactory.lean
rename to Strata/Dialects/Lambda/TypeFactory.lean
index a3240a560..38978bdeb 100644
--- a/Strata/DL/Lambda/TypeFactory.lean
+++ b/Strata/Dialects/Lambda/TypeFactory.lean
@@ -4,9 +4,9 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprWF
-import Strata.DL.Lambda.LTy
-import Strata.DL.Lambda.Factory
+import Strata.Dialects.Lambda.LExprWF
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.Lambda.Factory
 
 /-!
 ## Lambda's Type Factory
diff --git a/Strata/DL/SMT/Basic.lean b/Strata/Dialects/SMT/Basic.lean
similarity index 100%
rename from Strata/DL/SMT/Basic.lean
rename to Strata/Dialects/SMT/Basic.lean
diff --git a/Strata/DL/SMT/CexParser.lean b/Strata/Dialects/SMT/CexParser.lean
similarity index 100%
rename from Strata/DL/SMT/CexParser.lean
rename to Strata/Dialects/SMT/CexParser.lean
diff --git a/Strata/DL/SMT/DDMTransform/Parse.lean b/Strata/Dialects/SMT/DDMTransform/Parse.lean
similarity index 100%
rename from Strata/DL/SMT/DDMTransform/Parse.lean
rename to Strata/Dialects/SMT/DDMTransform/Parse.lean
diff --git a/Strata/DL/SMT/Encoder.lean b/Strata/Dialects/SMT/Encoder.lean
similarity index 98%
rename from Strata/DL/SMT/Encoder.lean
rename to Strata/Dialects/SMT/Encoder.lean
index b9937c67e..d4554f838 100644
--- a/Strata/DL/SMT/Encoder.lean
+++ b/Strata/Dialects/SMT/Encoder.lean
@@ -4,11 +4,11 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.SMT.Factory
-import Strata.DL.SMT.Op
-import Strata.DL.SMT.Solver
-import Strata.DL.SMT.Term
-import Strata.DL.SMT.TermType
+import Strata.Dialects.SMT.Factory
+import Strata.Dialects.SMT.Op
+import Strata.Dialects.SMT.Solver
+import Strata.Dialects.SMT.Term
+import Strata.Dialects.SMT.TermType
 import Std.Data.HashMap
 
 /-!
diff --git a/Strata/DL/SMT/Factory.lean b/Strata/Dialects/SMT/Factory.lean
similarity index 98%
rename from Strata/DL/SMT/Factory.lean
rename to Strata/Dialects/SMT/Factory.lean
index fc84d4aea..3106e15dd 100644
--- a/Strata/DL/SMT/Factory.lean
+++ b/Strata/Dialects/SMT/Factory.lean
@@ -4,11 +4,11 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.SMT.Basic
-import Strata.DL.SMT.Function
-import Strata.DL.SMT.Op
-import Strata.DL.SMT.Term
-import Strata.DL.SMT.TermType
+import Strata.Dialects.SMT.Basic
+import Strata.Dialects.SMT.Function
+import Strata.Dialects.SMT.Op
+import Strata.Dialects.SMT.Term
+import Strata.Dialects.SMT.TermType
 
 
 /-!
diff --git a/Strata/DL/SMT/Function.lean b/Strata/Dialects/SMT/Function.lean
similarity index 95%
rename from Strata/DL/SMT/Function.lean
rename to Strata/Dialects/SMT/Function.lean
index da3917f20..cdd5be768 100644
--- a/Strata/DL/SMT/Function.lean
+++ b/Strata/Dialects/SMT/Function.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.SMT.Term
+import Strata.Dialects.SMT.Term
 
 /-!
 Based on Cedar's Term language.
diff --git a/Strata/DL/SMT/Op.lean b/Strata/Dialects/SMT/Op.lean
similarity index 99%
rename from Strata/DL/SMT/Op.lean
rename to Strata/Dialects/SMT/Op.lean
index 2aa4dc19f..8503e5709 100644
--- a/Strata/DL/SMT/Op.lean
+++ b/Strata/Dialects/SMT/Op.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.SMT.TermType
+import Strata.Dialects.SMT.TermType
 import Lean.Elab.Command
 
 /-!
diff --git a/Strata/Dialects/SMT/SMT.lean b/Strata/Dialects/SMT/SMT.lean
new file mode 100644
index 000000000..fca8ff82b
--- /dev/null
+++ b/Strata/Dialects/SMT/SMT.lean
@@ -0,0 +1,15 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Dialects.SMT.Basic
+import Strata.Dialects.SMT.CexParser
+import Strata.Dialects.SMT.Encoder
+import Strata.Dialects.SMT.Factory
+import Strata.Dialects.SMT.Function
+import Strata.Dialects.SMT.Op
+import Strata.Dialects.SMT.Solver
+import Strata.Dialects.SMT.Term
+import Strata.Dialects.SMT.TermType
diff --git a/Strata/DL/SMT/Solver.lean b/Strata/Dialects/SMT/Solver.lean
similarity index 100%
rename from Strata/DL/SMT/Solver.lean
rename to Strata/Dialects/SMT/Solver.lean
diff --git a/Strata/DL/SMT/Term.lean b/Strata/Dialects/SMT/Term.lean
similarity index 98%
rename from Strata/DL/SMT/Term.lean
rename to Strata/Dialects/SMT/Term.lean
index 96203e77d..b8bc44b9c 100644
--- a/Strata/DL/SMT/Term.lean
+++ b/Strata/Dialects/SMT/Term.lean
@@ -4,9 +4,9 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.SMT.TermType
-import Strata.DL.SMT.Basic
-import Strata.DL.SMT.Op
+import Strata.Dialects.SMT.TermType
+import Strata.Dialects.SMT.Basic
+import Strata.Dialects.SMT.Op
 
 /-!
 Based on Cedar's Term language.
diff --git a/Strata/DL/SMT/TermType.lean b/Strata/Dialects/SMT/TermType.lean
similarity index 100%
rename from Strata/DL/SMT/TermType.lean
rename to Strata/Dialects/SMT/TermType.lean
diff --git a/Strata/DL/Util/Counter.lean b/Strata/Dialects/Util/Counter.lean
similarity index 100%
rename from Strata/DL/Util/Counter.lean
rename to Strata/Dialects/Util/Counter.lean
diff --git a/Strata/DL/Util/DecidableEq.lean b/Strata/Dialects/Util/DecidableEq.lean
similarity index 100%
rename from Strata/DL/Util/DecidableEq.lean
rename to Strata/Dialects/Util/DecidableEq.lean
diff --git a/Strata/DL/Util/LabelGen.lean b/Strata/Dialects/Util/LabelGen.lean
similarity index 96%
rename from Strata/DL/Util/LabelGen.lean
rename to Strata/Dialects/Util/LabelGen.lean
index 17b38b115..da153b596 100644
--- a/Strata/DL/Util/LabelGen.lean
+++ b/Strata/Dialects/Util/LabelGen.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Util.Counter
-import Strata.DL.Util.StringGen
+import Strata.Dialects.Util.Counter
+import Strata.Dialects.Util.StringGen
 namespace LabelGen
 
 /-! ## Well-Formed Label Generator -/
diff --git a/Strata/DL/Util/List.lean b/Strata/Dialects/Util/List.lean
similarity index 100%
rename from Strata/DL/Util/List.lean
rename to Strata/Dialects/Util/List.lean
diff --git a/Strata/DL/Util/ListMap.lean b/Strata/Dialects/Util/ListMap.lean
similarity index 100%
rename from Strata/DL/Util/ListMap.lean
rename to Strata/Dialects/Util/ListMap.lean
diff --git a/Strata/DL/Util/ListUtils.lean b/Strata/Dialects/Util/ListUtils.lean
similarity index 100%
rename from Strata/DL/Util/ListUtils.lean
rename to Strata/Dialects/Util/ListUtils.lean
diff --git a/Strata/DL/Util/Map.lean b/Strata/Dialects/Util/Map.lean
similarity index 100%
rename from Strata/DL/Util/Map.lean
rename to Strata/Dialects/Util/Map.lean
diff --git a/Strata/DL/Util/Maps.lean b/Strata/Dialects/Util/Maps.lean
similarity index 99%
rename from Strata/DL/Util/Maps.lean
rename to Strata/Dialects/Util/Maps.lean
index 8d95e6afa..5c0bd1b29 100644
--- a/Strata/DL/Util/Maps.lean
+++ b/Strata/Dialects/Util/Maps.lean
@@ -5,7 +5,7 @@
 -/
 
 
-import Strata.DL.Util.Map
+import Strata.Dialects.Util.Map
 
 open Std (ToFormat Format format)
 
diff --git a/Strata/DL/Util/Nodup.lean b/Strata/Dialects/Util/Nodup.lean
similarity index 100%
rename from Strata/DL/Util/Nodup.lean
rename to Strata/Dialects/Util/Nodup.lean
diff --git a/Strata/DL/Util/StringGen.lean b/Strata/Dialects/Util/StringGen.lean
similarity index 99%
rename from Strata/DL/Util/StringGen.lean
rename to Strata/Dialects/Util/StringGen.lean
index 2f11f1b64..62597ee5e 100644
--- a/Strata/DL/Util/StringGen.lean
+++ b/Strata/Dialects/Util/StringGen.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Util.Counter
+import Strata.Dialects.Util.Counter
 
 /-! ## String Generator
   This file contains a string generator `StringGenState.gen`, where the
diff --git a/Strata/Languages/Boogie/Axiom.lean b/Strata/Languages/Boogie/Axiom.lean
index ea113002b..0d6e0a719 100644
--- a/Strata/Languages/Boogie/Axiom.lean
+++ b/Strata/Languages/Boogie/Axiom.lean
@@ -8,8 +8,8 @@
 
 
 import Strata.Languages.Boogie.Statement
-import Strata.DL.Lambda.LTy
-import Strata.DL.Lambda.LExpr
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.Lambda.LExpr
 
 namespace Boogie
 ---------------------------------------------------------------------
diff --git a/Strata/Languages/Boogie/BoogieGen.lean b/Strata/Languages/Boogie/BoogieGen.lean
index 58f845b91..615105bd1 100644
--- a/Strata/Languages/Boogie/BoogieGen.lean
+++ b/Strata/Languages/Boogie/BoogieGen.lean
@@ -5,9 +5,9 @@
 -/
 
 import Strata.Languages.Boogie.Statement
-import Strata.DL.Util.LabelGen
-import Strata.DL.Util.StringGen
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Util.LabelGen
+import Strata.Dialects.Util.StringGen
+import Strata.Dialects.Util.ListUtils
 open Boogie Lambda Imperative
 
 /-! ## Boogie Identifier Generator
diff --git a/Strata/Languages/Boogie/CmdEval.lean b/Strata/Languages/Boogie/CmdEval.lean
index d5fb1d410..240199ec4 100644
--- a/Strata/Languages/Boogie/CmdEval.lean
+++ b/Strata/Languages/Boogie/CmdEval.lean
@@ -9,8 +9,8 @@
 import Strata.Languages.Boogie.OldExpressions
 import Strata.Languages.Boogie.Expressions
 import Strata.Languages.Boogie.Env
-import Strata.DL.Imperative.EvalContext
-import Strata.DL.Imperative.CmdEval
+import Strata.Dialects.Imperative.EvalContext
+import Strata.Dialects.Imperative.CmdEval
 
 namespace Boogie
 open Lambda Imperative
diff --git a/Strata/Languages/Boogie/CmdType.lean b/Strata/Languages/Boogie/CmdType.lean
index 83abc2a89..fcc11d59b 100644
--- a/Strata/Languages/Boogie/CmdType.lean
+++ b/Strata/Languages/Boogie/CmdType.lean
@@ -8,8 +8,8 @@
 
 import Strata.Languages.Boogie.OldExpressions
 import Strata.Languages.Boogie.Expressions
-import Strata.DL.Imperative.TypeContext
-import Strata.DL.Lambda.Factory
+import Strata.Dialects.Imperative.TypeContext
+import Strata.Dialects.Lambda.Factory
 
 namespace Boogie
 open Lambda Imperative
diff --git a/Strata/Languages/Boogie/Env.lean b/Strata/Languages/Boogie/Env.lean
index 75f972886..7614dff76 100644
--- a/Strata/Languages/Boogie/Env.lean
+++ b/Strata/Languages/Boogie/Env.lean
@@ -7,7 +7,7 @@
 
 
 import Strata.Languages.Boogie.Program
-import Strata.DL.Imperative.EvalContext
+import Strata.Dialects.Imperative.EvalContext
 
 namespace Boogie
 open Std (ToFormat Format format)
diff --git a/Strata/Languages/Boogie/Expressions.lean b/Strata/Languages/Boogie/Expressions.lean
index b11fa1b73..6dada6ac3 100644
--- a/Strata/Languages/Boogie/Expressions.lean
+++ b/Strata/Languages/Boogie/Expressions.lean
@@ -6,10 +6,10 @@
 
 
 
-import Strata.DL.Lambda.Lambda
-import Strata.DL.Imperative.PureExpr
+import Strata.Dialects.Lambda.Lambda
+import Strata.Dialects.Imperative.PureExpr
 import Strata.Languages.Boogie.Identifiers
-import Strata.DL.Imperative.HasVars
+import Strata.Dialects.Imperative.HasVars
 
 namespace Boogie
 open Std (ToFormat Format format)
diff --git a/Strata/Languages/Boogie/Factory.lean b/Strata/Languages/Boogie/Factory.lean
index 13331eec1..f1a01e22d 100644
--- a/Strata/Languages/Boogie/Factory.lean
+++ b/Strata/Languages/Boogie/Factory.lean
@@ -7,8 +7,8 @@ import Lean.Elab.Command
 
 import Strata.Languages.Boogie.Identifiers
 import Strata.Languages.Boogie.Expressions
-import Strata.DL.Lambda.Factory
-import Strata.DL.Lambda.IntBoolFactory
+import Strata.Dialects.Lambda.Factory
+import Strata.Dialects.Lambda.IntBoolFactory
 ---------------------------------------------------------------------
 
 namespace Boogie
diff --git a/Strata/Languages/Boogie/Identifiers.lean b/Strata/Languages/Boogie/Identifiers.lean
index ec84c4ffe..e62b9ac72 100644
--- a/Strata/Languages/Boogie/Identifiers.lean
+++ b/Strata/Languages/Boogie/Identifiers.lean
@@ -6,8 +6,8 @@
 
 
 
-import Strata.DL.Lambda.LExprTypeEnv
-import Strata.DL.Lambda.Factory
+import Strata.Dialects.Lambda.LExprTypeEnv
+import Strata.Dialects.Lambda.Factory
 namespace Boogie
 
 open Std
diff --git a/Strata/Languages/Boogie/Procedure.lean b/Strata/Languages/Boogie/Procedure.lean
index edfaf804a..facee6d15 100644
--- a/Strata/Languages/Boogie/Procedure.lean
+++ b/Strata/Languages/Boogie/Procedure.lean
@@ -6,7 +6,7 @@
 
 
 
-import Strata.DL.Imperative.HasVars
+import Strata.Dialects.Imperative.HasVars
 import Strata.Languages.Boogie.Statement
 
 ---------------------------------------------------------------------
diff --git a/Strata/Languages/Boogie/ProcedureType.lean b/Strata/Languages/Boogie/ProcedureType.lean
index 8c52d91a3..5653d1136 100644
--- a/Strata/Languages/Boogie/ProcedureType.lean
+++ b/Strata/Languages/Boogie/ProcedureType.lean
@@ -7,7 +7,7 @@
 
 
 import Strata.Languages.Boogie.Procedure
-import Strata.DL.Imperative.HasVars
+import Strata.Dialects.Imperative.HasVars
 import Strata.Languages.Boogie.StatementType
 import Strata.Languages.Boogie.OldExpressions
 
diff --git a/Strata/Languages/Boogie/ProcedureWF.lean b/Strata/Languages/Boogie/ProcedureWF.lean
index 1df073e9c..c1cffcfa1 100644
--- a/Strata/Languages/Boogie/ProcedureWF.lean
+++ b/Strata/Languages/Boogie/ProcedureWF.lean
@@ -6,7 +6,7 @@
 
 
 
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Util.ListUtils
 import Strata.Languages.Boogie.Program
 import Strata.Languages.Boogie.ProcedureType
 import Strata.Languages.Boogie.WF
diff --git a/Strata/Languages/Boogie/ProgramType.lean b/Strata/Languages/Boogie/ProgramType.lean
index 29908ac0e..99cddcc9e 100644
--- a/Strata/Languages/Boogie/ProgramType.lean
+++ b/Strata/Languages/Boogie/ProgramType.lean
@@ -6,7 +6,7 @@
 
 
 
-import Strata.DL.Lambda.LExprType
+import Strata.Dialects.Lambda.LExprType
 import Strata.Languages.Boogie.Program
 import Strata.Languages.Boogie.FunctionType
 import Strata.Languages.Boogie.ProcedureType
diff --git a/Strata/Languages/Boogie/ProgramWF.lean b/Strata/Languages/Boogie/ProgramWF.lean
index 65f1a4176..18d220365 100644
--- a/Strata/Languages/Boogie/ProgramWF.lean
+++ b/Strata/Languages/Boogie/ProgramWF.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Util.ListUtils
 import Strata.Languages.Boogie.ProgramType
 import Strata.Languages.Boogie.WF
 import Strata.Languages.Boogie.StatementWF
diff --git a/Strata/Languages/Boogie/SMTEncoder.lean b/Strata/Languages/Boogie/SMTEncoder.lean
index 5cebe218b..de69e9e86 100644
--- a/Strata/Languages/Boogie/SMTEncoder.lean
+++ b/Strata/Languages/Boogie/SMTEncoder.lean
@@ -7,7 +7,7 @@
 
 
 import Strata.Languages.Boogie.Boogie
-import Strata.DL.SMT.SMT
+import Strata.Dialects.SMT.SMT
 import Init.Data.String.Extra
 import Strata.DDM.Util.DecimalRat
 
diff --git a/Strata/Languages/Boogie/Statement.lean b/Strata/Languages/Boogie/Statement.lean
index 21da02779..94a74a557 100644
--- a/Strata/Languages/Boogie/Statement.lean
+++ b/Strata/Languages/Boogie/Statement.lean
@@ -7,12 +7,12 @@
 
 
 import Strata.Languages.Boogie.Expressions
-import Strata.DL.Imperative.PureExpr
+import Strata.Dialects.Imperative.PureExpr
 import Strata.Languages.Boogie.Identifiers
 import Strata.Languages.Boogie.Factory
-import Strata.DL.Imperative.Stmt
-import Strata.DL.Imperative.HasVars
-import Strata.DL.Lambda.LExpr
+import Strata.Dialects.Imperative.Stmt
+import Strata.Dialects.Imperative.HasVars
+import Strata.Dialects.Lambda.LExpr
 
 namespace Boogie
 open Imperative
diff --git a/Strata/Languages/Boogie/StatementSemantics.lean b/Strata/Languages/Boogie/StatementSemantics.lean
index 49f6d4855..ab1f4f9cd 100644
--- a/Strata/Languages/Boogie/StatementSemantics.lean
+++ b/Strata/Languages/Boogie/StatementSemantics.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExpr
-import Strata.DL.Imperative.StmtSemantics
+import Strata.Dialects.Lambda.LExpr
+import Strata.Dialects.Imperative.StmtSemantics
 import Strata.Languages.Boogie.OldExpressions
 
 ---------------------------------------------------------------------
diff --git a/Strata/Languages/Boogie/StatementSemanticsProps.lean b/Strata/Languages/Boogie/StatementSemanticsProps.lean
index a678913b3..4d8c151e7 100644
--- a/Strata/Languages/Boogie/StatementSemanticsProps.lean
+++ b/Strata/Languages/Boogie/StatementSemanticsProps.lean
@@ -4,11 +4,11 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.CmdSemantics
-import Strata.DL.Imperative.StmtSemantics
-import Strata.DL.Imperative.HasVars
-import Strata.DL.Util.Nodup
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Imperative.CmdSemantics
+import Strata.Dialects.Imperative.StmtSemantics
+import Strata.Dialects.Imperative.HasVars
+import Strata.Dialects.Util.Nodup
+import Strata.Dialects.Util.ListUtils
 import Strata.Languages.Boogie.Procedure
 import Strata.Languages.Boogie.Statement
 import Strata.Languages.Boogie.OldExpressions
diff --git a/Strata/Languages/Boogie/StatementType.lean b/Strata/Languages/Boogie/StatementType.lean
index 5a6c0bf37..f2ade2baa 100644
--- a/Strata/Languages/Boogie/StatementType.lean
+++ b/Strata/Languages/Boogie/StatementType.lean
@@ -10,7 +10,7 @@ import Strata.Languages.Boogie.Statement
 import Strata.Languages.Boogie.CmdType
 import Strata.Languages.Boogie.Program
 import Strata.Languages.Boogie.OldExpressions
-import Strata.DL.Imperative.CmdType
+import Strata.Dialects.Imperative.CmdType
 
 namespace Boogie
 namespace Statement
diff --git a/Strata/Languages/Boogie/StatementWF.lean b/Strata/Languages/Boogie/StatementWF.lean
index d0a3cc36f..acad49bab 100644
--- a/Strata/Languages/Boogie/StatementWF.lean
+++ b/Strata/Languages/Boogie/StatementWF.lean
@@ -6,7 +6,7 @@
 
 
 
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Util.ListUtils
 import Strata.Languages.Boogie.Program
 import Strata.Languages.Boogie.WF
 import Strata.Languages.Boogie.StatementType
diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean
index ed39c6d1c..91586c2df 100644
--- a/Strata/Languages/Boogie/Verifier.lean
+++ b/Strata/Languages/Boogie/Verifier.lean
@@ -8,9 +8,9 @@ import Strata.Languages.Boogie.DDMTransform.Translate
 import Strata.Languages.Boogie.Options
 import Strata.Languages.Boogie.CallGraph
 import Strata.Languages.Boogie.SMTEncoder
-import Strata.DL.Imperative.MetaData
-import Strata.DL.Imperative.SMTUtils
-import Strata.DL.SMT.CexParser
+import Strata.Dialects.Imperative.MetaData
+import Strata.Dialects.Imperative.SMTUtils
+import Strata.Dialects.SMT.CexParser
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/Languages/Boogie/WF.lean b/Strata/Languages/Boogie/WF.lean
index e79c6f445..bb542d622 100644
--- a/Strata/Languages/Boogie/WF.lean
+++ b/Strata/Languages/Boogie/WF.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Util.ListUtils
 import Strata.Languages.Boogie.Program
 import Strata.Languages.Boogie.OldExpressions
 
diff --git a/Strata/Languages/C_Simp/C_Simp.lean b/Strata/Languages/C_Simp/C_Simp.lean
index e27c14828..351f63e43 100644
--- a/Strata/Languages/C_Simp/C_Simp.lean
+++ b/Strata/Languages/C_Simp/C_Simp.lean
@@ -5,11 +5,11 @@
 -/
 
 import Strata.Languages.C_Simp.DDMTransform.Parse
-import Strata.DL.Imperative.Stmt
-import Strata.DL.Lambda.Lambda
-import Strata.DL.Lambda.LExpr
-import Strata.DL.Lambda.LTy
-import Strata.DL.Lambda.Identifiers
+import Strata.Dialects.Imperative.Stmt
+import Strata.Dialects.Lambda.Lambda
+import Strata.Dialects.Lambda.LExpr
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.Lambda.Identifiers
 
 -- We define the AST for our language here.
 
diff --git a/Strata/Languages/C_Simp/StrataToCBMC.lean b/Strata/Languages/C_Simp/StrataToCBMC.lean
index ba3cafab7..631c64387 100644
--- a/Strata/Languages/C_Simp/StrataToCBMC.lean
+++ b/Strata/Languages/C_Simp/StrataToCBMC.lean
@@ -5,7 +5,7 @@
 -/
 
 import Strata.Backends.CBMC.Common
-import Strata.DL.Util.Map
+import Strata.Dialects.Util.Map
 import Strata.Languages.C_Simp.C_Simp
 import Strata.Languages.C_Simp.Verify
 
diff --git a/Strata/Languages/C_Simp/Verify.lean b/Strata/Languages/C_Simp/Verify.lean
index 901c5be83..57396fb3c 100644
--- a/Strata/Languages/C_Simp/Verify.lean
+++ b/Strata/Languages/C_Simp/Verify.lean
@@ -7,7 +7,7 @@
 import Strata.Languages.C_Simp.C_Simp
 import Strata.Languages.C_Simp.DDMTransform.Translate
 import Strata.Languages.Boogie.Verifier
-import Strata.DL.Imperative.Stmt
+import Strata.Dialects.Imperative.Stmt
 
 namespace Strata
 
diff --git a/Strata/Languages/Laurel/LaurelEval.lean b/Strata/Languages/Laurel/LaurelEval.lean
index fd81fc67d..6adfdb001 100644
--- a/Strata/Languages/Laurel/LaurelEval.lean
+++ b/Strata/Languages/Laurel/LaurelEval.lean
@@ -10,7 +10,7 @@ Both are defined using the 'eval' function. It will only return a single type or
 
 TODO: implicit casting from primitives types to Dynamic
 -/
-import Strata.DL.HighStrata.HighStrata
+import Strata.Dialects.HighStrata.HighStrata
 import Std.Data.HashMap.Basic
 import Lean.Data.AssocList
 
diff --git a/Strata/Transform/BoogieTransform.lean b/Strata/Transform/BoogieTransform.lean
index 1ecb9698e..79425d16b 100644
--- a/Strata/Transform/BoogieTransform.lean
+++ b/Strata/Transform/BoogieTransform.lean
@@ -7,7 +7,7 @@
 import Strata.Languages.Boogie.Statement
 import Strata.Languages.Boogie.Boogie
 import Strata.Languages.Boogie.BoogieGen
-import Strata.DL.Util.LabelGen
+import Strata.Dialects.Util.LabelGen
 
 /-! # Utility functions for program transformation in Boogie -/
 
diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean
index 5a0c4c3b2..fab6adc77 100644
--- a/Strata/Transform/CallElimCorrect.lean
+++ b/Strata/Transform/CallElimCorrect.lean
@@ -11,13 +11,13 @@ import Strata.Languages.Boogie.Identifiers
 import Strata.Languages.Boogie.Program
 import Strata.Languages.Boogie.ProgramType
 import Strata.Languages.Boogie.WF
-import Strata.DL.Lambda.Lambda
+import Strata.Dialects.Lambda.Lambda
 import Strata.Transform.BoogieTransform
 import Strata.Transform.CallElim
-import Strata.DL.Imperative.CmdSemantics
+import Strata.Dialects.Imperative.CmdSemantics
 import Strata.Languages.Boogie.StatementSemantics
 import Strata.Languages.Boogie.StatementSemanticsProps
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Util.ListUtils
 
 /-! # Call Elimination Correctness Proof
 
diff --git a/Strata/Transform/DetToNondet.lean b/Strata/Transform/DetToNondet.lean
index 712093d66..c460e2bd1 100644
--- a/Strata/Transform/DetToNondet.lean
+++ b/Strata/Transform/DetToNondet.lean
@@ -4,9 +4,9 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.Cmd
-import Strata.DL.Imperative.Stmt
-import Strata.DL.Imperative.NondetStmt
+import Strata.Dialects.Imperative.Cmd
+import Strata.Dialects.Imperative.Stmt
+import Strata.Dialects.Imperative.NondetStmt
 import Strata.Languages.Boogie.StatementType
 
 /-! # Deterministic-to-Nondeterministic Transformation -/
diff --git a/Strata/Transform/DetToNondetCorrect.lean b/Strata/Transform/DetToNondetCorrect.lean
index eaec65d73..4b05cc14c 100644
--- a/Strata/Transform/DetToNondetCorrect.lean
+++ b/Strata/Transform/DetToNondetCorrect.lean
@@ -4,10 +4,10 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.Stmt
-import Strata.DL.Imperative.StmtSemantics
-import Strata.DL.Imperative.NondetStmt
-import Strata.DL.Imperative.NondetStmtSemantics
+import Strata.Dialects.Imperative.Stmt
+import Strata.Dialects.Imperative.StmtSemantics
+import Strata.Dialects.Imperative.NondetStmt
+import Strata.Dialects.Imperative.NondetStmtSemantics
 import Strata.Transform.DetToNondet
 
 /-! # Deterministic-to-Nondeterministic Transformation Correctness Proof
diff --git a/Strata/Transform/LoopElim.lean b/Strata/Transform/LoopElim.lean
index 85909d1d1..6e91c9021 100644
--- a/Strata/Transform/LoopElim.lean
+++ b/Strata/Transform/LoopElim.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.Stmt
+import Strata.Dialects.Imperative.Stmt
 
 namespace Boogie
 open Imperative Lambda
diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean
index f9038b34e..c3645f22b 100644
--- a/Strata/Transform/ProcedureInlining.lean
+++ b/Strata/Transform/ProcedureInlining.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Util.LabelGen
-import Strata.DL.Util.ListUtils
+import Strata.Dialects.Util.LabelGen
+import Strata.Dialects.Util.ListUtils
 import Strata.Languages.Boogie.Boogie
 import Strata.Languages.Boogie.BoogieGen
 import Strata.Languages.Boogie.ProgramWF
diff --git a/StrataTest/Backends/CBMC/LambdaToCProverGOTO.lean b/StrataTest/Backends/CBMC/LambdaToCProverGOTO.lean
index e23446a65..8dac6bd32 100644
--- a/StrataTest/Backends/CBMC/LambdaToCProverGOTO.lean
+++ b/StrataTest/Backends/CBMC/LambdaToCProverGOTO.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.Lambda
+import Strata.Dialects.Lambda.Lambda
 import Strata.Backends.CBMC.GOTO.Expr
 
 namespace Lambda
diff --git a/StrataTest/Backends/CBMC/ToCProverGOTO.lean b/StrataTest/Backends/CBMC/ToCProverGOTO.lean
index 4ba14958f..12cc3cc89 100644
--- a/StrataTest/Backends/CBMC/ToCProverGOTO.lean
+++ b/StrataTest/Backends/CBMC/ToCProverGOTO.lean
@@ -5,7 +5,7 @@
 -/
 
 import StrataTest.Backends.CBMC.LambdaToCProverGOTO
-import Strata.DL.Imperative.ToCProverGOTO
+import Strata.Dialects.Imperative.ToCProverGOTO
 
 -------------------------------------------------------------------------------
 
diff --git a/StrataTest/DL/Imperative/ArithEval.lean b/StrataTest/DL/Imperative/ArithEval.lean
index f9ee3f0f6..d5367e1c9 100644
--- a/StrataTest/DL/Imperative/ArithEval.lean
+++ b/StrataTest/DL/Imperative/ArithEval.lean
@@ -7,7 +7,7 @@
 
 
 import StrataTest.DL.Imperative.ArithExpr
-import Strata.DL.Imperative.CmdEval
+import Strata.Dialects.Imperative.CmdEval
 
 namespace Arith
 
diff --git a/StrataTest/DL/Imperative/ArithExpr.lean b/StrataTest/DL/Imperative/ArithExpr.lean
index 8c98cda42..17504bfa6 100644
--- a/StrataTest/DL/Imperative/ArithExpr.lean
+++ b/StrataTest/DL/Imperative/ArithExpr.lean
@@ -4,9 +4,9 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.Cmd
-import Strata.DL.Imperative.EvalError
-import Strata.DL.Util.Maps
+import Strata.Dialects.Imperative.Cmd
+import Strata.Dialects.Imperative.EvalError
+import Strata.Dialects.Util.Maps
 
 namespace Arith
 open Std (ToFormat Format format)
diff --git a/StrataTest/DL/Imperative/ArithType.lean b/StrataTest/DL/Imperative/ArithType.lean
index 7826e2091..40f3de812 100644
--- a/StrataTest/DL/Imperative/ArithType.lean
+++ b/StrataTest/DL/Imperative/ArithType.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Imperative.CmdType
+import Strata.Dialects.Imperative.CmdType
 import StrataTest.DL.Imperative.ArithExpr
 
 namespace Arith
diff --git a/StrataTest/DL/Imperative/SMTEncoder.lean b/StrataTest/DL/Imperative/SMTEncoder.lean
index de003b164..4bc038dba 100644
--- a/StrataTest/DL/Imperative/SMTEncoder.lean
+++ b/StrataTest/DL/Imperative/SMTEncoder.lean
@@ -5,8 +5,8 @@
 -/
 
 import StrataTest.DL.Imperative.Arith
-import Strata.DL.Imperative.EvalContext
-import Strata.DL.SMT.SMT
+import Strata.Dialects.Imperative.EvalContext
+import Strata.Dialects.SMT.SMT
 import Init.Data.String.Extra
 
 namespace Arith
diff --git a/StrataTest/DL/Imperative/Verify.lean b/StrataTest/DL/Imperative/Verify.lean
index c5cf224b9..3e7493e61 100644
--- a/StrataTest/DL/Imperative/Verify.lean
+++ b/StrataTest/DL/Imperative/Verify.lean
@@ -6,7 +6,7 @@
 
 import StrataTest.DL.Imperative.DDMTranslate
 import StrataTest.DL.Imperative.SMTEncoder
-import Strata.DL.Imperative.SMTUtils
+import Strata.Dialects.Imperative.SMTUtils
 
 ---------------------------------------------------------------------
 namespace Arith
diff --git a/StrataTest/DL/Lambda/LExprEvalTests.lean b/StrataTest/DL/Lambda/LExprEvalTests.lean
index ddfeccee8..2adb1020a 100644
--- a/StrataTest/DL/Lambda/LExprEvalTests.lean
+++ b/StrataTest/DL/Lambda/LExprEvalTests.lean
@@ -4,8 +4,8 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.Semantics
-import Strata.DL.Lambda.LExprEval
+import Strata.Dialects.Lambda.Semantics
+import Strata.Dialects.Lambda.LExprEval
 
 ---------------------------------------------------------------------
 
diff --git a/StrataTest/DL/Lambda/LExprTTests.lean b/StrataTest/DL/Lambda/LExprTTests.lean
index 6b89f7774..39178c953 100644
--- a/StrataTest/DL/Lambda/LExprTTests.lean
+++ b/StrataTest/DL/Lambda/LExprTTests.lean
@@ -4,7 +4,7 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.LExprT
+import Strata.Dialects.Lambda.LExprT
 
 namespace Lambda
 ---------------------------------------------------------------------
diff --git a/StrataTest/DL/Lambda/Lambda.lean b/StrataTest/DL/Lambda/Lambda.lean
index 5ae49e4ff..aad1e3048 100644
--- a/StrataTest/DL/Lambda/Lambda.lean
+++ b/StrataTest/DL/Lambda/Lambda.lean
@@ -6,8 +6,8 @@
 
 
 
-import Strata.DL.Lambda.Lambda
-import Strata.DL.Lambda.IntBoolFactory
+import Strata.Dialects.Lambda.Lambda
+import Strata.Dialects.Lambda.IntBoolFactory
 
 ---------------------------------------------------------------------
 
diff --git a/StrataTest/DL/Lambda/TypeFactoryTests.lean b/StrataTest/DL/Lambda/TypeFactoryTests.lean
index ed16511dd..b9d97adec 100644
--- a/StrataTest/DL/Lambda/TypeFactoryTests.lean
+++ b/StrataTest/DL/Lambda/TypeFactoryTests.lean
@@ -6,9 +6,9 @@
 
 
 
-import Strata.DL.Lambda.Lambda
-import Strata.DL.Lambda.IntBoolFactory
-import Strata.DL.Lambda.TypeFactory
+import Strata.Dialects.Lambda.Lambda
+import Strata.Dialects.Lambda.IntBoolFactory
+import Strata.Dialects.Lambda.TypeFactory
 
 ---------------------------------------------------------------------
 
diff --git a/StrataTest/Languages/Boogie/ExprEvalTest.lean b/StrataTest/Languages/Boogie/ExprEvalTest.lean
index 4d00d82d3..c1616b53d 100644
--- a/StrataTest/Languages/Boogie/ExprEvalTest.lean
+++ b/StrataTest/Languages/Boogie/ExprEvalTest.lean
@@ -4,12 +4,12 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.DL.Lambda.Lambda
-import Strata.DL.Lambda.LExpr
-import Strata.DL.Lambda.LState
-import Strata.DL.Lambda.LTy
-import Strata.DL.SMT.Term
-import Strata.DL.SMT.Encoder
+import Strata.Dialects.Lambda.Lambda
+import Strata.Dialects.Lambda.LExpr
+import Strata.Dialects.Lambda.LState
+import Strata.Dialects.Lambda.LTy
+import Strata.Dialects.SMT.Term
+import Strata.Dialects.SMT.Encoder
 import Strata.Languages.Boogie.Env
 import Strata.Languages.Boogie.Factory
 import Strata.Languages.Boogie.Identifiers
diff --git a/StrataTest/Transform/DetToNondet.lean b/StrataTest/Transform/DetToNondet.lean
index b3aa28597..46a8d7805 100644
--- a/StrataTest/Transform/DetToNondet.lean
+++ b/StrataTest/Transform/DetToNondet.lean
@@ -8,7 +8,7 @@ import Strata.Transform.DetToNondet
 import Strata.Languages.Boogie.StatementSemantics
 import Strata.Languages.Boogie.ProgramType
 import Strata.Languages.Boogie.ProgramWF
-import Strata.DL.Lambda.IntBoolFactory
+import Strata.Dialects.Lambda.IntBoolFactory
 
 open Boogie
 
diff --git a/docs/Architecture.md b/docs/Architecture.md
index 0cac5e463..a72fcd872 100644
--- a/docs/Architecture.md
+++ b/docs/Architecture.md
@@ -30,15 +30,15 @@ Transformations (located in [`Strata.Transform`](../Strata/Transform/)) are a ce
 
 ## Dialect Library
 
-Strata includes several generic dialects that allow it to represent the semantics of a variety of common programming languages. These dialects are currently sufficient to represent the constructs available in Boogie, and allow some flexibility beyond what Boogie provides, as well. These dialects are located in the [`Strata.DL`](../Strata/DL/) namespace.
+Strata includes several generic dialects that allow it to represent the semantics of a variety of common programming languages. These dialects are currently sufficient to represent the constructs available in Boogie, and allow some flexibility beyond what Boogie provides, as well. These dialects are located in the [`Strata.Dialects`](../Strata/DL/) namespace.
 
 ### Lambda
 
-The `Lambda` dialect ([`Strata.DL.Lambda`](../Strata/DL/Lambda/)) is intended to represent pure expressions of the sort that appear in essentially every programming or specification language. This dialect is parameterized by a set of built-in functions, allowing many first-order and higher-order expression languages as specific instantiations.
+The `Lambda` dialect ([`Strata.Dialects.Lambda`](../Strata/DL/Lambda/)) is intended to represent pure expressions of the sort that appear in essentially every programming or specification language. This dialect is parameterized by a set of built-in functions, allowing many first-order and higher-order expression languages as specific instantiations.
 
 ### Imperative
 
-The `Imperative` dialect ([`Strata.DL.Imperative`](../Strata/DL/Imperative/)) is intended to represent imperative statements of the sort that appear in many programming languages. It is built of commands, which execute atomically, and currently has two mechanisms for combining commands:
+The `Imperative` dialect ([`Strata.Dialects.Imperative`](../Strata/DL/Imperative/)) is intended to represent imperative statements of the sort that appear in many programming languages. It is built of commands, which execute atomically, and currently has two mechanisms for combining commands:
 
 * deterministic structured statements (if and while statements with explicit conditions), 
 * non-deterministic structured statements (choice and repetition, with conditions encoded using assumptions), 
@@ -80,7 +80,7 @@ The current Strata implementation includes only one analysis: the Boogie dialect
 
 ## External Reasoning Tools
 
-Strata was designed to be used with external reasoning tools such as SMT solvers, CHC solvers, abstract interpretation engines, model checkers, and others. Currently, the VCG for the Boogie language based on partial evaluation along with an interface to SMT solvers (in [`Strata.DL.SMT`](../Strata/DL/SMT/)).
+Strata was designed to be used with external reasoning tools such as SMT solvers, CHC solvers, abstract interpretation engines, model checkers, and others. Currently, the VCG for the Boogie language based on partial evaluation along with an interface to SMT solvers (in [`Strata.Dialects.SMT`](../Strata/DL/SMT/)).
 
 ## Third-Party Dialects and Analyses