diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,15 @@
+2021-11-07
+        * Version bump (3.6). (#264)
+        * Deprecate Copilot.Core.Type.Dynamic.toDynF and fromDynF. (#269)
+        * Deprecate copilot-core:Copilot.Core.Type.Uninitialized. (#270)
+        * Deprecate export of copilot-core:Copilot.Core.Interpret.Render. (#268)
+        * Replace uses of copilot-core's error reporting functions. (#267)
+        * Introduce new ops atan2, ceiling, floor. (#246)
+        * Add initial support for unit testing. (#256)
+        * Deprecate unused type. (#260)
+        * Remove deprecated module. (#250)
+        * Fix outdated/broken links. (#252)
+
 2021-08-19
         * Version bump (3.5). (#247)
         * Update travis domain in README. (#222)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-[![Build Status](https://travis-ci.com/Copilot-Language/copilot-core.svg?branch=master)](https://travis-ci.com/Copilot-Language/copilot-core)
+[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](https://app.travis-ci.com/github/Copilot-Language/copilot)
 
 # Copilot: a stream DSL
 The core language, which efficiently represents Copilot expressions.  The core
@@ -30,4 +30,4 @@
 
 ## License
 Copilot is distributed under the BSD-3-Clause license, which can be found
-[here](https://raw.githubusercontent.com/Copilot-Language/copilot-core/master/LICENSE).
+[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-core/LICENSE).
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.5
+version:             3.6
 synopsis:            An intermediate representation for Copilot.
 description:
   Intermediate representation for Copilot.
@@ -55,7 +55,6 @@
     Copilot.Core.Interpret
     Copilot.Core.Interpret.Eval
     Copilot.Core.Interpret.Render
-    Copilot.Core.MakeTags
     Copilot.Core.Operators
     Copilot.Core.Spec
     Copilot.Core.Locals
@@ -69,3 +68,45 @@
     Copilot.Core.Type.Uninitialized
     Copilot.Core.PrettyPrint
     Copilot.Core.PrettyDot
+
+  other-modules:
+
+    Copilot.Core.ErrorInternal
+    Copilot.Core.Interpret.RenderInternal
+
+test-suite unit-tests
+  type:
+    exitcode-stdio-1.0
+
+  main-is:
+    Main.hs
+
+  other-modules:
+    Test.Extra
+    Test.Copilot.Core.Error
+    Test.Copilot.Core.External
+    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:
+      base
+    , HUnit
+    , QuickCheck
+    , pretty
+    , test-framework
+    , test-framework-hunit
+    , test-framework-quickcheck2
+
+    , copilot-core
+
+  hs-source-dirs:
+    tests
+
+  default-language:
+    Haskell2010
+
+  ghc-options:
+    -Wall
diff --git a/src/Copilot/Core.hs b/src/Copilot/Core.hs
--- a/src/Copilot/Core.hs
+++ b/src/Copilot/Core.hs
@@ -26,7 +26,6 @@
   ( module Copilot.Core.Error
   , module Copilot.Core.Expr
   , module Copilot.Core.External
-  , module Copilot.Core.MakeTags
   , module Copilot.Core.Operators
   , module Copilot.Core.Spec
   , module Copilot.Core.Type
@@ -39,7 +38,6 @@
 import Copilot.Core.Error
 import Copilot.Core.Expr
 import Copilot.Core.External
-import Copilot.Core.MakeTags
 import Copilot.Core.Operators
 import Copilot.Core.Spec
 import Copilot.Core.Type
diff --git a/src/Copilot/Core/Error.hs b/src/Copilot/Core/Error.hs
--- a/src/Copilot/Core/Error.hs
+++ b/src/Copilot/Core/Error.hs
@@ -9,18 +9,17 @@
   ( impossible
   , badUsage ) where
 
+import qualified Copilot.Core.ErrorInternal as Err
+
 -- | Report an error due to a bug in Copilot.
+{-# DEPRECATED impossible "This function is deprecated in Copilot 3.6." #-}
 impossible :: String -- ^ Name of the function in which the error was detected.
            -> String -- ^ Name of the package in which the function is located.
            -> a
-impossible function package =
-  error $ "\"Impossible\" error in function "
-    ++ function ++ ", in package " ++ package
-    ++ ". Please file an issue at "
-    ++ "https://github.com/Copilot-Language/copilot/issues"
-    ++ "or email the maintainers at <ivan.perezdominguez@nasa.gov>"
+impossible = Err.impossible
 
 -- | Report an error due to an error detected by Copilot (e.g., user error).
+{-# DEPRECATED badUsage "This function is deprecated in Copilot 3.6." #-}
 badUsage :: String -- ^ Description of the error.
          -> a
-badUsage msg = error $ "Copilot error: " ++ msg
+badUsage = Err.badUsage
diff --git a/src/Copilot/Core/ErrorInternal.hs b/src/Copilot/Core/ErrorInternal.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/ErrorInternal.hs
@@ -0,0 +1,26 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+{-# LANGUAGE Safe #-}
+
+-- | Custom functions to report error messages to users.
+module Copilot.Core.ErrorInternal
+  ( impossible
+  , badUsage ) where
+
+-- | Report an error due to a bug in Copilot.
+impossible :: String -- ^ Name of the function in which the error was detected.
+           -> String -- ^ Name of the package in which the function is located.
+           -> a
+impossible function package =
+  error $ "\"Impossible\" error in function "
+    ++ function ++ ", in package " ++ package
+    ++ ". Please file an issue at "
+    ++ "https://github.com/Copilot-Language/copilot/issues"
+    ++ "or email the maintainers at <ivan.perezdominguez@nasa.gov>"
+
+-- | Report an error due to an error detected by Copilot (e.g., user error).
+badUsage :: String -- ^ Description of the error.
+         -> a
+badUsage msg = error $ "Copilot error: " ++ msg
diff --git a/src/Copilot/Core/Expr.hs b/src/Copilot/Core/Expr.hs
--- a/src/Copilot/Core/Expr.hs
+++ b/src/Copilot/Core/Expr.hs
@@ -39,6 +39,7 @@
 --------------------------------------------------------------------------------
 
 -- | A unique tag for external arrays/function calls.
+{-# DEPRECATED Tag "The type Tag is deprecated in Copilot 3.6." #-}
 type Tag = Int
 
 --------------------------------------------------------------------------------
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
@@ -13,7 +13,7 @@
 
 import Copilot.Core
 import Copilot.Core.Interpret.Eval
-import Copilot.Core.Interpret.Render
+import Copilot.Core.Interpret.RenderInternal
 import Copilot.Core.Type.Show (ShowType(..))
 
 -- | Output format for the results of a Copilot spec interpretation.
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
@@ -14,7 +14,8 @@
   , eval
   ) where
 
-import Copilot.Core
+import Copilot.Core hiding (badUsage)
+import Copilot.Core.ErrorInternal (badUsage)
 import Copilot.Core.Type.Show (showWithType, ShowType)
 
 import Prelude hiding (id)
@@ -196,28 +197,36 @@
 -- 'Copilot.Core.Operators.Op1'.
 evalOp1 :: Op1 a b -> (a -> b)
 evalOp1 op = case op of
-  Not        -> P.not
-  Abs _      -> P.abs
-  Sign _     -> P.signum
-  Recip _    -> P.recip
-  Exp _      -> P.exp
-  Sqrt _     -> P.sqrt
-  Log _      -> P.log
-  Sin _      -> P.sin
-  Tan _      -> P.tan
-  Cos _      -> P.cos
-  Asin _     -> P.asin
-  Atan _     -> P.atan
-  Acos _     -> P.acos
-  Sinh _     -> P.sinh
-  Tanh _     -> P.tanh
-  Cosh _     -> P.cosh
-  Asinh _    -> P.asinh
-  Atanh _    -> P.atanh
-  Acosh _    -> P.acosh
-  BwNot _    -> complement
-  Cast _ _   -> P.fromIntegral
-  GetField (Struct _) _ f -> unfield . f where
+    Not        -> P.not
+    Abs _      -> P.abs
+    Sign _     -> P.signum
+    Recip _    -> P.recip
+    Exp _      -> P.exp
+    Sqrt _     -> P.sqrt
+    Log _      -> P.log
+    Sin _      -> P.sin
+    Tan _      -> P.tan
+    Cos _      -> P.cos
+    Asin _     -> P.asin
+    Atan _     -> P.atan
+    Acos _     -> P.acos
+    Sinh _     -> P.sinh
+    Tanh _     -> P.tanh
+    Cosh _     -> P.cosh
+    Asinh _    -> P.asinh
+    Atanh _    -> P.atanh
+    Acosh _    -> P.acosh
+    Ceiling _  -> P.fromIntegral . idI . P.ceiling
+    Floor _    -> P.fromIntegral . idI . P.floor
+    BwNot _    -> complement
+    Cast _ _   -> P.fromIntegral
+    GetField (Struct _) _ f -> unfield . f
+  where
+    -- Used to help GHC pick a return type for ceiling/floor
+    idI :: Integer -> Integer
+    idI = P.id
+
+    -- Extract value from field
     unfield (Field v) = v
 
 --------------------------------------------------------------------------------
@@ -237,6 +246,7 @@
   Fdiv _       -> (P./)
   Pow _        -> (P.**)
   Logb _       -> P.logBase
+  Atan2 _      -> P.atan2
   Eq _         -> (==)
   Ne _         -> (/=)
   Le _         -> (<=)
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
@@ -7,124 +7,9 @@
 {-# LANGUAGE Safe #-}
 
 module Copilot.Core.Interpret.Render
+  {-# DEPRECATED "This module is deprecated in Copilot 3.6." #-}
   ( renderAsTable
   , renderAsCSV
   ) where
 
-import Data.List (intersperse, transpose, foldl')
-import Data.Maybe (catMaybes)
-import Copilot.Core.Interpret.Eval (Output, ExecTrace (..))
-import Text.PrettyPrint
-
-import Prelude hiding ((<>))
-
---------------------------------------------------------------------------------
-
--- | Render an execution trace as a table, formatted to faciliate readability.
-renderAsTable :: ExecTrace -> String
-renderAsTable
-  ExecTrace
-    { interpTriggers  = trigs
-    , interpObservers = obsvs } = ( render
-                                  . asColumns
-                                  . transpose
-                                  . (:) (ppTriggerNames ++ ppObserverNames)
-                                  . transpose
-                                  ) (ppTriggerOutputs ++ ppObserverOutputs)
-     where
-
-     ppTriggerNames :: [Doc]
-     ppTriggerNames  = map (text . (++ ":")) (map fst trigs)
-
-     ppObserverNames :: [Doc]
-     ppObserverNames = map (text . (++ ":")) (map fst obsvs)
-
-     ppTriggerOutputs :: [[Doc]]
-     ppTriggerOutputs = map (map ppTriggerOutput) (map snd trigs)
-
-     ppTriggerOutput :: Maybe [Output] -> Doc
-     ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"
-     ppTriggerOutput Nothing   = text "--"
-
-     ppObserverOutputs :: [[Doc]]
-     ppObserverOutputs = map (map text) (map snd obsvs)
-
---------------------------------------------------------------------------------
-
--- | Render an execution trace as using comma-separate value (CSV) format.
-renderAsCSV :: ExecTrace -> String
-renderAsCSV = render . unfold
-
--- | Pretty print all the steps of the execution trace and concatenate the
--- results.
-unfold :: ExecTrace -> Doc
-unfold r =
-  case step r of
-    (cs, Nothing) -> cs
-    (cs, Just r') -> cs $$ unfold r'
-
--- | Pretty print the state of the triggers, and provide a continuation
--- for the execution trace at the next point in time.
-step :: ExecTrace -> (Doc, Maybe ExecTrace)
-step ExecTrace
-       { interpTriggers  = trigs
-       } =
-  if null trigs then (empty, Nothing)
-    else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)
-
-  where
-
-  ppTriggerOutputs :: [Doc]
-  ppTriggerOutputs =
-      catMaybes
-    . fmap ppTriggerOutput
-    . map (fmap head)
-    $ trigs
-
-  ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc
-  ppTriggerOutput (_,  Nothing) = Nothing
-  ppTriggerOutput (cs, Just xs) = Just $
-    text cs <> text "," <>
-      (foldr (<>) empty . map text . intersperse ",") xs
-
-  tails :: Maybe ExecTrace
-  tails =
-    if any null (fmap (tail.snd) trigs)
-      then Nothing
-      else Just
-        ExecTrace
-          { interpTriggers  = map (fmap tail) trigs
-          , interpObservers = []
-          }
-
---------------------------------------------------------------------------------
-
-
-
--- Copied from pretty-ncols because of incompatibility with newer GHC versions.
-asColumns :: [[Doc]] -> Doc
-asColumns = flip asColumnsWithBuff $ 1
-
-asColumnsWithBuff :: [[Doc]] -> Int -> Doc
-asColumnsWithBuff lls q = normalize
-        where normalize = vcat $ map hsep
-                        $ map (\x -> pad (length x) longColumnLen empty x)
-                        $ pad' longEntryLen q
-                        $ transpose lls -- normalize column height
-              longColumnLen = maximum (map length lls)
-              longEntryLen = maximum $ map docLen (concat lls)
-
-docLen d = length $ render d
-
--- | Pad a string on the right to reach an expected length.
-pad :: Int -> Int -> a -> [a] -> [a]
-pad lx max b ls = ls ++ replicate (max - lx) b
-
--- | Pad a list of strings on the right with spaces.
-pad' :: Int      -- ^ Mininum number of spaces to add
-     -> Int      -- ^ Maximum number of spaces to add
-     -> [[Doc]]  -- ^ List of documents to pad
-     -> [[Doc]]
-pad' _ _ []       = []
-pad' mx q (ls:xs) = map buf ls : pad' mx q xs
-        where buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
+import Copilot.Core.Interpret.RenderInternal
diff --git a/src/Copilot/Core/Interpret/RenderInternal.hs b/src/Copilot/Core/Interpret/RenderInternal.hs
new file mode 100644
--- /dev/null
+++ b/src/Copilot/Core/Interpret/RenderInternal.hs
@@ -0,0 +1,130 @@
+--------------------------------------------------------------------------------
+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
+--------------------------------------------------------------------------------
+
+-- | Pretty-print the results of a simulation.
+
+{-# LANGUAGE Safe #-}
+
+module Copilot.Core.Interpret.RenderInternal
+  ( renderAsTable
+  , renderAsCSV
+  ) where
+
+import Data.List (intersperse, transpose, foldl')
+import Data.Maybe (catMaybes)
+import Copilot.Core.Interpret.Eval (Output, ExecTrace (..))
+import Text.PrettyPrint
+
+import Prelude hiding ((<>))
+
+--------------------------------------------------------------------------------
+
+-- | Render an execution trace as a table, formatted to faciliate readability.
+renderAsTable :: ExecTrace -> String
+renderAsTable
+  ExecTrace
+    { interpTriggers  = trigs
+    , interpObservers = obsvs } = ( render
+                                  . asColumns
+                                  . transpose
+                                  . (:) (ppTriggerNames ++ ppObserverNames)
+                                  . transpose
+                                  ) (ppTriggerOutputs ++ ppObserverOutputs)
+     where
+
+     ppTriggerNames :: [Doc]
+     ppTriggerNames  = map (text . (++ ":")) (map fst trigs)
+
+     ppObserverNames :: [Doc]
+     ppObserverNames = map (text . (++ ":")) (map fst obsvs)
+
+     ppTriggerOutputs :: [[Doc]]
+     ppTriggerOutputs = map (map ppTriggerOutput) (map snd trigs)
+
+     ppTriggerOutput :: Maybe [Output] -> Doc
+     ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"
+     ppTriggerOutput Nothing   = text "--"
+
+     ppObserverOutputs :: [[Doc]]
+     ppObserverOutputs = map (map text) (map snd obsvs)
+
+--------------------------------------------------------------------------------
+
+-- | Render an execution trace as using comma-separate value (CSV) format.
+renderAsCSV :: ExecTrace -> String
+renderAsCSV = render . unfold
+
+-- | Pretty print all the steps of the execution trace and concatenate the
+-- results.
+unfold :: ExecTrace -> Doc
+unfold r =
+  case step r of
+    (cs, Nothing) -> cs
+    (cs, Just r') -> cs $$ unfold r'
+
+-- | Pretty print the state of the triggers, and provide a continuation
+-- for the execution trace at the next point in time.
+step :: ExecTrace -> (Doc, Maybe ExecTrace)
+step ExecTrace
+       { interpTriggers  = trigs
+       } =
+  if null trigs then (empty, Nothing)
+    else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)
+
+  where
+
+  ppTriggerOutputs :: [Doc]
+  ppTriggerOutputs =
+      catMaybes
+    . fmap ppTriggerOutput
+    . map (fmap head)
+    $ trigs
+
+  ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc
+  ppTriggerOutput (_,  Nothing) = Nothing
+  ppTriggerOutput (cs, Just xs) = Just $
+    text cs <> text "," <>
+      (foldr (<>) empty . map text . intersperse ",") xs
+
+  tails :: Maybe ExecTrace
+  tails =
+    if any null (fmap (tail.snd) trigs)
+      then Nothing
+      else Just
+        ExecTrace
+          { interpTriggers  = map (fmap tail) trigs
+          , interpObservers = []
+          }
+
+--------------------------------------------------------------------------------
+
+
+
+-- Copied from pretty-ncols because of incompatibility with newer GHC versions.
+asColumns :: [[Doc]] -> Doc
+asColumns = flip asColumnsWithBuff $ 1
+
+asColumnsWithBuff :: [[Doc]] -> Int -> Doc
+asColumnsWithBuff lls q = normalize
+        where normalize = vcat $ map hsep
+                        $ map (\x -> pad (length x) longColumnLen empty x)
+                        $ pad' longEntryLen q
+                        $ transpose lls -- normalize column height
+              longColumnLen = maximum (map length lls)
+              longEntryLen = maximum $ map docLen (concat lls)
+
+docLen d = length $ render d
+
+-- | Pad a string on the right to reach an expected length.
+pad :: Int -> Int -> a -> [a] -> [a]
+pad lx max b ls = ls ++ replicate (max - lx) b
+
+-- | Pad a list of strings on the right with spaces.
+pad' :: Int      -- ^ Mininum number of spaces to add
+     -> Int      -- ^ Maximum number of spaces to add
+     -> [[Doc]]  -- ^ List of documents to pad
+     -> [[Doc]]
+pad' _ _ []       = []
+pad' mx q (ls:xs) = map buf ls : pad' mx q xs
+        where buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
diff --git a/src/Copilot/Core/MakeTags.hs b/src/Copilot/Core/MakeTags.hs
deleted file mode 100644
--- a/src/Copilot/Core/MakeTags.hs
+++ /dev/null
@@ -1,113 +0,0 @@
---------------------------------------------------------------------------------
--- Copyright © 2011 National Institute of Aerospace / Galois, Inc.
---------------------------------------------------------------------------------
-
--- | Sets a unique tags for each external array\/function\/struct call.
-
-{-# LANGUAGE Safe #-}
-
-module Copilot.Core.MakeTags
-    {-# DEPRECATED "This module is deprecated in Copilot 3.3." #-}
-    (makeTags)
-  where
-
-import Copilot.Core.Expr
-import Copilot.Core.Spec
-import Control.Monad.State
-import Prelude hiding (id)
-
-next :: State Int Int
-next = do
-  k <- get
-  put (succ k)
-  return k
-
-makeTags :: Spec -> Spec
-makeTags spec = evalState (mkTagsSpec spec) 0
-
-mkTagsSpec :: Spec -> State Int Spec
-mkTagsSpec
-  Spec
-    { specStreams    = strms
-    , specObservers  = obsvs
-    , specTriggers   = trigs
-    , specProperties = props
-    } =
-  liftM4 Spec
-    (mkTagsStrms strms)
-    (mkTagsObsvs obsvs)
-    (mkTagsTrigs trigs)
-    (mkTagsProps props)
-
-mkTagsStrms :: [Stream] -> State Int [Stream]
-mkTagsStrms = mapM mkTagsStrm
-
-  where
-    mkTagsStrm Stream
-      { streamId         = id
-      , streamBuffer     = xs
-      , streamExpr       = e
-      , streamExprType   = t } =
-        do
-          e' <- mkTagsExpr e
-          return $ Stream
-            { streamId         = id
-            , streamBuffer     = xs
-            , streamExpr       = e'
-            , streamExprType   = t }
-
-mkTagsObsvs :: [Observer] -> State Int [Observer]
-mkTagsObsvs = mapM mkTagsObsv
-
-  where
-    mkTagsObsv Observer
-      { observerName     = name
-      , observerExpr     = e
-      , observerExprType = t } =
-        do
-          e' <- mkTagsExpr e
-          return $ Observer
-            { observerName     = name
-            , observerExpr     = e'
-            , observerExprType = t }
-
-mkTagsTrigs :: [Trigger] -> State Int [Trigger]
-mkTagsTrigs = mapM mkTagsTrig
-
- where
-   mkTagsTrig Trigger
-     { triggerName      = name
-     , triggerGuard     = g
-     , triggerArgs      = args } =
-       do
-         g' <- mkTagsExpr g
-         args' <- mapM mkTagsUExpr args
-         return $ Trigger
-           { triggerName      = name
-           , triggerGuard     = g'
-           , triggerArgs      = args' }
-
-mkTagsProps :: [Property] -> State Int [Property]
-mkTagsProps = mapM mkTagsProp
-
-  where mkTagsProp p = do
-          e' <- mkTagsExpr (propertyExpr p)
-          return $ p { propertyExpr = e' }
-
-mkTagsUExpr :: UExpr -> State Int UExpr
-mkTagsUExpr UExpr { uExprExpr = e, uExprType = t } =
-  do
-    e' <- mkTagsExpr e
-    return $ UExpr { uExprExpr = e', uExprType = t }
-
-mkTagsExpr :: Expr a -> State Int (Expr a)
-mkTagsExpr e0 = case e0 of
-  Const t x                      -> return $ Const t x
-  Drop t k id                    -> return $ Drop t k id
-  Local t1 t2 name e1 e2         -> liftM2 (Local t1 t2 name) (mkTagsExpr e1) (mkTagsExpr e2)
-  Var t name                     -> return $ Var t name
-  ExternVar t name e             -> return $ ExternVar t name e
-  Op1 op e                       -> liftM  (Op1 op) (mkTagsExpr e)
-  Op2 op e1 e2                   -> liftM2 (Op2 op) (mkTagsExpr e1) (mkTagsExpr e2)
-  Op3 op e1 e2 e3                -> liftM3 (Op3 op) (mkTagsExpr e1) (mkTagsExpr e2) (mkTagsExpr e3)
-  Label t s e                    -> liftM  (Label t s) (mkTagsExpr e)
diff --git a/src/Copilot/Core/Operators.hs b/src/Copilot/Core/Operators.hs
--- a/src/Copilot/Core/Operators.hs
+++ b/src/Copilot/Core/Operators.hs
@@ -46,6 +46,9 @@
   Asinh    :: Floating a => Type a -> Op1 a a
   Atanh    :: Floating a => Type a -> Op1 a a
   Acosh    :: Floating a => Type a -> Op1 a a
+  -- RealFrac operators
+  Ceiling  :: RealFrac a => Type a -> Op1 a a
+  Floor    :: RealFrac a => Type a -> Op1 a a
   -- Bitwise operators.
   BwNot    :: Bits     a => Type a -> Op1 a a
   -- Casting operator.
@@ -73,6 +76,8 @@
   -- Floating operators.
   Pow      :: Floating a => Type a -> Op2 a a a
   Logb     :: Floating a => Type a -> Op2 a a a
+  -- RealFloat operators.
+  Atan2    :: RealFloat a => Type a -> Op2 a a a
   -- Equality operators.
   Eq       :: Eq a => Type a -> Op2 a a Bool
   Ne       :: Eq a => Type a -> Op2 a a Bool
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
@@ -96,27 +96,29 @@
 -- | Pretty print a unary operator.
 ppOp1 :: Op1 a b -> String
 ppOp1 op = case op of
-  Not      -> "not"
-  Abs _    -> "abs"
-  Sign _   -> "signum"
-  Recip _  -> "recip"
-  Exp _    -> "exp"
-  Sqrt _   -> "sqrt"
-  Log _    -> "log"
-  Sin _    -> "sin"
-  Tan _    -> "tan"
-  Cos _    -> "cos"
-  Asin _   -> "asin"
-  Atan _   -> "atan"
-  Acos _   -> "acos"
-  Sinh _   -> "sinh"
-  Tanh _   -> "tanh"
-  Cosh _   -> "cosh"
-  Asinh _  -> "asinh"
-  Atanh _  -> "atanh"
-  Acosh _  -> "acosh"
-  BwNot _  -> "~"
-  Cast _ _ -> "(cast)"
+  Not       -> "not"
+  Abs _     -> "abs"
+  Sign _    -> "signum"
+  Recip _   -> "recip"
+  Exp _     -> "exp"
+  Sqrt _    -> "sqrt"
+  Log _     -> "log"
+  Sin _     -> "sin"
+  Tan _     -> "tan"
+  Cos _     -> "cos"
+  Asin _    -> "asin"
+  Atan _    -> "atan"
+  Acos _    -> "acos"
+  Sinh _    -> "sinh"
+  Tanh _    -> "tanh"
+  Cosh _    -> "cosh"
+  Asinh _   -> "asinh"
+  Atanh _   -> "atanh"
+  Acosh _   -> "acosh"
+  Ceiling _ -> "ceiling"
+  Floor _   -> "floor"
+  BwNot _   -> "~"
+  Cast _ _  -> "(cast)"
 
 -- | Pretty print a binary operator.
 ppOp2 :: Op2 a b c -> String
@@ -131,6 +133,7 @@
   Fdiv     _   -> "/"
   Pow      _   -> "**"
   Logb     _   -> "logBase"
+  Atan2    _   -> "atan2"
   Eq       _   -> "=="
   Ne       _   -> "/="
   Le       _   -> "<="
diff --git a/src/Copilot/Core/PrettyPrint.hs b/src/Copilot/Core/PrettyPrint.hs
--- a/src/Copilot/Core/PrettyPrint.hs
+++ b/src/Copilot/Core/PrettyPrint.hs
@@ -12,7 +12,8 @@
   , ppExpr
   ) where
 
-import Copilot.Core
+import Copilot.Core hiding (impossible)
+import Copilot.Core.ErrorInternal (impossible)
 import Copilot.Core.Type.Show (showWithType, ShowType(..), showType)
 import Prelude hiding (id, (<>))
 import Text.PrettyPrint.HughesPJ
@@ -72,6 +73,8 @@
   Asinh _                 -> ppPrefix "asinh"
   Atanh _                 -> ppPrefix "atanh"
   Acosh _                 -> ppPrefix "acosh"
+  Ceiling _               -> ppPrefix "ceiling"
+  Floor _                 -> ppPrefix "floor"
   BwNot _                 -> ppPrefix "~"
   Cast _ _                -> ppPrefix "(cast)"
   GetField (Struct _) _ f -> \e -> ppInfix "#" e (text $ accessorname f)
@@ -90,6 +93,7 @@
   Fdiv     _   -> ppInfix "/"
   Pow      _   -> ppInfix "**"
   Logb     _   -> ppInfix "logBase"
+  Atan2    _   -> ppInfix "atan2"
   Eq       _   -> ppInfix "=="
   Ne       _   -> ppInfix "/="
   Le       _   -> ppInfix "<="
diff --git a/src/Copilot/Core/Type/Dynamic.hs b/src/Copilot/Core/Type/Dynamic.hs
--- a/src/Copilot/Core/Type/Dynamic.hs
+++ b/src/Copilot/Core/Type/Dynamic.hs
@@ -49,11 +49,13 @@
     Nothing   -> Nothing
 
 -- | Enclose a function and its type in a container.
+{-# DEPRECATED toDynF "This function is deprecated in Copilot 3.6." #-}
 toDynF :: t a -> f a -> DynamicF f t
 toDynF t fx = DynamicF fx t
 
 -- | Extract a value from a dynamic function container. Return 'Nothing' if
 -- the value is not of the given type.
+{-# DEPRECATED fromDynF "This function is deprecated in Copilot 3.6." #-}
 fromDynF :: EqualType t => t a -> DynamicF f t -> Maybe (f a)
 fromDynF t1 (DynamicF fx t2) =
   case t1 =~= t2 of
diff --git a/src/Copilot/Core/Type/Eq.hs b/src/Copilot/Core/Type/Eq.hs
--- a/src/Copilot/Core/Type/Eq.hs
+++ b/src/Copilot/Core/Type/Eq.hs
@@ -12,7 +12,7 @@
   , UVal (..)
   ) where
 
-import Copilot.Core.Error (impossible)
+import Copilot.Core.ErrorInternal (impossible)
 import Copilot.Core.Type
 import Copilot.Core.Type.Dynamic (fromDyn, toDyn)
 
diff --git a/src/Copilot/Core/Type/Read.hs b/src/Copilot/Core/Type/Read.hs
--- a/src/Copilot/Core/Type/Read.hs
+++ b/src/Copilot/Core/Type/Read.hs
@@ -13,7 +13,7 @@
   ) where
 
 import Copilot.Core.Type
-import Copilot.Core.Error (badUsage)
+import Copilot.Core.ErrorInternal (badUsage)
 
 --------------------------------------------------------------------------------
 
diff --git a/src/Copilot/Core/Type/Uninitialized.hs b/src/Copilot/Core/Type/Uninitialized.hs
--- a/src/Copilot/Core/Type/Uninitialized.hs
+++ b/src/Copilot/Core/Type/Uninitialized.hs
@@ -18,6 +18,7 @@
 -- | Initial value for a given type.
 --
 -- Does not support structs or arrays.
+{-# DEPRECATED uninitialized "This function is deprecated in Copilot 3.6" #-}
 uninitialized :: Type a -> a
 uninitialized t =
   case t of
diff --git a/tests/Main.hs b/tests/Main.hs
new file mode 100644
--- /dev/null
+++ b/tests/Main.hs
@@ -0,0 +1,31 @@
+-- | Test copilot-core.
+module Main where
+
+-- External imports
+import Data.Monoid    (mempty)
+import Test.Framework (Test, defaultMainWithOpts)
+
+-- Internal library modules being tested
+import qualified Test.Copilot.Core.Error
+import qualified Test.Copilot.Core.External
+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.
+main :: IO ()
+main = defaultMainWithOpts tests mempty
+
+-- | All unit tests in copilot-core.
+tests :: [Test.Framework.Test]
+tests =
+  [ Test.Copilot.Core.Error.tests
+  , Test.Copilot.Core.External.tests
+  , 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/Error.hs b/tests/Test/Copilot/Core/Error.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Core/Error.hs
@@ -0,0 +1,35 @@
+-- | Test copilot-core:Copilot.Core.Error.
+module Test.Copilot.Core.Error where
+
+-- External imports
+import Test.Framework                 (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit                     (assertBool)
+
+-- Internal imports: auxiliary testing facilities
+import Test.Extra (withoutException)
+
+-- Internal imports: library modules being tested
+import Copilot.Core.Error (badUsage, impossible)
+
+-- | All unit tests for copilot-core:Copilot.Core.Error.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Core.Error"
+    [ testCase "impossible" testErrorImpossible
+    , testCase "badUsage"   testErrorBadUsage
+    ]
+
+-- * Individual tests
+
+-- | Test that 'Error.impossible' always throws an exception of some kind.
+testErrorImpossible :: IO ()
+testErrorImpossible = do
+  res <- not <$> withoutException (impossible "func1" "pkg1")
+  assertBool "The function impossible should fail with an exception" res
+
+-- | Test that 'Error.badUsage' always throws an exception of some kind.
+testErrorBadUsage :: IO ()
+testErrorBadUsage = do
+  res <- not <$> withoutException (badUsage "func1")
+  assertBool "The function badUsage should fail with an exception" res
diff --git a/tests/Test/Copilot/Core/External.hs b/tests/Test/Copilot/Core/External.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Core/External.hs
@@ -0,0 +1,43 @@
+-- | Test copilot-core:Copilot.Core.External.
+module Test.Copilot.Core.External where
+
+-- External imports
+import Data.List                      (sort)
+import Test.Framework                 (Test, testGroup)
+import Test.Framework.Providers.HUnit (testCase)
+import Test.HUnit                     (assertBool)
+
+-- Internal imports: library modules being tested
+import Copilot.Core.Expr      (Expr (ExternVar, Op1))
+import Copilot.Core.External  (externVarName, externVars)
+import Copilot.Core.Operators (Op1 (Abs, Sign))
+import Copilot.Core.Spec      (Spec (..), Stream (..))
+import Copilot.Core.Type      (Type (Int64))
+
+-- | All unit tests for copilot-core:Copilot.Core.External.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Core.External"
+    [ testCase "externVars" testExternVarsFind
+    ]
+
+-- * Individual tests
+
+-- | Test that 'externVars' will find an extern in a spec.
+testExternVarsFind :: IO ()
+testExternVarsFind = do
+  -- A simple stream and a nested stream
+  let s1     = Stream 1 [] (ExternVar Int64 "z" Nothing) Int64
+      s2     = Stream 2 [] s2Expr Int64
+      s2Expr = Op1 (Abs Int64)
+             $ Op1 (Sign Int64)
+             $ ExternVar Int64 "y" Nothing
+
+  -- Calculate the expected external vars in a spec
+  let res = sort $ map externVarName $ externVars $ Spec [s1, s2] [] [] []
+
+  -- Compare result with the expectation
+  let success = [ "y", "z" ] == res
+  assertBool
+    "The function externVars could not find the expected externs"
+    success
diff --git a/tests/Test/Copilot/Core/Interpret/Eval.hs b/tests/Test/Copilot/Core/Interpret/Eval.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Core/Interpret/Eval.hs
@@ -0,0 +1,770 @@
+{-# LANGUAGE ExistentialQuantification #-}
+-- | Test copilot-core:Copilot.Core.Interpret.Eval.
+--
+-- The gist of this evaluation is in 'SemanticsP' and 'checkSemanticsP' which
+-- evaluates an expression using Copilot's evaluator and compares it against
+-- its expected meaning.
+module Test.Copilot.Core.Interpret.Eval where
+
+-- External imports
+import Data.Bits                            (Bits, complement, shiftL, shiftR,
+                                             xor, (.&.), (.|.))
+import Data.Int                             (Int16, Int32, Int64, Int8)
+import Data.List                            (lookup)
+import Data.Maybe                           (fromMaybe)
+import Data.Typeable                        (Typeable)
+import Data.Word                            (Word16, Word32, Word64, Word8)
+import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.QuickCheck                      (Arbitrary, Gen, Property,
+                                             arbitrary, chooseInt, elements,
+                                             forAll, forAllShow, frequency,
+                                             getPositive, oneof, suchThat,
+                                             vectorOf)
+import Text.PrettyPrint.HughesPJ            (render)
+
+-- Internal imports: library modules being tested
+import Copilot.Core.Expr           (Expr (Const, Drop, Op1, Op2, Op3),
+                                    UExpr (UExpr))
+import Copilot.Core.Interpret.Eval (ExecTrace (interpObservers), eval)
+import Copilot.Core.Operators      (Op1 (..), Op2 (..), Op3 (..))
+import Copilot.Core.PrettyPrint    (ppExpr)
+import Copilot.Core.Spec           (Observer (..), Spec (..), Stream (Stream))
+import Copilot.Core.Type           (Typed (typeOf))
+import Copilot.Core.Type.Show      (ShowType (Haskell), showType)
+
+-- Internal imports: auxiliary functions
+import Test.Extra (apply1, apply2, apply3)
+
+-- * Constants
+
+-- | Max length of the traces being tested.
+maxTraceLength :: Int
+maxTraceLength = 200
+
+-- | All unit tests for copilot-core:Copilot.Core.Interpret.Eval.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Core.Interpret.Eval"
+    [ testProperty "eval Expr"           testEvalExpr
+    , testProperty "eval Expr with Drop" testEvalExprWithDrop
+    ]
+
+-- * Individual tests
+
+-- | Test for expression evaluation.
+testEvalExpr :: Property
+testEvalExpr =
+  forAll (chooseInt (0, maxTraceLength)) $ \steps ->
+  forAllShow arbitrarySemanticsP (semanticsShowK steps) $ \pair ->
+  checkSemanticsP steps [] pair
+
+-- | Test for expression evaluation with a drop.
+testEvalExprWithDrop :: Property
+testEvalExprWithDrop =
+  forAll (chooseInt (0, maxTraceLength)) $ \steps ->
+  forAllShow arbitrarySemanticsP (semanticsShowK steps) $ \pair ->
+  forAllShow (arbitraryDrop pair) (semanticsShowK steps . snd) $ \(str, sem) ->
+  checkSemanticsP steps [str] sem
+
+-- * Random generators
+
+-- ** Random SemanticsP generators
+
+-- | An arbitrary expression, paired with its expected meaning.
+--
+-- See the function 'checkSemanticsP' to evaluate the pair.
+arbitrarySemanticsP :: Gen SemanticsP
+arbitrarySemanticsP = oneof
+  [ SemanticsP <$> (arbitraryBoolExpr         :: Gen (Semantics Bool))
+  , SemanticsP <$> (arbitraryNumExpr          :: Gen (Semantics Int8))
+  , SemanticsP <$> (arbitraryNumExpr          :: Gen (Semantics Int16))
+  , SemanticsP <$> (arbitraryNumExpr          :: Gen (Semantics Int32))
+  , SemanticsP <$> (arbitraryNumExpr          :: Gen (Semantics Int64))
+  , SemanticsP <$> (arbitraryNumExpr          :: Gen (Semantics Word8))
+  , SemanticsP <$> (arbitraryNumExpr          :: Gen (Semantics Word16))
+  , SemanticsP <$> (arbitraryNumExpr          :: Gen (Semantics Word32))
+  , SemanticsP <$> (arbitraryNumExpr          :: Gen (Semantics Word64))
+  , SemanticsP <$> (arbitraryFloatingExpr     :: Gen (Semantics Float))
+  , SemanticsP <$> (arbitraryFloatingExpr     :: Gen (Semantics Double))
+  , SemanticsP <$> (arbitraryRealFracExpr     :: Gen (Semantics Float))
+  , SemanticsP <$> (arbitraryRealFracExpr     :: Gen (Semantics Double))
+  , SemanticsP <$> (arbitraryRealFloatExpr    :: Gen (Semantics Float))
+  , SemanticsP <$> (arbitraryRealFloatExpr    :: Gen (Semantics Double))
+  , SemanticsP <$> (arbitraryFractionalExpr   :: Gen (Semantics Float))
+  , SemanticsP <$> (arbitraryFractionalExpr   :: Gen (Semantics Double))
+  , SemanticsP <$> (arbitraryIntegralExpr     :: Gen (Semantics Int8))
+  , SemanticsP <$> (arbitraryIntegralExpr     :: Gen (Semantics Int16))
+  , SemanticsP <$> (arbitraryIntegralExpr     :: Gen (Semantics Int32))
+  , SemanticsP <$> (arbitraryIntegralExpr     :: Gen (Semantics Int64))
+  , SemanticsP <$> (arbitraryIntegralExpr     :: Gen (Semantics Word8))
+  , SemanticsP <$> (arbitraryIntegralExpr     :: Gen (Semantics Word16))
+  , SemanticsP <$> (arbitraryIntegralExpr     :: Gen (Semantics Word32))
+  , SemanticsP <$> (arbitraryIntegralExpr     :: Gen (Semantics Word64))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Bool))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Int8))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Int16))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Int32))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Int64))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Word8))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Word16))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Word32))
+  , SemanticsP <$> (arbitraryBitsExpr         :: Gen (Semantics Word64))
+  , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int8))
+  , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int16))
+  , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int32))
+  , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int64))
+  , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word8))
+  , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word16))
+  , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word32))
+  , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word64))
+  ]
+
+-- | Generate an arbitrary drop by taking an expression, adding a number of
+-- elements to it, and then dropping some.
+arbitraryDrop :: SemanticsP -> Gen (Stream, SemanticsP)
+arbitraryDrop (SemanticsP (expr, meaning)) = do
+  -- Randomly generate a list of elements
+  prependLength <- getPositive <$> arbitrary
+  buffer        <- vectorOf prependLength arbitrary
+
+  -- Build the stream with the buffer
+  let streamId = 0
+      stream   = Stream streamId buffer expr typeOf
+
+  -- Select how many elements to drop from the stream (up to the length of the
+  -- buffer)
+  dropLength <- chooseInt (0, prependLength)
+
+  -- Build a drop expression that drops those many elements, paired with its
+  -- meaning.
+  let expr'    = Drop typeOf (fromIntegral dropLength) streamId
+      meaning' = drop dropLength buffer ++ meaning
+
+  return (stream, SemanticsP (expr', meaning'))
+
+-- ** Random Expr generators
+
+-- | An arbitrary constant expression of any type, paired with its expected
+-- meaning.
+arbitraryConst :: (Arbitrary t, Typed t)
+               => Gen (Expr t, [t])
+arbitraryConst = (\v -> (Const typeOf v, repeat v)) <$> arbitrary
+
+-- | An arbitrary boolean expression, paired with its expected meaning.
+arbitraryBoolExpr :: Gen (Expr Bool, [Bool])
+arbitraryBoolExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (5, apply1 <$> arbitraryBoolOp1 <*> arbitraryBoolExpr)
+
+    , (1, apply2 <$> arbitraryBoolOp2
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryBoolExpr)
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryBoolExpr)
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBitsExpr
+                 <*> (arbitraryBitsExpr :: Gen (Expr Int8, [Int8])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBitsExpr
+                 <*> (arbitraryBitsExpr :: Gen (Expr Int16, [Int16])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBitsExpr
+                 <*> (arbitraryBitsExpr :: Gen (Expr Int32, [Int32])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBitsExpr
+                 <*> (arbitraryBitsExpr :: Gen (Expr Int64, [Int64])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBitsExpr
+                 <*> (arbitraryBitsExpr :: Gen (Expr Word8, [Word8])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBitsExpr
+                 <*> (arbitraryBitsExpr :: Gen (Expr Word16, [Word16])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBitsExpr
+                 <*> (arbitraryBitsExpr :: Gen (Expr Word32, [Word32])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryBitsExpr
+                 <*> (arbitraryBitsExpr :: Gen (Expr Word64, [Word64])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Int8, [Int8])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Int16, [Int16])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Int32, [Int32])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Int64, [Int64])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Word8, [Word8])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Word16, [Word16])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Word32, [Word32])))
+
+    , (1, apply2 <$> arbitraryEqOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Word64, [Word64])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Int8, [Int8])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Int16, [Int16])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Int32, [Int32])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Int64, [Int64])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Word8, [Word8])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Word16, [Word16])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Word32, [Word32])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryNumExpr
+                 <*> (arbitraryNumExpr :: Gen (Expr Word64, [Word64])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryFloatingExpr
+                 <*> (arbitraryFloatingExpr :: Gen (Expr Float, [Float])))
+
+    , (1, apply2 <$> arbitraryOrdOp2
+                 <*> arbitraryFloatingExpr
+                 <*> (arbitraryFloatingExpr :: Gen (Expr Double, [Double])))
+
+    , (1, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryBoolExpr)
+    ]
+
+-- | An arbitrary numeric expression, paired with its expected meaning.
+arbitraryNumExpr :: (Arbitrary t, Typed t, Num t)
+                 => Gen (Expr t, [t])
+arbitraryNumExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryNumExpr)
+
+    , (2, apply2 <$> arbitraryNumOp2 <*> arbitraryNumExpr <*> arbitraryNumExpr)
+
+    , (2, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryNumExpr
+                 <*> arbitraryNumExpr)
+    ]
+
+-- | An arbitrary floating point expression, paired with its expected meaning.
+arbitraryFloatingExpr :: (Arbitrary t, Typed t, Floating t)
+                      => Gen (Expr t, [t])
+arbitraryFloatingExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (5, apply1 <$> arbitraryFloatingOp1 <*> arbitraryFloatingExpr)
+
+    , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryFloatingExpr)
+
+    , (2, apply2 <$> arbitraryFloatingOp2
+                 <*> arbitraryFloatingExpr
+                 <*> arbitraryFloatingExpr)
+
+    , (2, apply2 <$> arbitraryNumOp2
+                 <*> arbitraryFloatingExpr
+                 <*> arbitraryFloatingExpr)
+
+    , (1, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryFloatingExpr
+                 <*> arbitraryFloatingExpr)
+    ]
+
+-- | An arbitrary realfrac expression, paired with its expected meaning.
+arbitraryRealFracExpr :: (Arbitrary t, Typed t, RealFrac t)
+                      => Gen (Expr t, [t])
+arbitraryRealFracExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (2, apply1 <$> arbitraryRealFracOp1 <*> arbitraryRealFracExpr)
+
+    , (5, apply1 <$> arbitraryNumOp1      <*> arbitraryRealFracExpr)
+
+    , (1, apply2 <$> arbitraryNumOp2
+                 <*> arbitraryRealFracExpr
+                 <*> arbitraryRealFracExpr)
+
+    , (1, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryRealFracExpr
+                 <*> arbitraryRealFracExpr)
+    ]
+
+-- | An arbitrary realfloat expression, paired with its expected meaning.
+arbitraryRealFloatExpr :: (Arbitrary t, Typed t, RealFloat t)
+                       => Gen (Expr t, [t])
+arbitraryRealFloatExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (2, apply1 <$> arbitraryNumOp1 <*> arbitraryRealFloatExpr)
+
+    , (5, apply2 <$> arbitraryRealFloatOp2
+                 <*> arbitraryRealFloatExpr
+                 <*> arbitraryRealFloatExpr)
+
+    , (1, apply2 <$> arbitraryNumOp2
+                 <*> arbitraryRealFloatExpr
+                 <*> arbitraryRealFloatExpr)
+
+    , (1, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryRealFloatExpr
+                 <*> arbitraryRealFloatExpr)
+    ]
+
+-- | An arbitrary fractional expression, paired with its expected meaning.
+--
+-- We add the constraint Eq because we sometimes need to make sure numbers are
+-- not zero.
+arbitraryFractionalExpr :: (Arbitrary t, Typed t, Fractional t, Eq t)
+                        => Gen (Expr t, [t])
+arbitraryFractionalExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (5, apply1 <$> arbitraryFractionalOp1 <*> arbitraryFractionalExpr)
+
+    , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryFractionalExpr)
+
+    , (2, apply2 <$> arbitraryFractionalOp2
+                 <*> arbitraryFractionalExpr
+                 <*> arbitraryFractionalExprNonZero)
+
+    , (1, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryFractionalExpr
+                 <*> arbitraryFractionalExpr)
+    ]
+  where
+
+    -- Generator for fractional expressions that are never zero.
+    --
+    -- The list is infinite, so this generator checks up to maxTraceLength
+    -- elements.
+    arbitraryFractionalExprNonZero = arbitraryFractionalExpr
+      `suchThat` (notElem 0 . take maxTraceLength . snd)
+
+-- | An arbitrary integral expression, paired with its expected meaning.
+--
+-- We add the constraint Eq because we sometimes need to make sure numbers are
+-- not zero.
+arbitraryIntegralExpr :: (Arbitrary t, Typed t, Integral t, Eq t)
+                      => Gen (Expr t, [t])
+arbitraryIntegralExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryIntegralExpr)
+
+    , (2, apply2 <$> arbitraryNumOp2
+                 <*> arbitraryIntegralExpr
+                 <*> arbitraryIntegralExpr)
+
+    , (2, apply2 <$> arbitraryIntegralOp2
+                 <*> arbitraryIntegralExpr
+                 <*> arbitraryIntegralExprNonZero)
+
+    , (1, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryIntegralExpr
+                 <*> arbitraryIntegralExpr)
+    ]
+  where
+
+    -- Generator for integral expressions that are never zero.
+    --
+    -- The list is infinite, so this generator checks up to maxTraceLength
+    -- elements.
+    arbitraryIntegralExprNonZero = arbitraryIntegralExpr
+      `suchThat` (notElem 0 . take maxTraceLength . snd)
+
+-- | An arbitrary Bits expression, paired with its expected meaning.
+arbitraryBitsExpr :: (Arbitrary t, Typed t, Bits t)
+                  => Gen (Expr t, [t])
+arbitraryBitsExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (5, apply1 <$> arbitraryBitsOp1 <*> arbitraryBitsExpr)
+
+    , (2, apply2 <$> arbitraryBitsOp2
+                 <*> arbitraryBitsExpr
+                 <*> arbitraryBitsExpr)
+
+    , (2, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryBitsExpr <*> arbitraryBitsExpr)
+    ]
+
+-- | An arbitrary expression for types that are instances of Bits and Integral,
+-- paired with its expected meaning.
+arbitraryBitsIntegralExpr :: (Arbitrary t, Typed t, Bits t, Integral t)
+                          => Gen (Expr t, [t])
+arbitraryBitsIntegralExpr =
+  -- We use frequency instead of oneof because the random expression generator
+  -- seems to generate expressions that are too large and the test fails due
+  -- to running out of memory.
+  frequency
+    [ (10, arbitraryConst)
+
+    , (2, apply1 <$> arbitraryNumOp1 <*> arbitraryBitsIntegralExpr)
+
+    , (1, apply2 <$> arbitraryNumOp2
+                 <*> arbitraryBitsIntegralExpr
+                 <*> arbitraryBitsIntegralExpr)
+
+    , (5, apply2 <$> arbitraryBitsIntegralOp2
+                 <*> arbitraryBitsIntegralExpr
+                 <*> arbitraryBitsIntegralExpr)
+
+    , (1, apply3 <$> arbitraryITEOp3
+                 <*> arbitraryBoolExpr
+                 <*> arbitraryBitsIntegralExpr
+                 <*> arbitraryBitsIntegralExpr)
+    ]
+
+-- ** Operators
+
+-- *** Op 1
+
+-- | Generator for arbitrary boolean operators with arity 1, paired with their
+-- expected meaning.
+arbitraryBoolOp1 :: Gen (Expr Bool -> Expr Bool, [Bool] -> [Bool])
+arbitraryBoolOp1 = elements
+  [ (Op1 Not, fmap not)
+  ]
+
+-- | Generator for arbitrary numeric operators with arity 1, paired with their
+-- expected meaning.
+arbitraryNumOp1 :: (Typed t, Num t)
+                => Gen (Expr t -> Expr t, [t] -> [t])
+arbitraryNumOp1 = elements
+  [ (Op1 (Abs typeOf),  fmap abs)
+  , (Op1 (Sign typeOf), fmap signum)
+  ]
+
+-- | Generator for arbitrary floating point operators with arity 1, paired with
+-- their expected meaning.
+arbitraryFloatingOp1 :: (Typed t, Floating t)
+                     => Gen (Expr t -> Expr t, [t] -> [t])
+arbitraryFloatingOp1 = elements
+  [ (Op1 (Exp typeOf),   fmap exp)
+  , (Op1 (Sqrt typeOf),  fmap sqrt)
+  , (Op1 (Log typeOf),   fmap log)
+  , (Op1 (Sin typeOf),   fmap sin)
+  , (Op1 (Tan typeOf),   fmap tan)
+  , (Op1 (Cos typeOf),   fmap cos)
+  , (Op1 (Asin typeOf),  fmap asin)
+  , (Op1 (Atan typeOf),  fmap atan)
+  , (Op1 (Acos typeOf),  fmap acos)
+  , (Op1 (Sinh typeOf),  fmap sinh)
+  , (Op1 (Tanh typeOf),  fmap tanh)
+  , (Op1 (Cosh typeOf),  fmap cosh)
+  , (Op1 (Asinh typeOf), fmap asinh)
+  , (Op1 (Atanh typeOf), fmap atanh)
+  , (Op1 (Acosh typeOf), fmap acosh)
+  ]
+
+-- | Generator for arbitrary realfrac operators with arity 1, paired with their
+-- expected meaning.
+arbitraryRealFracOp1 :: (Typed t, RealFrac t)
+                     => Gen (Expr t -> Expr t, [t] -> [t])
+arbitraryRealFracOp1 = elements
+    [ (Op1 (Ceiling typeOf), fmap (fromIntegral . idI . ceiling))
+    , (Op1 (Floor typeOf), fmap (fromIntegral . idI . floor))
+    ]
+  where
+    -- Auxiliary function to help the compiler determine which integral type
+    -- the result of ceiling must be converted to. An Integer ensures that the
+    -- result fits and there is no loss of precision due to the intermediate
+    -- casting.
+    idI :: Integer -> Integer
+    idI = id
+
+-- | Generator for arbitrary fractional operators with arity 1, paired with
+-- their expected meaning.
+arbitraryFractionalOp1 :: (Typed t, Fractional t)
+                       => Gen (Expr t -> Expr t, [t] -> [t])
+arbitraryFractionalOp1 = elements
+  [ (Op1 (Recip typeOf), fmap recip)
+  ]
+
+-- | Generator for arbitrary bitwise operators with arity 1, paired with their
+-- expected meaning.
+arbitraryBitsOp1 :: (Typed t, Bits t)
+                 => Gen (Expr t -> Expr t, [t] -> [t])
+arbitraryBitsOp1 = elements
+  [ (Op1 (BwNot typeOf), fmap complement)
+  ]
+
+-- *** Op 2
+
+-- | Generator for arbitrary boolean operators with arity 2, paired with their
+-- expected meaning.
+arbitraryBoolOp2 :: Gen ( Expr Bool -> Expr Bool -> Expr Bool
+                        , [Bool] -> [Bool] -> [Bool]
+                        )
+arbitraryBoolOp2 = elements
+  [ (Op2 And, zipWith (&&))
+  , (Op2 Or,  zipWith (||))
+  ]
+
+-- | Generator for arbitrary numeric operators with arity 2, paired with their
+-- expected meaning.
+arbitraryNumOp2 :: (Typed t, Num t)
+                => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])
+arbitraryNumOp2 = elements
+  [ (Op2 (Add typeOf), zipWith (+))
+  , (Op2 (Sub typeOf), zipWith (-))
+  , (Op2 (Mul typeOf), zipWith (*))
+  ]
+
+-- | Generator for arbitrary integral operators with arity 2, paired with their
+-- expected meaning.
+arbitraryIntegralOp2 :: (Typed t, Integral t)
+                     => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])
+arbitraryIntegralOp2 = elements
+  [ (Op2 (Mod typeOf), zipWith mod)
+  , (Op2 (Div typeOf), zipWith quot)
+  ]
+
+-- | Generator for arbitrary fractional operators with arity 2, paired with
+-- their expected meaning.
+arbitraryFractionalOp2 :: (Typed t, Fractional t)
+                       => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])
+arbitraryFractionalOp2 = elements
+  [ (Op2 (Fdiv typeOf), zipWith (/))
+  ]
+
+-- | Generator for arbitrary floating point operators with arity 2, paired with
+-- their expected meaning.
+arbitraryFloatingOp2 :: (Typed t, Floating t)
+                     => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])
+arbitraryFloatingOp2 = elements
+  [ (Op2 (Pow typeOf),  zipWith (**))
+  , (Op2 (Logb typeOf), zipWith logBase)
+  ]
+
+-- | Generator for arbitrary floating point operators with arity 2, paired with
+-- their expected meaning.
+arbitraryRealFloatOp2 :: (Typed t, RealFloat t)
+                      => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])
+arbitraryRealFloatOp2 = elements
+  [ (Op2 (Atan2 typeOf), zipWith atan2)
+  ]
+
+-- | Generator for arbitrary equality operators with arity 2, paired with their
+-- expected meaning.
+arbitraryEqOp2 :: (Typed t, Eq t)
+               => Gen (Expr t -> Expr t -> Expr Bool, [t] -> [t] -> [Bool])
+arbitraryEqOp2 = elements
+  [ (Op2 (Eq typeOf), zipWith (==))
+  , (Op2 (Ne typeOf), zipWith (/=))
+  ]
+
+-- | Generator for arbitrary ordering operators with arity 2, paired with their
+-- expected meaning.
+arbitraryOrdOp2 :: (Typed t, Ord t)
+                => Gen (Expr t -> Expr t -> Expr Bool, [t] -> [t] -> [Bool])
+arbitraryOrdOp2 = elements
+  [ (Op2 (Le typeOf), zipWith (<=))
+  , (Op2 (Lt typeOf), zipWith (<))
+  , (Op2 (Ge typeOf), zipWith (>=))
+  , (Op2 (Gt typeOf), zipWith (>))
+  ]
+
+-- | Generator for arbitrary bitwise operators with arity 2, paired with their
+-- expected meaning.
+arbitraryBitsOp2 :: (Typed t, Bits t)
+                 => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])
+arbitraryBitsOp2 = elements
+  [ (Op2 (BwAnd typeOf), zipWith (.&.))
+  , (Op2 (BwOr typeOf),  zipWith (.|.))
+  , (Op2 (BwXor typeOf), zipWith xor)
+  ]
+
+-- | Generator for arbitrary bit shifting operators with arity 2, paired with
+-- their expected meaning.
+--
+-- This generator is a bit more strict in its type signature than the
+-- underlying bit-shifting operators being tested, since it enforces both the
+-- value being manipulated and the value that indicates how much to shift by to
+-- have the same type.
+arbitraryBitsIntegralOp2 :: (Typed t, Bits t, Integral t)
+                         => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])
+arbitraryBitsIntegralOp2 = elements
+  [ (Op2 (BwShiftL typeOf typeOf), zipWith (\x y -> shiftL x (fromIntegral y)))
+  , (Op2 (BwShiftR typeOf typeOf), zipWith (\x y -> shiftR x (fromIntegral y)))
+  ]
+
+-- *** Op 3
+
+-- | Generator for if-then-else operator (with arity 3), paired with its
+-- expected meaning.
+--
+-- Although this is constant and there is nothing arbitrary, we use the same
+-- structure and naming convention as with others for simplicity.
+arbitraryITEOp3 :: (Arbitrary t, Typed t)
+                => Gen ( Expr Bool -> Expr t -> Expr t -> Expr t
+                       , [Bool] -> [t] -> [t] -> [t]
+                       )
+arbitraryITEOp3 = return
+  (Op3 (Mux typeOf), zipWith3 (\x y z -> if x then y else z))
+
+-- * Semantics
+
+-- | Type that pairs an expression with its meaning as an infinite stream.
+type Semantics t = (Expr t, [t])
+
+-- | A phantom semantics pair is an existential type that encloses an
+-- expression and its expected meaning as an infinite list of values.
+--
+-- It is needed by the arbitrary expression generator, to create a
+-- heterogeneous list.
+data SemanticsP = forall t
+                . (Typeable t, Read t, Eq t, Show t, Typed t, Arbitrary t)
+                => SemanticsP
+  { semanticsPair :: (Expr t, [t])
+  }
+
+-- | Show function for test triplets that limits the accompanying list
+-- to a certain length.
+semanticsShowK :: Int -> SemanticsP -> String
+semanticsShowK steps (SemanticsP (expr, exprList)) =
+    show (showType ty, render $ ppExpr expr, take steps exprList)
+
+  where
+
+    -- Type of the expression. The type is enforced by _u below.
+    ty = typeOf
+
+    -- We want to show the type. To help GHC determine that the type t is the
+    -- same as the expression's (expr), we use an UExpr, which has an
+    -- additional constraint. This definition serves no other purpose than to
+    -- help enforce that constraint.
+    _u = UExpr ty expr
+
+-- | Check that the expression in the semantics pair is evaluated to the given
+-- list, up to a number of steps.
+--
+-- Some operations will overflow and return NaN. Because comparing any NaN
+-- will, as per IEEE 754, always fail (i.e., return False), we handle that
+-- specific case by stating that the test succeeds if any expected values
+-- is NaN.
+checkSemanticsP :: Int -> [Stream] -> SemanticsP -> Bool
+checkSemanticsP steps streams (SemanticsP (expr, exprList)) =
+    any isNaN' expectation || resultValues == expectation
+  where
+    -- Limit expectation to the number of evaluation steps.
+    expectation = take steps exprList
+
+    -- Obtain the results by looking up the observer in the spec
+    -- and parsing the results into Haskell values.
+    resultValues = fmap readResult results
+    results      = lookupWithDefault testObserverName []
+                 $ interpObservers trace
+
+    -- Spec with just one observer of one expression.
+    trace     = eval Haskell steps spec
+    spec      = Spec streams observers [] []
+    observers = [Observer testObserverName expr typeOf]
+
+    -- Fixed name for the observer. Used to obtain the result from the
+    -- trace. It should be the only observer in the trace.
+    testObserverName :: String
+    testObserverName = "res"
+
+    -- | Is NaN with Eq requirement only.
+    isNaN' :: Eq a => a -> Bool
+    isNaN' x = x /= x
+
+-- * Auxiliary
+
+-- | Read a Haskell value from the output of the evaluator.
+readResult :: Read a => String -> a
+readResult = read . readResult'
+  where
+    readResult' :: String -> String
+    readResult' "false" = "False"
+    readResult' "true"  = "True"
+    readResult' s       = s
+
+-- | Variant of 'lookup' with an additional default value returned when the key
+-- provided is not found in the map.
+lookupWithDefault :: Ord k => k -> v -> [(k, v)] -> v
+lookupWithDefault k def = fromMaybe def . lookup k
diff --git a/tests/Test/Copilot/Core/Type.hs b/tests/Test/Copilot/Core/Type.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Core/Type.hs
@@ -0,0 +1,69 @@
+-- | Test copilot-core:Copilot.Core.Type.
+module Test.Copilot.Core.Type where
+
+-- External imports
+import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.QuickCheck                      (Property, elements, forAllBlind,
+                                             shuffle, (==>))
+
+-- Internal imports: library modules being tested
+import Copilot.Core.Type (SimpleType (..))
+
+-- | All unit tests for copilot-core:Copilot.Core.Type.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Core.Type"
+    [ testProperty "reflexivity of equality of simple types"
+        testSimpleTypesEqualityReflexive
+    , testProperty "symmetry of equality of simple types"
+        testSimpleTypesEqualitySymmetric
+    , testProperty "transitivity of equality of simple types"
+        testSimpleTypesEqualityTransitive
+    , testProperty "uniqueness of equality of simple types"
+        testSimpleTypesEqualityUniqueness
+    ]
+
+-- | Test that the equality relation for simple types is reflexive.
+testSimpleTypesEqualityReflexive :: Property
+testSimpleTypesEqualityReflexive =
+  forAllBlind (elements simpleTypes) $ \t ->
+    t == t
+
+-- | Test that the equality relation for simple types is symmetric.
+testSimpleTypesEqualitySymmetric :: Property
+testSimpleTypesEqualitySymmetric =
+  forAllBlind (elements simpleTypes) $ \t1 ->
+  forAllBlind (elements simpleTypes) $ \t2 ->
+    t1 == t2 ==> t2 == t1
+
+-- | Test that the equality relation for simple types is transitive.
+testSimpleTypesEqualityTransitive :: Property
+testSimpleTypesEqualityTransitive =
+  forAllBlind (elements simpleTypes) $ \t1 ->
+  forAllBlind (elements simpleTypes) $ \t2 ->
+  forAllBlind (elements simpleTypes) $ \t3 ->
+    (t1 == t2 && t2 == t3) ==> (t1 == t3)
+
+-- | Test that each type is only equal to itself.
+testSimpleTypesEqualityUniqueness :: Property
+testSimpleTypesEqualityUniqueness =
+  forAllBlind (shuffle simpleTypes) $ \(t:ts) ->
+    notElem t ts
+
+-- | Simple types tested.
+simpleTypes :: [SimpleType]
+simpleTypes =
+  [ SBool
+  , SInt8
+  , SInt16
+  , SInt32
+  , SInt64
+  , SWord8
+  , SWord16
+  , SWord32
+  , SWord64
+  , SFloat
+  , SDouble
+  , SStruct
+  ]
diff --git a/tests/Test/Copilot/Core/Type/Array.hs b/tests/Test/Copilot/Core/Type/Array.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Core/Type/Array.hs
@@ -0,0 +1,132 @@
+{-# LANGUAGE DataKinds           #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+-- | Test copilot-core:Copilot.Core.Type.Array.
+module Test.Copilot.Core.Type.Array where
+
+-- External imports
+import Data.Int                             (Int64)
+import Data.Proxy                           (Proxy (..))
+import GHC.TypeNats                         (KnownNat, natVal)
+import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.QuickCheck                      (Gen, Property, arbitrary, forAll,
+                                             vectorOf)
+
+-- Internal imports: library modules being tested
+import Copilot.Core.Type.Array (Array, array, arrayelems, flatten, size)
+
+-- | All unit tests for copilot-core:Copilot.Core.Array.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Core.Type.Array"
+    [ testProperty "arrayElems . array (identity; 0)"
+        (testArrayElemsLeft (Proxy :: Proxy 0))
+    , testProperty "arrayElems . array (identity; 5)"
+        (testArrayElemsLeft (Proxy :: Proxy 5))
+    , testProperty "arrayElems . array (identity; 200)"
+        (testArrayElemsLeft (Proxy :: Proxy 200))
+    , testProperty "arrayFlatten . array (identity; 0)"
+        (testArrayFlattenLeft (Proxy :: Proxy 0))
+    , testProperty "arrayFlatten . array (identity; 1)"
+        (testArrayFlattenLeft (Proxy :: Proxy 1))
+    , testProperty "arrayFlatten . array (identity; 2)"
+        (testArrayFlattenLeft (Proxy :: Proxy 2))
+    , testProperty "arrayFlatten . array (identity; 22)"
+        (testArrayFlattenLeft (Proxy :: Proxy 22))
+    , testProperty "arrayFlatten . array (identity; 50)"
+        (testArrayFlattenLeft (Proxy :: Proxy 50))
+    , testProperty "arrayFlatten . array (identity; nested; nested; 2x6)"
+        (testArrayFlattenNestedLeft (Proxy :: Proxy 2) (Proxy :: Proxy 6))
+    , testProperty "arrayFlatten . array (identity; nested; nested; 10x2)"
+        (testArrayFlattenNestedLeft (Proxy :: Proxy 10) (Proxy :: Proxy 2))
+    , testProperty "arrayFlatten . array (identity; nested; nested; 38x20)"
+        (testArrayFlattenNestedLeft (Proxy :: Proxy 38) (Proxy :: Proxy 20))
+    , testProperty "arrayFlatten . array (identity; nested; nested; 125x100)"
+        (testArrayFlattenNestedLeft (Proxy :: Proxy 125) (Proxy :: Proxy 100))
+    , testProperty "arraySize . array (identity; 0)"
+        (testArraySizeLeft (Proxy :: Proxy 0))
+    , testProperty "arraySize . array (identity; 45)"
+        (testArraySizeLeft (Proxy :: Proxy 45))
+    , testProperty "arraySize . array (identity; 100)"
+        (testArraySizeLeft (Proxy :: Proxy 100))
+    ]
+
+-- * Individual tests
+
+-- | Test that building an array from a list and extracting the elements with
+-- the function 'arrayelems' will result in the same list.
+testArrayElemsLeft :: forall n . KnownNat n => Proxy n -> Property
+testArrayElemsLeft len =
+    forAll xsInt64 $ \ls ->
+      let array' :: Array n Int64
+          array' = array ls
+      in arrayelems array' == ls
+
+  where
+
+    -- Generator for lists of Int64 of known length.
+    xsInt64 :: Gen [Int64]
+    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary
+
+-- | Test that building an array from a list and extracting the elements with
+-- the function 'flatten' will result in the same list.
+--
+-- This test tests only plain arrays (no nesting).
+testArrayFlattenLeft :: forall n . KnownNat n => Proxy n -> Property
+testArrayFlattenLeft len =
+    forAll xsInt64 $ \ls ->
+      let array' :: Array n Int64
+          array' = array ls
+      in flatten array' == ls
+
+  where
+
+    -- Generator for lists of Int64 of known length.
+    xsInt64 :: Gen [Int64]
+    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary
+
+-- | Test that building a nested array of a known size and extracting the
+-- elements with the function 'flatten' will result in a list with a size that
+-- is the product of the sizes provided.
+testArrayFlattenNestedLeft :: forall n1 n2
+                           .  (KnownNat n1, KnownNat n2)
+                           => Proxy n1
+                           -> Proxy n2
+                           -> Property
+testArrayFlattenNestedLeft len1 len2 =
+    forAll xsArrays $ \array' ->
+      length (flatten array' :: [Int64]) == expectedSize
+
+  where
+
+    -- Expected size of the matrix / array.
+    expectedSize :: Int
+    expectedSize = fromIntegral $ natVal len1 * natVal len2
+
+    -- Generator for nested matrices of Int64 of known size.
+    xsArrays :: Gen (Array n1 (Array n2 Int64))
+    xsArrays =
+      array <$> vectorOf (fromIntegral (natVal len1)) xsArrayInt64
+
+    -- Generator for arrays of Int64 of known length.
+    xsArrayInt64 :: Gen (Array n2 Int64)
+    xsArrayInt64 = array <$> xsInt64
+
+    -- Generator for lists of Int64 of known length.
+    xsInt64 :: Gen [Int64]
+    xsInt64 = vectorOf (fromIntegral (natVal len2)) arbitrary
+
+-- | Test that building an array from a list and calculating the size will
+-- return the length of the list.
+testArraySizeLeft :: forall n . KnownNat n => Proxy n -> Property
+testArraySizeLeft len =
+    forAll xsInt64 $ \ls ->
+      let array' :: Array n Int64
+          array' = array ls
+      in size array' == length ls
+
+  where
+
+    -- Generator for lists of Int64 of known length.
+    xsInt64 :: Gen [Int64]
+    xsInt64 = vectorOf (fromIntegral (natVal len)) arbitrary
diff --git a/tests/Test/Copilot/Core/Type/Dynamic.hs b/tests/Test/Copilot/Core/Type/Dynamic.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Core/Type/Dynamic.hs
@@ -0,0 +1,48 @@
+{-# 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
diff --git a/tests/Test/Copilot/Core/Type/Show.hs b/tests/Test/Copilot/Core/Type/Show.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Copilot/Core/Type/Show.hs
@@ -0,0 +1,34 @@
+-- | Test copilot-core:Copilot.Core.Type.Show.
+module Test.Copilot.Core.Type.Show where
+
+-- External imports
+import Test.Framework                       (Test, testGroup)
+import Test.Framework.Providers.QuickCheck2 (testProperty)
+import Test.QuickCheck                      (Arbitrary, Property, property)
+import Text.Read                            (readMaybe)
+
+-- Internal imports: library modules being tested
+import Copilot.Core.Type      (Type (Double, Float, Int16, Int32, Int64))
+import Copilot.Core.Type.Show (ShowType (Haskell), showWithType)
+
+-- | All unit tests for copilot-core:Copilot.Core.Type.Show.
+tests :: Test.Framework.Test
+tests =
+  testGroup "Copilot.Core.Type.Show"
+    [ testProperty "read . showWithType == identity (Int16)"
+        (testShowRead Int16)
+    , testProperty "read . showWithType == identity (Int32)"
+        (testShowRead Int32)
+    , testProperty "read . showWithType == identity (Int64)"
+        (testShowRead Int64)
+    , testProperty "read . showWithType == identity (Float)"
+        (testShowRead Float)
+    , testProperty "read . showWithType == identity (Double)"
+        (testShowRead Double)
+    ]
+
+-- | Test that showing a value with 'showWithType' and reading it back results
+-- in the same value.
+testShowRead :: (Arbitrary a, Eq a, Read a) => Type a -> a -> Property
+testShowRead t v = property $
+  Just v == readMaybe (showWithType Haskell t v)
diff --git a/tests/Test/Extra.hs b/tests/Test/Extra.hs
new file mode 100644
--- /dev/null
+++ b/tests/Test/Extra.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+-- | Auxiliary testing helper functions.
+module Test.Extra where
+
+-- External imports
+import Control.Arrow     ((***))
+import Control.Exception (SomeException, catch)
+
+-- * Detecting exceptions
+
+-- | Test that a computation terminates without throwing an exception.
+--
+-- Returns 'True' if the computation can be completed without an exception,
+-- and 'False' otherwise.
+withoutException :: IO a -> IO Bool
+withoutException e =
+  catch (e >> return True)
+        (\(_ :: SomeException) -> return False)
+
+-- * Function application
+
+-- | Apply a tuple with two functions to a tuple of arguments.
+apply1 :: (a1 -> b1, a2 -> b2) -- ^ Pair with functions
+       -> (a1, a2)             -- ^ Pair with arguments
+       -> (b1, b2)             -- ^ Pair with results
+apply1 = uncurry (***)
+
+-- | Apply a tuple with two functions on two arguments to their tupled
+-- arguments.
+apply2 :: (a1 -> b1 -> c1, a2 -> b2 -> c2) -- ^ Pair with functions
+       -> (a1, a2)                         -- ^ Pair with first arguments
+       -> (b1, b2)                         -- ^ Pair with second arguments
+       -> (c1, c2)                         -- ^ Pair with results
+apply2 fs = apply1 . apply1 fs
+
+-- | Apply a tuple with two functions on three arguments to their tupled
+-- arguments.
+apply3 :: (a1 -> b1 -> c1 -> d1, a2 -> b2 -> c2 -> d2)
+                    -- ^ Pair with functions
+       -> (a1, a2)  -- ^ Pair with first arguments
+       -> (b1, b2)  -- ^ Pair with second arguments
+       -> (c1, c2)  -- ^ Pair with third arguments
+       -> (d1, d2)  -- ^ Pair with results
+apply3 fs = apply2 . apply1 fs