diff --git a/semantic.cabal b/semantic.cabal
index 01224b601..47b8a8e30 100644
--- a/semantic.cabal
+++ b/semantic.cabal
@@ -47,10 +47,10 @@ library
                      , Data.Abstract.Environment
                      , Data.Abstract.Evaluatable
                      , Data.Abstract.FreeVariables
+                     , Data.Abstract.Heap
                      , Data.Abstract.Live
                      , Data.Abstract.ModuleTable
                      , Data.Abstract.Number
-                     , Data.Abstract.Store
                      , Data.Abstract.Type
                      , Data.Abstract.Value
                      -- General datatype definitions & generic algorithms
diff --git a/src/Analysis/Abstract/Caching.hs b/src/Analysis/Abstract/Caching.hs
index 09d45f4a7..77b6c7d2b 100644
--- a/src/Analysis/Abstract/Caching.hs
+++ b/src/Analysis/Abstract/Caching.hs
@@ -6,9 +6,8 @@ module Analysis.Abstract.Caching
 import Control.Abstract.Analysis
 import Data.Abstract.Cache
 import Data.Abstract.Configuration
-import Data.Abstract.Store
+import Data.Abstract.Heap
 import Data.Abstract.Value
-import Data.Monoid (Alt (..))
 import Prologue
 
 -- | The effects necessary for caching analyses.
@@ -26,22 +25,23 @@ type CacheFor term value = Cache (LocationFor value) term value
 newtype Caching m term value (effects :: [* -> *]) a = Caching (m term value effects a)
   deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
 
+deriving instance MonadControl term (m term value effects) => MonadControl term (Caching m term value effects)
 deriving instance MonadEnvironment value (m term value effects) => MonadEnvironment value (Caching m term value effects)
-deriving instance MonadStore value (m term value effects) => MonadStore value (Caching m term value effects)
+deriving instance MonadHeap value (m term value effects) => MonadHeap value (Caching m term value effects)
 deriving instance MonadModuleTable term value (m term value effects) => MonadModuleTable term value (Caching m term value effects)
 deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (Caching m term value effects)
 
 -- | Functionality used to perform caching analysis. This is not exported, and exists primarily for organizational reasons.
 class MonadEvaluator term value m => MonadCaching term value m where
   -- | Look up the set of values for a given configuration in the in-cache.
-  consultOracle :: ConfigurationFor term value -> m (Set (value, StoreFor value))
+  consultOracle :: ConfigurationFor term value -> m (Set (value, HeapFor value))
   -- | Run an action with the given in-cache.
   withOracle :: CacheFor term value -> m a -> m a
 
   -- | Look up the set of values for a given configuration in the out-cache.
-  lookupCache :: ConfigurationFor term value -> m (Maybe (Set (value, StoreFor value)))
-  -- | Run an action, caching its result and 'Store' under the given configuration.
-  caching :: ConfigurationFor term value -> Set (value, StoreFor value) -> m value -> m value
+  lookupCache :: ConfigurationFor term value -> m (Maybe (Set (value, HeapFor value)))
+  -- | Run an action, caching its result and 'Heap' under the given configuration.
+  caching :: ConfigurationFor term value -> Set (value, HeapFor value) -> m value -> m value
 
   -- | Run an action starting from an empty out-cache, and return the out-cache afterwards.
   isolateCache :: m a -> m (CacheFor term value)
@@ -61,7 +61,7 @@ instance ( Effectful (m term value)
   lookupCache configuration = raise (cacheLookup configuration <$> get)
   caching configuration values action = do
     raise (modify (cacheSet configuration values))
-    result <- (,) <$> action <*> getStore
+    result <- (,) <$> action <*> getHeap
     raise (modify (cacheInsert configuration result))
     pure (fst result)
 
@@ -97,7 +97,7 @@ instance ( Corecursive term
     c <- getConfiguration e
     -- Convergence here is predicated upon an Eq instance, not α-equivalence
     cache <- converge (\ prevCache -> isolateCache $ do
-      putStore (configurationStore c)
+      putHeap (configurationHeap c)
       -- We need to reset fresh generation so that this invocation converges.
       reset 0
       -- This is subtle: though the calling context supports nondeterminism, we want
@@ -124,5 +124,5 @@ converge f = loop
             loop x'
 
 -- | Nondeterministically write each of a collection of stores & return their associated results.
-scatter :: (Alternative m, Foldable t, MonadEvaluator term value m) => t (a, Store (LocationFor value) value) -> m a
-scatter = getAlt . foldMap (\ (value, store') -> Alt (putStore store' *> pure value))
+scatter :: (Alternative m, Foldable t, MonadEvaluator term value m) => t (a, Heap (LocationFor value) value) -> m a
+scatter = foldMapA (\ (value, heap') -> putHeap heap' *> pure value)
diff --git a/src/Analysis/Abstract/Collecting.hs b/src/Analysis/Abstract/Collecting.hs
index e6bb87d9c..6399b795e 100644
--- a/src/Analysis/Abstract/Collecting.hs
+++ b/src/Analysis/Abstract/Collecting.hs
@@ -6,16 +6,17 @@ module Analysis.Abstract.Collecting
 import Control.Abstract.Analysis
 import Data.Abstract.Address
 import Data.Abstract.Configuration
+import Data.Abstract.Heap
 import Data.Abstract.Live
-import Data.Abstract.Store
 import Data.Abstract.Value
 import Prologue
 
 newtype Collecting m term value (effects :: [* -> *]) a = Collecting (m term value effects a)
   deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
 
+deriving instance MonadControl term (m term value effects) => MonadControl term (Collecting m term value effects)
 deriving instance MonadEnvironment value (m term value effects) => MonadEnvironment value (Collecting m term value effects)
-deriving instance MonadStore value (m term value effects) => MonadStore value (Collecting m term value effects)
+deriving instance MonadHeap value (m term value effects) => MonadHeap value (Collecting m term value effects)
 deriving instance MonadModuleTable term value (m term value effects) => MonadModuleTable term value (Collecting m term value effects)
 
 instance ( Effectful (m term value)
@@ -23,7 +24,7 @@ instance ( Effectful (m term value)
          , MonadEvaluator term value (m term value effects)
          )
          => MonadEvaluator term value (Collecting m term value effects) where
-  getConfiguration term = Configuration term <$> askRoots <*> askLocalEnv <*> getStore
+  getConfiguration term = Configuration term <$> askRoots <*> askLocalEnv <*> getHeap
 
 
 instance ( Effectful (m term value)
@@ -42,7 +43,7 @@ instance ( Effectful (m term value)
   analyzeTerm term = do
     roots <- askRoots
     v <- liftAnalyze analyzeTerm term
-    modifyStore (gc (roots <> valueRoots v))
+    modifyHeap (gc (roots <> valueRoots v))
     pure v
 
 
@@ -55,27 +56,27 @@ askRoots = raise ask
 -- extraRoots roots = raise . local (<> roots) . lower
 
 
--- | Collect any addresses in the store not rooted in or reachable from the given 'Live' set.
+-- | Collect any addresses in the heap not rooted in or reachable from the given 'Live' set.
 gc :: ( Ord (LocationFor value)
       , Foldable (Cell (LocationFor value))
       , ValueRoots value
       )
-   => LiveFor value  -- ^ The set of addresses to consider rooted.
-   -> StoreFor value -- ^ A store to collect unreachable addresses within.
-   -> StoreFor value -- ^ A garbage-collected store.
-gc roots store = storeRestrict store (reachable roots store)
+   => LiveFor value -- ^ The set of addresses to consider rooted.
+   -> HeapFor value -- ^ A heap to collect unreachable addresses within.
+   -> HeapFor value -- ^ A garbage-collected heap.
+gc roots heap = heapRestrict heap (reachable roots heap)
 
--- | Compute the set of addresses reachable from a given root set in a given store.
+-- | Compute the set of addresses reachable from a given root set in a given heap.
 reachable :: ( Ord (LocationFor value)
              , Foldable (Cell (LocationFor value))
              , ValueRoots value
              )
-          => LiveFor value  -- ^ The set of root addresses.
-          -> StoreFor value -- ^ The store to trace addresses through.
-          -> LiveFor value  -- ^ The set of addresses reachable from the root set.
-reachable roots store = go mempty roots
+          => LiveFor value -- ^ The set of root addresses.
+          -> HeapFor value -- ^ The heap to trace addresses through.
+          -> LiveFor value -- ^ The set of addresses reachable from the root set.
+reachable roots heap = go mempty roots
   where go seen set = case liveSplit set of
           Nothing -> seen
-          Just (a, as) -> go (liveInsert a seen) (case storeLookupAll a store of
+          Just (a, as) -> go (liveInsert a seen) (case heapLookupAll a heap of
             Just values -> liveDifference (foldr ((<>) . valueRoots) mempty values <> as) seen
             _           -> seen)
diff --git a/src/Analysis/Abstract/Dead.hs b/src/Analysis/Abstract/Dead.hs
index c3cb2c4fc..cf004925d 100644
--- a/src/Analysis/Abstract/Dead.hs
+++ b/src/Analysis/Abstract/Dead.hs
@@ -12,8 +12,9 @@ import Prologue
 newtype DeadCode m term value (effects :: [* -> *]) a = DeadCode (m term value effects a)
   deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
 
+deriving instance MonadControl term (m term value effects) => MonadControl term (DeadCode m term value effects)
 deriving instance MonadEnvironment value (m term value effects) => MonadEnvironment value (DeadCode m term value effects)
-deriving instance MonadStore value (m term value effects) => MonadStore value (DeadCode m term value effects)
+deriving instance MonadHeap value (m term value effects) => MonadHeap value (DeadCode m term value effects)
 deriving instance MonadModuleTable term value (m term value effects) => MonadModuleTable term value (DeadCode m term value effects)
 deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (DeadCode m term value effects)
 
diff --git a/src/Analysis/Abstract/Evaluating.hs b/src/Analysis/Abstract/Evaluating.hs
index a25887cbd..8f131fffd 100644
--- a/src/Analysis/Abstract/Evaluating.hs
+++ b/src/Analysis/Abstract/Evaluating.hs
@@ -18,6 +18,7 @@ import Data.Abstract.Address
 import Data.Abstract.ModuleTable
 import Data.Abstract.Value
 import Data.Blob
+import qualified Data.IntMap as IntMap
 import Data.Language
 import Data.List.Split (splitWhen)
 import Prelude hiding (fail)
@@ -32,7 +33,7 @@ evaluate :: forall value term effects
             , Evaluatable (Base term)
             , FreeVariables term
             , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-            , MonadValue term value (Evaluating term value effects)
+            , MonadValue value (Evaluating term value effects)
             , Recursive term
             )
          => term
@@ -45,7 +46,7 @@ evaluates :: forall value term effects
              , Evaluatable (Base term)
              , FreeVariables term
              , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-             , MonadValue term value (Evaluating term value effects)
+             , MonadValue value (Evaluating term value effects)
              , Recursive term
              )
           => [(Blob, term)] -- List of (blob, term) pairs that make up the program to be evaluated
@@ -70,7 +71,6 @@ withModules Blob{..} pairs = localModuleTable (const moduleTable)
 newtype Evaluating term value effects a = Evaluating (Eff effects a)
   deriving (Applicative, Functor, Effectful, Monad)
 
-
 deriving instance Member Fail      effects => MonadFail   (Evaluating term value effects)
 deriving instance Member Fresh     effects => MonadFresh  (Evaluating term value effects)
 deriving instance Member NonDetEff effects => Alternative (Evaluating term value effects)
@@ -81,13 +81,23 @@ type EvaluatingEffects term value
   = '[ Fail                                        -- Failure with an error message
      , Reader (EnvironmentFor value)               -- Local environment (e.g. binding over a closure)
      , State  (EnvironmentFor value)               -- Global (imperative) environment
-     , State  (StoreFor value)                     -- The heap
+     , State  (HeapFor value)                     -- The heap
      , Reader (ModuleTable [term])                 -- Cache of unevaluated modules
      , State  (ModuleTable (EnvironmentFor value)) -- Cache of evaluated modules
 
      , State (Map Name (Name, Maybe (Address (LocationFor value) value))) -- Set of exports
+     , State (IntMap.IntMap term) -- For jumps
      ]
 
+instance Members '[Fail, State (IntMap.IntMap term)] effects => MonadControl term (Evaluating term value effects) where
+  label term = do
+    m <- raise get
+    let i = IntMap.size m
+    raise (put (IntMap.insert i term m))
+    pure i
+
+  goto label = IntMap.lookup label <$> raise get >>= maybe (fail ("unknown label: " <> show label)) pure
+
 instance Members '[State (Map Name (Name, Maybe (Address (LocationFor value) value))), Reader (EnvironmentFor value), State (EnvironmentFor value)] effects => MonadEnvironment value (Evaluating term value effects) where
   getGlobalEnv = raise get
   putGlobalEnv = raise . put
@@ -100,9 +110,9 @@ instance Members '[State (Map Name (Name, Maybe (Address (LocationFor value) val
   askLocalEnv = raise ask
   localEnv f a = raise (local f (lower a))
 
-instance Member (State (StoreFor value)) effects => MonadStore value (Evaluating term value effects) where
-  getStore = raise get
-  putStore = raise . put
+instance Member (State (HeapFor value)) effects => MonadHeap value (Evaluating term value effects) where
+  getHeap = raise get
+  putHeap = raise . put
 
 instance Members '[Reader (ModuleTable [term]), State (ModuleTable (EnvironmentFor value))] effects => MonadModuleTable term value (Evaluating term value effects) where
   getModuleTable = raise get
@@ -112,13 +122,13 @@ instance Members '[Reader (ModuleTable [term]), State (ModuleTable (EnvironmentF
   localModuleTable f a = raise (local f (lower a))
 
 instance Members (EvaluatingEffects term value) effects => MonadEvaluator term value (Evaluating term value effects) where
-  getConfiguration term = Configuration term mempty <$> askLocalEnv <*> getStore
+  getConfiguration term = Configuration term mempty <$> askLocalEnv <*> getHeap
 
 instance ( Evaluatable (Base term)
          , FreeVariables term
          , Members (EvaluatingEffects term value) effects
          , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-         , MonadValue term value (Evaluating term value effects)
+         , MonadValue value (Evaluating term value effects)
          , Recursive term
          )
          => MonadAnalysis term value (Evaluating term value effects) where
diff --git a/src/Analysis/Abstract/Tracing.hs b/src/Analysis/Abstract/Tracing.hs
index d7b18ac97..d21f8b3c3 100644
--- a/src/Analysis/Abstract/Tracing.hs
+++ b/src/Analysis/Abstract/Tracing.hs
@@ -17,8 +17,9 @@ import Prologue hiding (trace)
 newtype Tracing (trace :: * -> *) m term value (effects :: [* -> *]) a = Tracing (m term value effects a)
   deriving (Alternative, Applicative, Functor, Effectful, Monad, MonadFail, MonadFresh, MonadNonDet)
 
+deriving instance MonadControl term (m term value effects) => MonadControl term (Tracing trace m term value effects)
 deriving instance MonadEnvironment value (m term value effects) => MonadEnvironment value (Tracing trace m term value effects)
-deriving instance MonadStore value (m term value effects) => MonadStore value (Tracing trace m term value effects)
+deriving instance MonadHeap value (m term value effects) => MonadHeap value (Tracing trace m term value effects)
 deriving instance MonadModuleTable term value (m term value effects) => MonadModuleTable term value (Tracing trace m term value effects)
 deriving instance MonadEvaluator term value (m term value effects) => MonadEvaluator term value (Tracing trace m term value effects)
 
diff --git a/src/Control/Abstract/Addressable.hs b/src/Control/Abstract/Addressable.hs
index d12cac5ba..f96f02a3a 100644
--- a/src/Control/Abstract/Addressable.hs
+++ b/src/Control/Abstract/Addressable.hs
@@ -7,13 +7,13 @@ import Control.Monad ((<=<))
 import Data.Abstract.Address
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
-import Data.Abstract.Store
+import Data.Abstract.Heap
 import Data.Abstract.Value
-import Data.Foldable (asum, toList)
 import Data.Semigroup.Reducer
 import Prelude hiding (fail)
+import Prologue
 
--- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Store.
+-- | Defines 'alloc'ation and 'deref'erencing of 'Address'es in a Heap.
 class (Monad m, Ord l, l ~ LocationFor value, Reducer value (Cell l value)) => MonadAddressable l value m where
   deref :: Address l value -> m value
 
@@ -30,7 +30,7 @@ lookupOrAlloc name = lookupLocalEnv name >>= maybe (alloc name) pure
 
 letrec :: ( MonadAddressable (LocationFor value) value m
           , MonadEnvironment value m
-          , MonadStore value m
+          , MonadHeap value m
           )
        => Name
        -> m value
@@ -45,18 +45,20 @@ letrec name body = do
 -- Instances
 
 -- | 'Precise' locations are always 'alloc'ated a fresh 'Address', and 'deref'erence to the 'Latest' value written.
-instance (MonadFail m, LocationFor value ~ Precise, MonadStore value m) => MonadAddressable Precise value m where
-  deref = maybe uninitializedAddress (pure . unLatest) <=< flip fmap getStore . storeLookup
-    where
-      -- | Fail with a message denoting an uninitialized address (i.e. one which was 'alloc'ated, but never 'assign'ed a value before being 'deref'erenced).
-      uninitializedAddress :: MonadFail m => m a
-      uninitializedAddress = fail "uninitialized address"
-
-  alloc _ = fmap (Address . Precise . storeSize) getStore
+instance (MonadFail m, LocationFor value ~ Precise, MonadHeap value m) => MonadAddressable Precise value m where
+  deref = derefWith (pure . unLatest)
+  alloc _ = fmap (Address . Precise . heapSize) getHeap
 
 
 -- | 'Monovariant' locations 'alloc'ate one 'Address' per unique variable name, and 'deref'erence once per stored value, nondeterministically.
-instance (Alternative m, LocationFor value ~ Monovariant, MonadStore value m, Ord value) => MonadAddressable Monovariant value m where
-  deref = asum . maybe [] (map pure . toList) <=< flip fmap getStore . storeLookup
-
+instance (Alternative m, LocationFor value ~ Monovariant, MonadFail m, MonadHeap value m, Ord value) => MonadAddressable Monovariant value m where
+  deref = derefWith (foldMapA pure)
   alloc = pure . Address . Monovariant
+
+-- | Dereference the given 'Address' in the heap, using the supplied function to act on the cell, or failing if the address is uninitialized.
+derefWith :: (MonadFail m, MonadHeap value m, Ord (LocationFor value)) => (CellFor value -> m a) -> Address (LocationFor value) value -> m a
+derefWith with = maybe uninitializedAddress with <=< lookupHeap
+
+-- | Fail with a message denoting an uninitialized address (i.e. one which was 'alloc'ated, but never 'assign'ed a value before being 'deref'erenced).
+uninitializedAddress :: MonadFail m => m a
+uninitializedAddress = fail "uninitialized address"
diff --git a/src/Control/Abstract/Evaluator.hs b/src/Control/Abstract/Evaluator.hs
index 685a18707..6e707d22b 100644
--- a/src/Control/Abstract/Evaluator.hs
+++ b/src/Control/Abstract/Evaluator.hs
@@ -3,19 +3,21 @@ module Control.Abstract.Evaluator
 ( MonadEvaluator(..)
 , MonadEnvironment(..)
 , modifyGlobalEnv
-, MonadStore(..)
-, modifyStore
+, MonadHeap(..)
+, modifyHeap
+, lookupHeap
 , assign
 , MonadModuleTable(..)
 , modifyModuleTable
+, MonadControl(..)
 ) where
 
 import Data.Abstract.Address
 import Data.Abstract.Configuration
 import Data.Abstract.Environment
 import Data.Abstract.FreeVariables
+import Data.Abstract.Heap
 import Data.Abstract.ModuleTable
-import Data.Abstract.Store
 import Data.Abstract.Value
 import Data.Semigroup.Reducer
 import Prelude hiding (fail)
@@ -27,10 +29,11 @@ import Prologue
 --   - environments binding names to addresses
 --   - a heap mapping addresses to (possibly sets of) values
 --   - tables of modules available for import
-class ( MonadEnvironment value m
+class ( MonadControl term m
+      , MonadEnvironment value m
       , MonadFail m
       , MonadModuleTable term value m
-      , MonadStore value m
+      , MonadHeap value m
       )
       => MonadEvaluator term value m | m -> term, m -> value where
   -- | Get the current 'Configuration' with a passed-in term.
@@ -74,27 +77,31 @@ modifyGlobalEnv f = do
 
 
 -- | A 'Monad' abstracting a heap of values.
-class Monad m => MonadStore value m | m -> value where
+class Monad m => MonadHeap value m | m -> value where
   -- | Retrieve the heap.
-  getStore :: m (StoreFor value)
+  getHeap :: m (HeapFor value)
   -- | Set the heap.
-  putStore :: StoreFor value -> m ()
+  putHeap :: HeapFor value -> m ()
 
 -- | Update the heap.
-modifyStore :: MonadStore value m => (StoreFor value -> StoreFor value) -> m ()
-modifyStore f = do
-  s <- getStore
-  putStore $! f s
+modifyHeap :: MonadHeap value m => (HeapFor value -> HeapFor value) -> m ()
+modifyHeap f = do
+  s <- getHeap
+  putHeap $! f s
+
+-- | Look up the cell for the given 'Address' in the 'Heap'.
+lookupHeap :: (MonadHeap value m, Ord (LocationFor value)) => Address (LocationFor value) value -> m (Maybe (CellFor value))
+lookupHeap = flip fmap getHeap . heapLookup
 
 -- | Write a value to the given 'Address' in the 'Store'.
 assign :: ( Ord (LocationFor value)
-          , MonadStore value m
+          , MonadHeap value m
           , Reducer value (CellFor value)
           )
        => Address (LocationFor value) value
        -> value
        -> m ()
-assign address = modifyStore . storeInsert address
+assign address = modifyHeap . heapInsert address
 
 
 -- | A 'Monad' abstracting tables of modules available for import.
@@ -114,3 +121,13 @@ modifyModuleTable :: MonadModuleTable term value m => (ModuleTable (EnvironmentF
 modifyModuleTable f = do
   table <- getModuleTable
   putModuleTable $! f table
+
+
+-- | A 'Monad' abstracting jumps in imperative control.
+class Monad m => MonadControl term m where
+  -- | Allocate a 'Label' for the given @term@.
+  --
+  --   Labels must be allocated before being jumped to with 'goto', but are suitable for nonlocal jumps; thus, they can be used to implement coroutines, exception handling, call with current continuation, and other esoteric control mechanisms.
+  label :: term -> m Label
+  -- | “Jump” to a previously-allocated 'Label' (retrieving the @term@ at which it points, which can then be evaluated in e.g. a 'MonadAnalysis' instance).
+  goto :: Label -> m term
diff --git a/src/Control/Abstract/Value.hs b/src/Control/Abstract/Value.hs
index ad157bd0e..afb01920b 100644
--- a/src/Control/Abstract/Value.hs
+++ b/src/Control/Abstract/Value.hs
@@ -26,7 +26,7 @@ data Comparator
 -- | A 'Monad' abstracting the evaluation of (and under) binding constructs (functions, methods, etc).
 --
 --   This allows us to abstract the choice of whether to evaluate under binders for different value types.
-class (MonadAnalysis term value m, Show value) => MonadValue term value m where
+class (Monad m, Show value) => MonadValue value m where
   -- | Construct an abstract unit value.
   --   TODO: This might be the same as the empty tuple for some value types
   unit :: m value
@@ -74,7 +74,7 @@ class (MonadAnalysis term value m, Show value) => MonadValue term value m where
   ifthenelse :: value -> m a -> m a -> m a
 
   -- | Evaluate an abstraction (a binder like a lambda or method definition).
-  abstract :: [Name] -> Subterm term (m value) -> m value
+  abstract :: (FreeVariables term, MonadControl term m) => [Name] -> Subterm term (m value) -> m value
   -- | Evaluate an application (like a function call).
   apply :: value -> [m value] -> m value
 
@@ -84,10 +84,10 @@ class (MonadAnalysis term value m, Show value) => MonadValue term value m where
   loop :: (m value -> m value) -> m value
 
 -- | Attempt to extract a 'Prelude.Bool' from a given value.
-toBool :: MonadValue term value m => value -> m Bool
+toBool :: MonadValue value m => value -> m Bool
 toBool v = ifthenelse v (pure True) (pure False)
 
-forLoop :: MonadValue term value m
+forLoop :: (MonadEnvironment value m, MonadValue value m)
         => m value -- | Initial statement
         -> m value -- | Condition
         -> m value -- | Increment/stepper
@@ -99,7 +99,7 @@ forLoop initial cond step body = do
   localEnv (mappend env) (while cond (body *> step))
 
 -- | The fundamental looping primitive, built on top of ifthenelse.
-while :: MonadValue term value m
+while :: MonadValue value m
       => m value
       -> m value
       -> m value
@@ -108,7 +108,7 @@ while cond body = loop $ \ continue -> do
   ifthenelse this (body *> continue) unit
 
 -- | Do-while loop, built on top of while.
-doWhile :: MonadValue term value m
+doWhile :: MonadValue value m
         => m value
         -> m value
         -> m value
@@ -117,13 +117,12 @@ doWhile body cond = loop $ \ continue -> body *> do
   ifthenelse this continue unit
 
 -- | Construct a 'Value' wrapping the value arguments (if any).
-instance ( FreeVariables term
-         , MonadAddressable location (Value location term) m
-         , MonadAnalysis term (Value location term) m
+instance ( Monad m
+         , MonadAddressable location Value m
+         , MonadAnalysis term Value m
          , Show location
-         , Show term
          )
-         => MonadValue term (Value location term) m where
+         => MonadValue Value m where
 
   unit     = pure . injValue $ Value.Unit
   integer  = pure . injValue . Value.Integer . Number.Integer
@@ -160,7 +159,7 @@ instance ( FreeVariables term
     | otherwise = fail ("Invalid operands to liftNumeric2: " <> show pair)
       where
         -- Dispatch whatever's contained inside a 'SomeNumber' to its appropriate 'MonadValue' ctor
-        specialize :: MonadValue term value m => SomeNumber -> m value
+        specialize :: MonadValue value m => SomeNumber -> m value
         specialize (SomeNumber (Number.Integer i)) = integer i
         specialize (SomeNumber (Ratio r))          = rational r
         specialize (SomeNumber (Decimal d))        = float d
@@ -178,7 +177,7 @@ instance ( FreeVariables term
       where
         -- Explicit type signature is necessary here because we're passing all sorts of things
         -- to these comparison functions.
-        go :: (Ord a, MonadValue term value m) => a -> a -> m value
+        go :: (Ord a, MonadValue value m) => a -> a -> m value
         go l r = case comparator of
           Concrete f  -> boolean (f l r)
           Generalized -> integer (orderingToInt (compare l r))
@@ -189,21 +188,23 @@ instance ( FreeVariables term
 
         pair = (left, right)
 
-  abstract names (Subterm body _) = injValue . Closure names body . bindEnv (foldr Set.delete (freeVariables body) names) <$> askLocalEnv
+  abstract names (Subterm body _) = do
+    l <- label body
+    injValue . Closure names l . bindEnv (foldr Set.delete (freeVariables body) names) <$> askLocalEnv
 
   apply op params = do
-    Closure names body env <- maybe (fail ("expected a closure, got: " <> show op)) pure (prjValue op)
+    Closure names label env <- maybe (fail ("expected a closure, got: " <> show op)) pure (prjValue op)
     bindings <- foldr (\ (name, param) rest -> do
       v <- param
       a <- alloc name
       assign a v
       envInsert name a <$> rest) (pure env) (zip names params)
-    localEnv (mappend bindings) (evaluateTerm body)
+    localEnv (mappend bindings) (goto label >>= evaluateTerm)
 
   loop = fix
 
--- | Discard the value arguments (if any), constructing a 'Type.Type' instead.
-instance (Alternative m, MonadAnalysis term Type m, MonadFresh m) => MonadValue term Type m where
+-- | Discard the value arguments (if any), constructing a 'Type' instead.
+instance (Alternative m, MonadEnvironment Type m, MonadFail m, MonadFresh m, MonadHeap Type m) => MonadValue Type m where
   abstract names (Subterm _ body) = do
     (env, tvars) <- foldr (\ name rest -> do
       a <- alloc name
diff --git a/src/Data/Abstract/Cache.hs b/src/Data/Abstract/Cache.hs
index f7c9550b1..34660dcb2 100644
--- a/src/Data/Abstract/Cache.hs
+++ b/src/Data/Abstract/Cache.hs
@@ -3,30 +3,30 @@ module Data.Abstract.Cache where
 
 import Data.Abstract.Address
 import Data.Abstract.Configuration
-import Data.Abstract.Store
+import Data.Abstract.Heap
 import Data.Map.Monoidal as Monoidal
 import Prologue
 
--- | A map of 'Configuration's to 'Set's of resulting values & 'Store's.
-newtype Cache l t v = Cache { unCache :: Monoidal.Map (Configuration l t v) (Set (v, Store l v)) }
+-- | A map of 'Configuration's to 'Set's of resulting values & 'Heap's.
+newtype Cache l t v = Cache { unCache :: Monoidal.Map (Configuration l t v) (Set (v, Heap l v)) }
 
 deriving instance (Eq l, Eq t, Eq v, Eq (Cell l v)) => Eq (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Ord (Cache l t v)
 deriving instance (Show l, Show t, Show v, Show (Cell l v)) => Show (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Semigroup (Cache l t v)
 deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Monoid (Cache l t v)
-deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Reducer (Configuration l t v, (v, Store l v)) (Cache l t v)
+deriving instance (Ord l, Ord t, Ord v, Ord (Cell l v)) => Reducer (Configuration l t v, (v, Heap l v)) (Cache l t v)
 
--- | Look up the resulting value & 'Store' for a given 'Configuration'.
-cacheLookup :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Cache l t v -> Maybe (Set (v, Store l v))
+-- | Look up the resulting value & 'Heap' for a given 'Configuration'.
+cacheLookup :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Cache l t v -> Maybe (Set (v, Heap l v))
 cacheLookup key = Monoidal.lookup key . unCache
 
--- | Set the resulting value & 'Store' for a given 'Configuration', overwriting any previous entry.
-cacheSet :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Set (v, Store l v) -> Cache l t v -> Cache l t v
+-- | Set the resulting value & 'Heap' for a given 'Configuration', overwriting any previous entry.
+cacheSet :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> Set (v, Heap l v) -> Cache l t v -> Cache l t v
 cacheSet key value = Cache . Monoidal.insert key value . unCache
 
--- | Insert the resulting value & 'Store' for a given 'Configuration', appending onto any previous entry.
-cacheInsert :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> (v, Store l v) -> Cache l t v -> Cache l t v
+-- | Insert the resulting value & 'Heap' for a given 'Configuration', appending onto any previous entry.
+cacheInsert :: (Ord l, Ord t, Ord v, Ord (Cell l v)) => Configuration l t v -> (v, Heap l v) -> Cache l t v -> Cache l t v
 cacheInsert = curry cons
 
 
@@ -40,7 +40,7 @@ instance (Show l, Show t, Show1 (Cell l)) => Show1 (Cache l t) where
   liftShowsPrec spV slV d = showsUnaryWith (liftShowsPrec2 spKey slKey (liftShowsPrec spPair slPair) (liftShowList spPair slPair)) "Cache" d . unCache
       where spKey = liftShowsPrec spV slV
             slKey = liftShowList spV slV
-            spPair = liftShowsPrec2 spV slV spStore slStore
-            slPair = liftShowList2 spV slV spStore slStore
-            spStore = liftShowsPrec spV slV
-            slStore = liftShowList  spV slV
+            spPair = liftShowsPrec2 spV slV spHeap slHeap
+            slPair = liftShowList2 spV slV spHeap slHeap
+            spHeap = liftShowsPrec spV slV
+            slHeap = liftShowList  spV slV
diff --git a/src/Data/Abstract/Configuration.hs b/src/Data/Abstract/Configuration.hs
index 0028c09f8..f08aef5c5 100644
--- a/src/Data/Abstract/Configuration.hs
+++ b/src/Data/Abstract/Configuration.hs
@@ -3,8 +3,8 @@ module Data.Abstract.Configuration where
 
 import Data.Abstract.Address
 import Data.Abstract.Environment
+import Data.Abstract.Heap
 import Data.Abstract.Live
-import Data.Abstract.Store
 import Data.Abstract.Value
 import Prologue
 
@@ -17,7 +17,7 @@ data Configuration l t v
     { configurationTerm        :: t               -- ^ The “instruction,” i.e. the current term to evaluate.
     , configurationRoots       :: Live l v        -- ^ The set of rooted addresses.
     , configurationEnvironment :: Environment l v -- ^ The environment binding any free variables in 'configurationTerm'.
-    , configurationStore       :: Store l v       -- ^ The store of values.
+    , configurationHeap        :: Heap l v        -- ^ The heap of values.
     }
     deriving (Generic1)
 
diff --git a/src/Data/Abstract/Evaluatable.hs b/src/Data/Abstract/Evaluatable.hs
index 740c49f32..5455f0e0c 100644
--- a/src/Data/Abstract/Evaluatable.hs
+++ b/src/Data/Abstract/Evaluatable.hs
@@ -26,7 +26,7 @@ class Evaluatable constr where
   eval :: ( FreeVariables term
           , MonadAddressable (LocationFor value) value m
           , MonadAnalysis term value m
-          , MonadValue term value m
+          , MonadValue value m
           )
        => SubtermAlgebra constr term (m value)
   default eval :: (MonadFail m, Show1 constr) => SubtermAlgebra constr term (m value)
@@ -60,6 +60,6 @@ instance MonadEnvironment value m => Semigroup (Imperative m a) where
     env <- getGlobalEnv
     localEnv (<> env) b
 
-instance MonadValue term value m => Monoid (Imperative m value) where
+instance (MonadEnvironment value m, MonadValue value m) => Monoid (Imperative m value) where
   mempty = Imperative unit
   mappend = (<>)
diff --git a/src/Data/Abstract/FreeVariables.hs b/src/Data/Abstract/FreeVariables.hs
index 2e73218c2..55138f9e9 100644
--- a/src/Data/Abstract/FreeVariables.hs
+++ b/src/Data/Abstract/FreeVariables.hs
@@ -19,6 +19,11 @@ friendlyName :: Name -> ByteString
 friendlyName xs = intercalate "." (NonEmpty.toList xs)
 
 
+-- | The type of labels.
+--   TODO: This should be rolled into 'Name' and tracked in the environment, both so that we can abstract over labels like any other location, and so that we can garbage collect unreachable labels.
+type Label = Int
+
+
 -- | Types which can contain unbound variables.
 class FreeVariables term where
   -- | The set of free variables in the given value.
diff --git a/src/Data/Abstract/Heap.hs b/src/Data/Abstract/Heap.hs
new file mode 100644
index 000000000..8f02ce79f
--- /dev/null
+++ b/src/Data/Abstract/Heap.hs
@@ -0,0 +1,45 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, UndecidableInstances #-}
+module Data.Abstract.Heap where
+
+import Data.Abstract.Address
+import Data.Abstract.Live
+import qualified Data.Map.Monoidal as Monoidal
+import Data.Semigroup.Reducer
+import Prologue
+
+-- | A map of addresses onto cells holding their values.
+newtype Heap l a = Heap { unStore :: Monoidal.Map l (Cell l a) }
+  deriving (Generic1)
+
+deriving instance (Eq l, Eq (Cell l a)) => Eq (Heap l a)
+deriving instance (Ord l, Ord (Cell l a)) => Ord (Heap l a)
+deriving instance (Show l, Show (Cell l a)) => Show (Heap l a)
+instance (Eq l, Eq1 (Cell l)) => Eq1 (Heap l) where liftEq = genericLiftEq
+instance (Ord l, Ord1 (Cell l)) => Ord1 (Heap l) where liftCompare = genericLiftCompare
+instance (Show l, Show1 (Cell l)) => Show1 (Heap l) where liftShowsPrec = genericLiftShowsPrec
+deriving instance Foldable (Cell l) => Foldable (Heap l)
+deriving instance Functor (Cell l) => Functor (Heap l)
+deriving instance Traversable (Cell l) => Traversable (Heap l)
+deriving instance (Ord l, Semigroup (Cell l a)) => Semigroup (Heap l a)
+deriving instance (Ord l, Semigroup (Cell l a)) => Monoid (Heap l a)
+deriving instance (Ord l, Reducer a (Cell l a)) => Reducer (l, a) (Heap l a)
+
+-- | Look up the cell of values for an 'Address' in a 'Heap', if any.
+heapLookup :: Ord l => Address l a -> Heap l a -> Maybe (Cell l a)
+heapLookup (Address address) = Monoidal.lookup address . unStore
+
+-- | Look up the list of values stored for a given address, if any.
+heapLookupAll :: (Ord l, Foldable (Cell l)) => Address l a -> Heap l a -> Maybe [a]
+heapLookupAll address = fmap toList . heapLookup address
+
+-- | Append a value onto the cell for a given address, inserting a new cell if none existed.
+heapInsert :: (Ord l, Reducer a (Cell l a)) => Address l a -> a -> Heap l a -> Heap l a
+heapInsert (Address address) value = flip snoc (address, value)
+
+-- | The number of addresses extant in a 'Heap'.
+heapSize :: Heap l a -> Int
+heapSize = Monoidal.size . unStore
+
+-- | Restrict a 'Heap' to only those 'Address'es in the given 'Live' set (in essence garbage collecting the rest).
+heapRestrict :: Ord l => Heap l a -> Live l a -> Heap l a
+heapRestrict (Heap m) roots = Heap (Monoidal.filterWithKey (\ address _ -> Address address `liveMember` roots) m)
diff --git a/src/Data/Abstract/Store.hs b/src/Data/Abstract/Store.hs
deleted file mode 100644
index d92847036..000000000
--- a/src/Data/Abstract/Store.hs
+++ /dev/null
@@ -1,45 +0,0 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving, MultiParamTypeClasses, StandaloneDeriving, UndecidableInstances #-}
-module Data.Abstract.Store where
-
-import Data.Abstract.Address
-import Data.Abstract.Live
-import qualified Data.Map.Monoidal as Monoidal
-import Data.Semigroup.Reducer
-import Prologue
-
--- | A map of addresses onto cells holding their values.
-newtype Store l a = Store { unStore :: Monoidal.Map l (Cell l a) }
-  deriving (Generic1)
-
-deriving instance (Eq l, Eq (Cell l a)) => Eq (Store l a)
-deriving instance (Ord l, Ord (Cell l a)) => Ord (Store l a)
-deriving instance (Show l, Show (Cell l a)) => Show (Store l a)
-instance (Eq l, Eq1 (Cell l)) => Eq1 (Store l) where liftEq = genericLiftEq
-instance (Ord l, Ord1 (Cell l)) => Ord1 (Store l) where liftCompare = genericLiftCompare
-instance (Show l, Show1 (Cell l)) => Show1 (Store l) where liftShowsPrec = genericLiftShowsPrec
-deriving instance Foldable (Cell l) => Foldable (Store l)
-deriving instance Functor (Cell l) => Functor (Store l)
-deriving instance Traversable (Cell l) => Traversable (Store l)
-deriving instance (Ord l, Semigroup (Cell l a)) => Semigroup (Store l a)
-deriving instance (Ord l, Semigroup (Cell l a)) => Monoid (Store l a)
-deriving instance (Ord l, Reducer a (Cell l a)) => Reducer (l, a) (Store l a)
-
--- | Look up the cell of values for an 'Address' in a 'Store', if any.
-storeLookup :: Ord l => Address l a -> Store l a -> Maybe (Cell l a)
-storeLookup (Address address) = Monoidal.lookup address . unStore
-
--- | Look up the list of values stored for a given address, if any.
-storeLookupAll :: (Ord l, Foldable (Cell l)) => Address l a -> Store l a -> Maybe [a]
-storeLookupAll address = fmap toList . storeLookup address
-
--- | Append a value onto the cell for a given address, inserting a new cell if none existed.
-storeInsert :: (Ord l, Reducer a (Cell l a)) => Address l a -> a -> Store l a -> Store l a
-storeInsert (Address address) value = flip snoc (address, value)
-
--- | The number of addresses extant in a 'Store'.
-storeSize :: Store l a -> Int
-storeSize = Monoidal.size . unStore
-
--- | Restrict a 'Store' to only those 'Address'es in the given 'Live' set (in essence garbage collecting the rest).
-storeRestrict :: Ord l => Store l a -> Live l a -> Store l a
-storeRestrict (Store m) roots = Store (Monoidal.filterWithKey (\ address _ -> Address address `liveMember` roots) m)
diff --git a/src/Data/Abstract/Value.hs b/src/Data/Abstract/Value.hs
index 3adf88598..d89ba74e6 100644
--- a/src/Data/Abstract/Value.hs
+++ b/src/Data/Abstract/Value.hs
@@ -1,10 +1,10 @@
-{-# LANGUAGE ConstraintKinds, DataKinds, FunctionalDependencies, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, ScopedTypeVariables, TypeFamilies, TypeOperators #-}
+{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators #-}
 module Data.Abstract.Value where
 
 import Data.Abstract.Address
 import Data.Abstract.Environment
-import Data.Abstract.Store
 import Data.Abstract.FreeVariables
+import Data.Abstract.Heap
 import Data.Abstract.Live
 import Data.Abstract.Number
 import qualified Data.Abstract.Type as Type
@@ -13,10 +13,10 @@ import Prologue
 import Prelude hiding (Float, Integer, String, Rational, fail)
 import qualified Prelude
 
-type ValueConstructors location term
+type ValueConstructors
   = '[Array
     , Boolean
-    , Closure location term
+    , Closure
     , Float
     , Integer
     , String
@@ -28,32 +28,32 @@ type ValueConstructors location term
 
 -- | Open union of primitive values that terms can be evaluated to.
 --   Fix by another name.
-newtype Value location term = Value { deValue :: Union (ValueConstructors location term) (Value location term) }
+newtype Value = Value { deValue :: Union ValueConstructors Value }
   deriving (Eq, Show, Ord)
 
 -- | Identical to 'inj', but wraps the resulting sub-entity in a 'Value'.
-injValue :: (f :< ValueConstructors location term) => f (Value location term) -> Value location term
+injValue :: (f :< ValueConstructors) => f Value -> Value
 injValue = Value . inj
 
 -- | Identical to 'prj', but unwraps the argument out of its 'Value' wrapper.
-prjValue :: (f :< ValueConstructors location term) => Value location term -> Maybe (f (Value location term))
+prjValue :: (f :< ValueConstructors) => Value -> Maybe (f Value)
 prjValue = prj . deValue
 
 -- | Convenience function for projecting two values.
-prjPair :: ( f :< ValueConstructors loc term1 , g :< ValueConstructors loc term2)
-        => (Value loc term1, Value loc term2)
-        -> Maybe (f (Value loc term1), g (Value loc term2))
+prjPair :: (f :< ValueConstructors , g :< ValueConstructors)
+        => (Value, Value)
+        -> Maybe (f Value, g Value)
 prjPair = bitraverse prjValue prjValue
 
 -- TODO: Parameterize Value by the set of constructors s.t. each language can have a distinct value union.
 
--- | A function value consisting of a list of parameters, the body of the function, and an environment of bindings captured by the body.
-data Closure location term value = Closure [Name] term (Environment location value)
+-- | A function value consisting of a list of parameter 'Name's, a 'Label' to jump to the body of the function, and an 'Environment' of bindings captured by the body.
+data Closure value = Closure [Name] Label (Environment Precise value)
   deriving (Eq, Generic1, Ord, Show)
 
-instance (Eq location, Eq term) => Eq1 (Closure location term) where liftEq = genericLiftEq
-instance (Ord location, Ord term) => Ord1 (Closure location term) where liftCompare = genericLiftCompare
-instance (Show location, Show term) => Show1 (Closure location term) where liftShowsPrec = genericLiftShowsPrec
+instance Eq1 Closure where liftEq = genericLiftEq
+instance Ord1 Closure where liftCompare = genericLiftCompare
+instance Show1 Closure where liftShowsPrec = genericLiftShowsPrec
 
 -- | The unit value. Typically used to represent the result of imperative statements.
 data Unit value = Unit
@@ -134,8 +134,8 @@ instance Show1 Array where liftShowsPrec = genericLiftShowsPrec
 -- | The environment for an abstract value type.
 type EnvironmentFor v = Environment (LocationFor v) v
 
--- | The store for an abstract value type.
-type StoreFor v = Store (LocationFor v) v
+-- | The 'Heap' for an abstract value type.
+type HeapFor value = Heap (LocationFor value) value
 
 -- | The cell for an abstract value type.
 type CellFor value = Cell (LocationFor value) value
@@ -145,7 +145,7 @@ type LiveFor value = Live (LocationFor value) value
 
 -- | The location type (the body of 'Address'es) which should be used for an abstract value type.
 type family LocationFor value :: *
-type instance LocationFor (Value location term) = location
+type instance LocationFor Value = Precise
 type instance LocationFor Type.Type = Monovariant
 
 -- | Value types, e.g. closures, which can root a set of addresses.
@@ -153,10 +153,10 @@ class ValueRoots value where
   -- | Compute the set of addresses rooted by a given value.
   valueRoots :: value -> LiveFor value
 
-instance Ord location => ValueRoots (Value location term) where
+instance ValueRoots Value where
   valueRoots v
-    | Just (Closure _ body env) <- prjValue v = envAll env `const` (body :: term)
-    | otherwise                               = mempty
+    | Just (Closure _ _ env) <- prjValue v = envAll env
+    | otherwise                            = mempty
 
 instance ValueRoots Type.Type where
   valueRoots _ = mempty
diff --git a/src/Language/Go/Syntax.hs b/src/Language/Go/Syntax.hs
index 904cbb2b1..27b67ce46 100644
--- a/src/Language/Go/Syntax.hs
+++ b/src/Language/Go/Syntax.hs
@@ -1,9 +1,9 @@
 {-# LANGUAGE DeriveAnyClass #-}
 module Language.Go.Syntax where
 
-import Prologue
-import Data.Abstract.Evaluatable
+import Data.Abstract.Evaluatable hiding (Label)
 import Diffing.Algorithm
+import Prologue
 
 -- A composite literal in Go
 data Composite a = Composite { compositeType :: !a, compositeElement :: !a }
diff --git a/src/Prologue.hs b/src/Prologue.hs
index cff645a5b..5d70b0572 100644
--- a/src/Prologue.hs
+++ b/src/Prologue.hs
@@ -1,7 +1,8 @@
 {-# LANGUAGE UndecidableInstances #-}
-module Prologue (
-  module X
-, ) where
+module Prologue
+( module X
+, foldMapA
+) where
 
 
 import Data.Bifunctor.Join as X
@@ -11,6 +12,7 @@ import Data.IntMap as X (IntMap)
 import Data.IntSet as X (IntSet)
 import Data.Ix as X (Ix(..))
 import Data.Map as X (Map)
+import Data.Monoid (Alt(..))
 import Data.Maybe as X
 import Data.Sequence as X (Seq)
 import Data.Set as X (Set)
@@ -67,3 +69,7 @@ import Data.Hashable as X (
 -- Generics
 import GHC.Generics as X hiding (moduleName)
 import GHC.Stack as X
+
+-- | Fold a collection by mapping each element onto an 'Alternative' action.
+foldMapA :: (Alternative m, Foldable t) => (b -> m a) -> t b -> m a
+foldMapA f = getAlt . foldMap (Alt . f)
diff --git a/src/Semantic/Util.hs b/src/Semantic/Util.hs
index 9089d4502..e41b90f52 100644
--- a/src/Semantic/Util.hs
+++ b/src/Semantic/Util.hs
@@ -14,7 +14,6 @@ import Data.Abstract.Evaluatable
 import Data.Abstract.Address
 import Data.Abstract.Type
 import Data.Abstract.Value
-import Data.AST
 import Data.Blob
 import Data.Diff
 import Data.Range
@@ -31,66 +30,58 @@ import Semantic.Task
 
 import qualified Language.Go.Assignment as Go
 import qualified Language.Python.Assignment as Python
-import qualified Language.Ruby.Assignment as Ruby
 import qualified Language.TypeScript.Assignment as TypeScript
 
-type PreciseValue a = Value Precise (Term (Union a) (Record Location))
-
-type GoValue         = PreciseValue Go.Syntax
-type RubyValue       = PreciseValue Ruby.Syntax
-type PythonValue     = PreciseValue Python.Syntax
-type TypeScriptValue = PreciseValue TypeScript.Syntax
-
 -- Ruby
-evaluateRubyFile = evaluateFile @RubyValue rubyParser
-evaluateRubyFiles = evaluateFiles @RubyValue rubyParser
+evaluateRubyFile = evaluateFile rubyParser
+evaluateRubyFiles = evaluateFiles rubyParser
 
 -- Go
-evaluateGoFile = evaluateFile @GoValue goParser
-evaluateGoFiles = evaluateFiles @GoValue goParser
+evaluateGoFile = evaluateFile goParser
+evaluateGoFiles = evaluateFiles goParser
 typecheckGoFile path = runAnalysis @(Caching Evaluating Go.Term Type) . evaluateModule . snd <$> parseFile goParser path
 
 -- Python
-evaluatePythonFile path = evaluate @PythonValue . snd <$> parseFile pythonParser path
-evaluatePythonFiles = evaluateFiles @PythonValue pythonParser
+evaluatePythonFile path = evaluate . snd <$> parseFile pythonParser path
+evaluatePythonFiles = evaluateFiles pythonParser
 typecheckPythonFile path = runAnalysis @(Caching Evaluating Python.Term Type) . evaluateModule . snd <$> parseFile pythonParser path
-tracePythonFile path = runAnalysis @(Tracing [] Evaluating Python.Term PythonValue) . evaluateModule . snd <$> parseFile pythonParser path
-evaluateDeadTracePythonFile path = runAnalysis @(DeadCode (Tracing [] Evaluating) Python.Term PythonValue) . evaluateModule . snd <$> parseFile pythonParser path
+tracePythonFile path = runAnalysis @(Tracing [] Evaluating Python.Term Value) . evaluateModule . snd <$> parseFile pythonParser path
+evaluateDeadTracePythonFile path = runAnalysis @(DeadCode (Tracing [] Evaluating) Python.Term Value) . evaluateModule . snd <$> parseFile pythonParser path
 
 -- TypeScript
 typecheckTypeScriptFile path = runAnalysis @(Caching Evaluating TypeScript.Term Type) . evaluateModule . snd <$> parseFile typescriptParser path
-evaluateTypeScriptFile = evaluateFile @TypeScriptValue typescriptParser
-evaluateTypeScriptFiles = evaluateFiles @TypeScriptValue typescriptParser
+evaluateTypeScriptFile = evaluateFile typescriptParser
+evaluateTypeScriptFiles = evaluateFiles typescriptParser
 
 -- Evalute a single file.
-evaluateFile :: forall value term effects
+evaluateFile :: forall term effects
              .  ( Evaluatable (Base term)
                 , FreeVariables term
-                , effects ~ RequiredEffects term value (Evaluating term value effects)
-                , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-                , MonadValue term value (Evaluating term value effects)
+                , effects ~ RequiredEffects term Value (Evaluating term Value effects)
+                , MonadAddressable Precise Value (Evaluating term Value effects)
+                , MonadValue Value (Evaluating term Value effects)
                 , Recursive term
                 )
              => Parser term
              -> FilePath
-             -> IO (Final effects value)
-evaluateFile parser path = runAnalysis @(Evaluating term value) . evaluateModule . snd <$> parseFile parser path
+             -> IO (Final effects Value)
+evaluateFile parser path = evaluate . snd <$> parseFile parser path
 
 -- Evaluate a list of files (head of file list is considered the entry point).
-evaluateFiles :: forall value term effects
+evaluateFiles :: forall term effects
               .  ( Evaluatable (Base term)
                  , FreeVariables term
-                 , effects ~ RequiredEffects term value (Evaluating term value effects)
-                 , MonadAddressable (LocationFor value) value (Evaluating term value effects)
-                 , MonadValue term value (Evaluating term value effects)
+                 , effects ~ RequiredEffects term Value (Evaluating term Value effects)
+                 , MonadAddressable Precise Value (Evaluating term Value effects)
+                 , MonadValue Value (Evaluating term Value effects)
                  , Recursive term
                  )
               => Parser term
               -> [FilePath]
-              -> IO (Final effects value)
+              -> IO (Final effects Value)
 evaluateFiles parser paths = do
   entry:xs <- traverse (parseFile parser) paths
-  pure $ evaluates @value xs entry
+  pure $ evaluates @Value xs entry
 
 -- Read and parse a file.
 parseFile :: Parser term -> FilePath -> IO (Blob, term)
diff --git a/test/Analysis/Go/Spec.hs b/test/Analysis/Go/Spec.hs
index faf26ff28..1e2d044ac 100644
--- a/test/Analysis/Go/Spec.hs
+++ b/test/Analysis/Go/Spec.hs
@@ -33,8 +33,8 @@ spec = parallel $ do
   where
     addr = Address . Precise
     fixtures = "test/fixtures/go/analysis/"
-    evaluate entry = snd . fst . fst . fst <$>
-      evaluateFiles @GoValue goParser
+    evaluate entry = snd . fst . fst . fst . fst <$>
+      evaluateFiles goParser
         [ fixtures <> entry
         , fixtures <> "foo/foo.go"
         , fixtures <> "bar/bar.go"
diff --git a/test/Analysis/Python/Spec.hs b/test/Analysis/Python/Spec.hs
index 4f7baa1ec..84df0f177 100644
--- a/test/Analysis/Python/Spec.hs
+++ b/test/Analysis/Python/Spec.hs
@@ -37,8 +37,8 @@ spec = parallel $ do
   where
     addr = Address . Precise
     fixtures = "test/fixtures/python/analysis/"
-    evaluate entry = snd . fst . fst . fst <$>
-      evaluateFiles @PythonValue pythonParser
+    evaluate entry = snd . fst . fst . fst . fst <$>
+      evaluateFiles pythonParser
       [ fixtures <> entry
       , fixtures <> "a.py"
       , fixtures <> "b/c.py"
diff --git a/test/Analysis/TypeScript/Spec.hs b/test/Analysis/TypeScript/Spec.hs
index 3ecc7962a..0deef4129 100644
--- a/test/Analysis/TypeScript/Spec.hs
+++ b/test/Analysis/TypeScript/Spec.hs
@@ -34,8 +34,8 @@ spec = parallel $ do
   where
     addr = Address . Precise
     fixtures = "test/fixtures/typescript/analysis/"
-    evaluate entry = snd . fst . fst . fst <$>
-      evaluateFiles @TypeScriptValue typescriptParser
+    evaluate entry = snd . fst . fst . fst . fst <$>
+      evaluateFiles typescriptParser
         [ fixtures <> entry
         , fixtures <> "a.ts"
         , fixtures <> "foo.ts"
diff --git a/test/SpecHelpers.hs b/test/SpecHelpers.hs
index d3752cf8a..568fb4276 100644
--- a/test/SpecHelpers.hs
+++ b/test/SpecHelpers.hs
@@ -12,8 +12,8 @@ module SpecHelpers (
 import Data.Abstract.Address as X
 import Data.Abstract.Environment as X
 import Data.Abstract.FreeVariables as X
+import Data.Abstract.Heap as X
 import Data.Abstract.ModuleTable as X
-import Data.Abstract.Store as X
 import Data.Blob as X
 import Data.Functor.Listable as X
 import Data.Language as X