diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,10 @@
+2022-09-07
+        * Version bump (3.11). (#376)
+        * Deprecate Copilot.Core.PrettyDot. (#359)
+        * Remove Copilot.Core.Type.Dynamic. (#360)
+        * Split copilot-interpreter into separate library. (#361)
+        * Deprecate unused classes, functions from Array module. (#369)
+
 2022-07-07
         * Version bump (3.10). (#356)
         * Fix error in test case generation; enable CLI args in tests. (#337)
diff --git a/copilot-core.cabal b/copilot-core.cabal
--- a/copilot-core.cabal
+++ b/copilot-core.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-core
-version:             3.10
+version:             3.11
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
@@ -57,7 +57,6 @@
     Copilot.Core.Spec
     Copilot.Core.Type
     Copilot.Core.Type.Array
-    Copilot.Core.Type.Dynamic
     Copilot.Core.Type.Equality
     Copilot.Core.Type.Show
     Copilot.Core.PrettyPrint
@@ -82,7 +81,6 @@
     Test.Copilot.Core.Interpret.Eval
     Test.Copilot.Core.Type
     Test.Copilot.Core.Type.Array
-    Test.Copilot.Core.Type.Dynamic
     Test.Copilot.Core.Type.Show
 
   build-depends:
diff --git a/src/Copilot/Core/Interpret.hs b/src/Copilot/Core/Interpret.hs
--- a/src/Copilot/Core/Interpret.hs
+++ b/src/Copilot/Core/Interpret.hs
@@ -1,3 +1,7 @@
+-- The following warning is enabled in this module so that the import of
+-- Copilot.Core.Interpret.Eval and Render do not give rise to warnings.
+{-# OPTIONS_GHC -fno-warn-deprecations #-}
+
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 
 -- | An interpreter for Copilot specifications.
@@ -5,6 +9,7 @@
 {-# LANGUAGE Safe #-}
 
 module Copilot.Core.Interpret
+  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}
   ( Format (..)
   , interpret
   ) where
diff --git a/src/Copilot/Core/Interpret/Eval.hs b/src/Copilot/Core/Interpret/Eval.hs
--- a/src/Copilot/Core/Interpret/Eval.hs
+++ b/src/Copilot/Core/Interpret/Eval.hs
@@ -8,6 +8,7 @@
 {-# LANGUAGE Safe               #-}
 
 module Copilot.Core.Interpret.Eval
+  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}
   ( Env
   , Output
   , ExecTrace (..)
diff --git a/src/Copilot/Core/Interpret/Render.hs b/src/Copilot/Core/Interpret/Render.hs
--- a/src/Copilot/Core/Interpret/Render.hs
+++ b/src/Copilot/Core/Interpret/Render.hs
@@ -1,3 +1,7 @@
+-- The following warning is enabled in this module so that the import of
+-- Copilot.Core.Interpret.Eval does not give rise to a warning.
+{-# OPTIONS_GHC -fno-warn-deprecations #-}
+
 -- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
 
 -- | Pretty-print the results of a simulation.
@@ -5,6 +9,7 @@
 {-# LANGUAGE Safe #-}
 
 module Copilot.Core.Interpret.Render
+  {-# DEPRECATED "This module is deprecated in Copilot 3.11. Use copilot-interpreter instead." #-}
   ( renderAsTable
   , renderAsCSV
   ) where
diff --git a/src/Copilot/Core/PrettyDot.hs b/src/Copilot/Core/PrettyDot.hs
--- a/src/Copilot/Core/PrettyDot.hs
+++ b/src/Copilot/Core/PrettyDot.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE Safe  #-}
 
 module Copilot.Core.PrettyDot
+  {-# DEPRECATED "This module is deprecated in Copilot 3.11." #-}
   ( prettyPrintDot
   , prettyPrintExprDot
   ) where
diff --git a/src/Copilot/Core/Type.hs b/src/Copilot/Core/Type.hs
--- a/src/Copilot/Core/Type.hs
+++ b/src/Copilot/Core/Type.hs
@@ -102,8 +102,6 @@
   Double  :: Type Double
   Array   :: forall n t. ( KnownNat n
                          , Typed t
-                         , Typed (InnerType t)
-                         , Flatten t (InnerType t)
                          ) => Type t -> Type (Array n t)
   Struct  :: (Typed a, Struct a) => a -> Type a
 
@@ -209,7 +207,7 @@
 instance Typed Double where
   typeOf       = Double
   simpleType _ = SDouble
-instance (Typeable t, Typed t, KnownNat n, Flatten t (InnerType t), Typed (InnerType t)) => Typed (Array n t) where
+instance (Typeable t, Typed t, KnownNat n) => Typed (Array n t) where
   typeOf                = Array typeOf
   simpleType (Array t)  = SArray t
 
diff --git a/src/Copilot/Core/Type/Array.hs b/src/Copilot/Core/Type/Array.hs
--- a/src/Copilot/Core/Type/Array.hs
+++ b/src/Copilot/Core/Type/Array.hs
@@ -46,11 +46,14 @@
              ") does not match length of type (" ++ show typelen ++ ")."
 
 -- | Association between an array and the type of the elements it contains.
+{-# DEPRECATED InnerType "This type family is deprecated in Copilot 3.11." #-}
 type family InnerType x where
   InnerType (Array _ x) = InnerType x
   InnerType x           = x
 
 -- | Flattening or conversion of arrays to lists.
+{-# DEPRECATED Flatten "This class is deprecated in Copilot 3.11." #-}
+{-# DEPRECATED flatten "This function is deprecated in Copilot 3.11." #-}
 class Flatten a b where
   -- | Flatten an array to a list.
   flatten :: Array n a -> [b]
@@ -63,10 +66,12 @@
 instance Flatten a b => Flatten (Array n a) b where
   flatten (Array xss) = concat $ map flatten xss
 
+-- | This instance is deprecated in Copilot 3.11.
 instance Foldable (Array n) where
   foldr f base (Array xs) = foldr f base xs
 
 -- | Total number of elements in a possibly nested array.
+{-# DEPRECATED size "This function is deprecated in Copilot 3.11." #-}
 size :: forall a n b. (Flatten a b, b ~ InnerType a) => Array n a -> Int
 size xs = length $ (flatten xs :: [b])
 
diff --git a/src/Copilot/Core/Type/Dynamic.hs b/src/Copilot/Core/Type/Dynamic.hs
deleted file mode 100644
--- a/src/Copilot/Core/Type/Dynamic.hs
+++ /dev/null
@@ -1,45 +0,0 @@
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
-
-{-# LANGUAGE ExistentialQuantification #-}
-{-# LANGUAGE GADTs                     #-}
-{-# LANGUAGE KindSignatures            #-}
-{-# LANGUAGE Rank2Types                #-}
-{-# LANGUAGE Safe                      #-}
-{-# LANGUAGE ScopedTypeVariables       #-}
-
--- | An implementation of dynamic types using "Copilot.Core.Type.Equality".
--- The theory behind this technique is described the following paper:
---
--- * Baars, Arthur I. and Swierstra, S. Doaitse,
--- \"/Typing dynamic typing/\",
--- ACM SIGPLAN Notices vol. 37, p. 157-166, 2002
-
-module Copilot.Core.Type.Dynamic
-  {-# DEPRECATED "This module is deprecated in Copilot 3.8." #-}
-  ( Dynamic  (..)
-  , DynamicF (..)
-  , toDyn
-  , fromDyn
-  ) where
-
-import Copilot.Core.Type.Equality
-
--- | Representation of a value accompanied by its type.
-data Dynamic :: (* -> *) -> * where
-  Dynamic :: a -> t a -> Dynamic t
-
--- | Representation of a function accompanied by its type.
-data DynamicF :: (* -> *) -> (* -> *) -> * where
-  DynamicF :: f a -> t a -> DynamicF f t
-
--- | Enclose a value and its type in a container.
-toDyn :: t a -> a -> Dynamic t
-toDyn t x = Dynamic x t
-
--- | Extract a value from a dynamic. Return 'Nothing' if the value is not of
--- the given type.
-fromDyn :: EqualType t => t a -> Dynamic t -> Maybe a
-fromDyn t1 (Dynamic x t2) =
-  case t1 =~= t2 of
-    Just Refl -> return x
-    Nothing   -> Nothing
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -9,7 +9,6 @@
 import qualified Test.Copilot.Core.Interpret.Eval
 import qualified Test.Copilot.Core.Type
 import qualified Test.Copilot.Core.Type.Array
-import qualified Test.Copilot.Core.Type.Dynamic
 import qualified Test.Copilot.Core.Type.Show
 
 -- | Run all unit tests on copilot-core.
@@ -23,6 +22,5 @@
   , Test.Copilot.Core.Interpret.Eval.tests
   , Test.Copilot.Core.Type.tests
   , Test.Copilot.Core.Type.Array.tests
-  , Test.Copilot.Core.Type.Dynamic.tests
   , Test.Copilot.Core.Type.Show.tests
   ]
diff --git a/tests/Test/Copilot/Core/Type/Dynamic.hs b/tests/Test/Copilot/Core/Type/Dynamic.hs
deleted file mode 100644
--- a/tests/Test/Copilot/Core/Type/Dynamic.hs
+++ /dev/null
@@ -1,48 +0,0 @@
-{-# LANGUAGE GADTs #-}
--- | Test copilot-core:Copilot.Core.Type.Dynamic.
-module Test.Copilot.Core.Type.Dynamic where
-
--- External imports
-import Test.Framework                       (Test, testGroup)
-import Test.Framework.Providers.QuickCheck2 (testProperty)
-import Test.QuickCheck                      (Arbitrary, Property, property)
-
--- Internal imports: library modules being tested
-import Copilot.Core.Type          (Type (..))
-import Copilot.Core.Type.Dynamic  (fromDyn, toDyn)
-import Copilot.Core.Type.Equality (Equal (Refl), EqualType ((=~=)))
-
--- | All unit tests for copilot-core:Copilot.Core.Type.Dynamic.
-tests :: Test.Framework.Test
-tests =
-  testGroup "Copilot.Core.Type.Dynamic"
-    [ testProperty "fromDyn . toDyn == identity (Int64)"
-        (testDynamicIdentity Int64 Int64)
-    , testProperty "fromDyn . toDyn == identity (Bool)"
-        (testDynamicIdentity Bool Bool)
-    , testProperty "fromDyn . toDyn == identity (Float)"
-        (testDynamicIdentity Float Float)
-    , testProperty "fromDyn . toDyn == identity (Double)"
-        (testDynamicIdentity Double Double)
-    , testProperty "fromDyn . toDyn /= identity (Int64 vs Int32)"
-        (testDynamicIdentity Int64 Int32)
-    , testProperty "fromDyn . toDyn /= identity (Int64 vs Int16)"
-        (testDynamicIdentity Int64 Int16)
-    , testProperty "fromDyn . toDyn /= identity (Bool vs Int16)"
-        (testDynamicIdentity Bool Int16)
-    , testProperty "fromDyn . toDyn /= identity (Float vs Double)"
-        (testDynamicIdentity Float Double)
-    ]
-
--- | Test that wrapping in and unwrapping from a dynamic gets the original
--- value if the types match, and Nothing otherwise.
-testDynamicIdentity :: (Eq a, Arbitrary b)
-                    => Type a  -- ^ Type to unwrap to
-                    -> Type b  -- ^ Type to wrap to
-                    -> b       -- ^ Value to wrap
-                    -> Property
-testDynamicIdentity t1 t2 ls = property $
-  let unwrapped = fromDyn t1 (toDyn t2 ls)
-  in case t1 =~= t2 of
-       Nothing   -> Nothing == unwrapped
-       Just Refl -> Just ls == unwrapped