diff --git a/semantic-core/src/Analysis/Concrete.hs b/semantic-core/src/Analysis/Concrete.hs
index 761a697dde..8cc45b8cbb 100644
--- a/semantic-core/src/Analysis/Concrete.hs
+++ b/semantic-core/src/Analysis/Concrete.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE FlexibleContexts, FlexibleInstances, LambdaCase, MultiParamTypeClasses, NamedFieldPuns, OverloadedStrings, RecordWildCards, TypeApplications, TypeOperators, UndecidableInstances #-}
 module Analysis.Concrete
 ( Concrete(..)
 , concrete
@@ -27,10 +27,11 @@ import qualified Data.IntMap as IntMap
 import qualified Data.IntSet as IntSet
 import           Data.Loc
 import qualified Data.Map as Map
-import           Data.Monoid (Alt(..))
 import           Data.Name
+import qualified Data.Set as Set
 import           Data.Term
 import           Data.Text (Text, pack)
+import           Data.Traversable (for)
 import           Prelude hiding (fail)
 
 type Precise = Int
@@ -40,25 +41,27 @@ newtype FrameId = FrameId { unFrameId :: Precise }
   deriving (Eq, Ord, Show)
 
 data Concrete
-  = Closure Loc User (Term Core.Core User) Precise
+  = Closure Loc User (Term Core.Core User) Env
   | Unit
   | Bool Bool
   | String Text
-  | Obj Frame
+  | Record Env
   deriving (Eq, Ord, Show)
 
-objectFrame :: Concrete -> Maybe Frame
-objectFrame (Obj frame) = Just frame
-objectFrame _           = Nothing
+recordFrame :: Concrete -> Maybe Env
+recordFrame (Record frame) = Just frame
+recordFrame _              = Nothing
 
-data Frame = Frame
-  { frameEdges :: [(Core.Edge, Precise)]
-  , frameSlots :: Env
+newtype Frame = Frame
+  { frameSlots :: Env
   }
   deriving (Eq, Ord, Show)
 
 type Heap = IntMap.IntMap Concrete
 
+data Edge = Lexical | Import
+  deriving (Eq, Ord, Show)
+
 
 -- | Concrete evaluation of a term to a value.
 --
@@ -74,7 +77,6 @@ concrete
 runFile :: ( Carrier sig m
            , Effect sig
            , Member Fresh sig
-           , Member (Reader FrameId) sig
            , Member (State Heap) sig
            )
         => File (Term Core.Core User)
@@ -82,38 +84,32 @@ runFile :: ( Carrier sig m
 runFile file = traverse run file
   where run = runReader (fileLoc file)
             . runFailWithLoc
+            . runReader @Env mempty
             . fix (eval concreteAnalysis)
 
 concreteAnalysis :: ( Carrier sig m
                     , Member Fresh sig
+                    , Member (Reader Env) sig
                     , Member (Reader Loc) sig
-                    , Member (Reader FrameId) sig
                     , Member (State Heap) sig
                     , MonadFail m
                     )
                  => Analysis Precise Concrete m
 concreteAnalysis = Analysis{..}
   where alloc _ = fresh
-        bind name addr = modifyCurrentFrame (updateFrameSlots (Map.insert name addr))
-        lookupEnv n = do
-          FrameId frameAddr <- ask
-          val <- deref frameAddr
-          heap <- get
-          pure (val >>= lookupConcrete heap n)
+        bind name addr m = local (Map.insert name addr) m
+        lookupEnv n = asks (Map.lookup n)
         deref = gets . IntMap.lookup
         assign addr value = modify (IntMap.insert addr value)
         abstract _ name body = do
           loc <- ask
-          FrameId parentAddr <- ask
-          pure (Closure loc name body parentAddr)
-        apply eval (Closure loc name body parentAddr) a = do
-          frameAddr <- fresh
-          assign frameAddr (Obj (Frame [(Core.Lexical, parentAddr)] mempty))
-          local (const loc) . (frameAddr ...) $ do
+          env <- asks (flip Map.restrictKeys (Set.delete name (foldMap Set.singleton body)))
+          pure (Closure loc name body env)
+        apply eval (Closure loc name body env) a = do
+          local (const loc) $ do
             addr <- alloc name
             assign addr a
-            bind name addr
-            eval body
+            local (const (Map.insert name addr env)) (eval body)
         apply _ f _ = fail $ "Cannot coerce " <> show f <> " to function"
         unit = pure Unit
         bool b = pure (Bool b)
@@ -122,30 +118,24 @@ concreteAnalysis = Analysis{..}
         string s = pure (String s)
         asString (String s) = pure s
         asString v          = fail $ "Cannot coerce " <> show v <> " to String"
-        -- FIXME: differential inheritance (reference fields instead of copying)
-        -- FIXME: copy non-lexical parents deeply?
-        frame = do
-          lexical <- asks unFrameId
-          pure (Obj (Frame [(Core.Lexical, lexical)] mempty))
-        -- FIXME: throw an error
-        -- FIXME: support dynamic imports
-        edge e addr = modifyCurrentFrame (\ (Frame ps fs) -> Frame ((e, addr) : ps) fs)
-        addr ... m = local (const (FrameId addr)) m
-
-        updateFrameSlots f frame = frame { frameSlots = f (frameSlots frame) }
-
-        modifyCurrentFrame f = do
-          addr <- asks unFrameId
-          Just (Obj frame) <- deref addr
-          assign addr (Obj (f frame))
+        record fields = do
+          fields' <- for fields $ \ (name, value) -> do
+            addr <- alloc name
+            assign addr value
+            pure (name, addr)
+          pure (Record (Map.fromList fields'))
+        addr ... n = do
+          val <- deref addr
+          heap <- get
+          pure (val >>= lookupConcrete heap n)
 
 
 lookupConcrete :: Heap -> User -> Concrete -> Maybe Precise
 lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete
   where -- look up the name in a concrete value
-        inConcrete = inFrame <=< maybeA . objectFrame
+        inConcrete = inFrame <=< maybeA . recordFrame
         -- look up the name in a specific 'Frame', with slots taking precedence over parents
-        inFrame (Frame ps fs) = maybeA (Map.lookup name fs) <|> getAlt (foldMap (Alt . inAddress . snd) ps)
+        inFrame fs = maybeA (Map.lookup name fs) <|> (maybeA (Map.lookup "__semantic_super" fs) >>= inAddress)
         -- look up the name in the value an address points to, if we haven’t already visited it
         inAddress addr = do
           visited <- get
@@ -157,10 +147,8 @@ lookupConcrete heap name = run . evalState IntSet.empty . runNonDet . inConcrete
         maybeA = maybe empty pure
 
 
-runHeap :: (Carrier sig m, Member Fresh sig) => ReaderC FrameId (StateC Heap m) a -> m (Heap, a)
-runHeap m = do
-  addr <- fresh
-  runState (IntMap.singleton addr (Obj (Frame [] mempty))) (runReader (FrameId addr) m)
+runHeap :: StateC Heap m a -> m (Heap, a)
+runHeap = runState mempty
 
 
 -- | 'heapGraph', 'heapValueGraph', and 'heapAddressGraph' allow us to conveniently export SVGs of the heap:
@@ -168,16 +156,15 @@ runHeap m = do
 --   > λ let (heap, res) = concrete [ruby]
 --   > λ writeFile "/Users/rob/Desktop/heap.dot" (export (addressStyle heap) (heapAddressGraph heap))
 --   > λ :!dot -Tsvg < ~/Desktop/heap.dot > ~/Desktop/heap.svg
-heapGraph :: (Precise -> Concrete -> a) -> (Either Core.Edge User -> Precise -> G.Graph a) -> Heap -> G.Graph a
+heapGraph :: (Precise -> Concrete -> a) -> (Either Edge User -> Precise -> G.Graph a) -> Heap -> G.Graph a
 heapGraph vertex edge h = foldr (uncurry graph) G.empty (IntMap.toList h)
   where graph k v rest = (G.vertex (vertex k v) `G.connect` outgoing v) `G.overlay` rest
         outgoing = \case
           Unit -> G.empty
           Bool _ -> G.empty
           String _ -> G.empty
-          Closure _ _ _ parentAddr -> edge (Left Core.Lexical) parentAddr
-          Obj frame -> fromFrame frame
-        fromFrame (Frame es ss) = foldr (G.overlay . uncurry (edge . Left)) (foldr (G.overlay . uncurry (edge . Right)) G.empty (Map.toList ss)) es
+          Closure _ _ _ env -> foldr (G.overlay . edge (Left Lexical)) G.empty env
+          Record frame -> Map.foldrWithKey (\ k -> G.overlay . edge (Right k)) G.empty frame
 
 heapValueGraph :: Heap -> G.Graph Concrete
 heapValueGraph h = heapGraph (const id) (const fromAddr) h
@@ -189,20 +176,20 @@ heapAddressGraph = heapGraph (\ addr v -> (Value v, addr)) (fmap G.vertex . (,)
 addressStyle :: Heap -> G.Style (EdgeType, Precise) Text
 addressStyle heap = (G.defaultStyle vertex) { G.edgeAttributes }
   where vertex (_, addr) = pack (show addr) <> " = " <> maybe "?" fromConcrete (IntMap.lookup addr heap)
-        edgeAttributes _ (Slot name,         _) = ["label" G.:= name]
-        edgeAttributes _ (Edge Core.Import,  _) = ["color" G.:= "blue"]
-        edgeAttributes _ (Edge Core.Lexical, _) = ["color" G.:= "green"]
-        edgeAttributes _ _                      = []
+        edgeAttributes _ (Slot name,    _) = ["label" G.:= name]
+        edgeAttributes _ (Edge Import,  _) = ["color" G.:= "blue"]
+        edgeAttributes _ (Edge Lexical, _) = ["color" G.:= "green"]
+        edgeAttributes _ _                 = []
         fromConcrete = \case
           Unit ->  "()"
           Bool b -> pack $ show b
           String s -> pack $ show s
           Closure (Loc p (Span s e)) n _ _ -> "\\\\ " <> n <> " [" <> p <> ":" <> showPos s <> "-" <> showPos e <> "]"
-          Obj _ -> "{}"
+          Record _ -> "{}"
         showPos (Pos l c) = pack (show l) <> ":" <> pack (show c)
 
 data EdgeType
-  = Edge Core.Edge
+  = Edge Edge
   | Slot User
   | Value Concrete
   deriving (Eq, Ord, Show)
diff --git a/semantic-core/src/Analysis/Eval.hs b/semantic-core/src/Analysis/Eval.hs
index a90df33753..2e68a8530f 100644
--- a/semantic-core/src/Analysis/Eval.hs
+++ b/semantic-core/src/Analysis/Eval.hs
@@ -11,6 +11,7 @@ module Analysis.Eval
 , Analysis(..)
 ) where
 
+import Control.Applicative (Alternative (..))
 import Control.Effect.Fail
 import Control.Effect.Reader
 import Control.Monad ((>=>))
@@ -18,7 +19,7 @@ import Data.Core as Core
 import Data.File
 import Data.Functor
 import Data.Loc
-import Data.Maybe (fromJust)
+import Data.Maybe (fromJust, fromMaybe)
 import Data.Name
 import Data.Scope
 import Data.Term
@@ -36,9 +37,17 @@ eval :: ( Carrier sig m
 eval Analysis{..} eval = \case
   Var n -> lookupEnv' n >>= deref' n
   Term c -> case c of
-    Let n -> alloc n >>= bind n >> unit
+    Rec (Named (Ignored n) b) -> do
+      addr <- alloc n
+      v <- bind n addr (eval (instantiate1 (pure n) b))
+      v <$ assign addr v
     a :>> b -> eval a >> eval b
-    Lam (Ignored n) b -> abstract eval n (instantiate1 (pure n) b)
+    Named (Ignored n) a :>>= b -> do
+      a' <- eval a
+      addr <- alloc n
+      assign addr a'
+      bind n addr (eval (instantiate1 (pure n) b))
+    Lam (Named (Ignored n) b) -> abstract eval n (instantiate1 (pure n) b)
     f :$ a -> do
       f' <- eval f
       a' <- eval a
@@ -50,11 +59,10 @@ eval Analysis{..} eval = \case
       if c' then eval t else eval e
     String s -> string s
     Load p -> eval p >>= asString >> unit -- FIXME: add a load command or something
-    Edge e a -> ref a >>= edge e >> unit
-    Frame -> frame
+    Record fields -> traverse (traverse eval) fields >>= record
     a :. b -> do
       a' <- ref a
-      a' ... eval b
+      a' ... b >>= maybe (freeVariable (show b)) (deref' b)
     a := b -> do
       b' <- eval b
       addr <- ref a
@@ -70,147 +78,140 @@ eval Analysis{..} eval = \case
         ref = \case
           Var n -> lookupEnv' n
           Term c -> case c of
-            Let n -> do
-              addr <- alloc n
-              addr <$ bind n addr
             If c t e -> do
               c' <- eval c >>= asBool
               if c' then ref t else ref e
             a :. b -> do
               a' <- ref a
-              a' ... ref b
+              a' ... b >>= maybe (freeVariable (show b)) pure
             Ann loc c -> local (const loc) (ref c)
             c -> invalidRef (show c)
 
 
 prog1 :: File (Term Core User)
-prog1 = fromBody . lam' foo $ block
-  [ let' bar .= pure foo
-  , Core.if' (pure bar)
+prog1 = fromBody $ lam (named' "foo")
+  (    named' "bar" :<- pure "foo"
+  >>>= Core.if' (pure "bar")
     (Core.bool False)
-    (Core.bool True)
-  ]
-  where (foo, bar) = ("foo", "bar")
+    (Core.bool True))
 
 prog2 :: File (Term Core User)
 prog2 = fromBody $ fileBody prog1 $$ Core.bool True
 
 prog3 :: File (Term Core User)
-prog3 = fromBody $ lams' [foo, bar, quux]
-  (Core.if' (pure quux)
-    (pure bar)
-    (pure foo))
-  where (foo, bar, quux) = ("foo", "bar", "quux")
+prog3 = fromBody $ lams [named' "foo", named' "bar", named' "quux"]
+  (Core.if' (pure "quux")
+    (pure "bar")
+    (pure "foo"))
 
 prog4 :: File (Term Core User)
-prog4 = fromBody $ block
-  [ let' foo .= Core.bool True
-  , Core.if' (pure foo)
+prog4 = fromBody
+  (    named' "foo" :<- Core.bool True
+  >>>= Core.if' (pure "foo")
     (Core.bool True)
-    (Core.bool False)
-  ]
-  where foo = "foo"
+    (Core.bool False))
 
 prog5 :: File (Term Core User)
-prog5 = fromBody $ block
-  [ let' "mkPoint" .= lam' "_x" (lam' "_y" (block
-    [ let' "this" .= Core.frame
-    , pure "this" Core.... let' "x" .= pure "_x"
-    , pure "this" Core.... let' "y" .= pure "_y"
-    , pure "this"
+prog5 = fromBody $ ann (do'
+  [ Just (named' "mkPoint") :<- lams [named' "_x", named' "_y"] (ann (Core.record
+    [ ("x", ann (pure "_x"))
+    , ("y", ann (pure "_y"))
     ]))
-  , let' "point" .= pure "mkPoint" $$ Core.bool True $$ Core.bool False
-  , pure "point" Core.... pure "x"
-  , pure "point" Core.... pure "y" .= pure "point" Core.... pure "x"
-  ]
+  , Just (named' "point") :<- ann (ann (ann (pure "mkPoint") $$ ann (Core.bool True)) $$ ann (Core.bool False))
+  , Nothing :<- ann (ann (pure "point") Core.... "x")
+  , Nothing :<- ann (ann (pure "point") Core.... "y") .= ann (ann (pure "point") Core.... "x")
+  ])
 
 prog6 :: [File (Term Core User)]
 prog6 =
-  [ File (Loc "dep"  (locSpan (fromJust here))) $ block
-    [ let' "dep" .= Core.frame
-    , pure "dep" Core.... (let' "var" .= Core.bool True)
-    ]
-  , File (Loc "main" (locSpan (fromJust here))) $ block
+  [ File (Loc "dep"  (locSpan (fromJust here))) $ Core.record
+    [ ("dep", Core.record [ ("var", Core.bool True) ]) ]
+  , File (Loc "main" (locSpan (fromJust here))) $ do' (map (Nothing :<-)
     [ load (Core.string "dep")
-    , let' "thing" .= pure "dep" Core.... pure "var"
-    ]
-  ]
-
-ruby :: File (Term Core User)
-ruby = fromBody . ann . block $
-  [ ann (let' "Class" .= Core.frame)
-  , ann (pure "Class" Core....
-    (ann (let' "new" .= lam' "self" (block
-      [ ann (let' "instance" .= Core.frame)
-      , ann (pure "instance" Core.... Core.edge Import (pure "self"))
-      , ann (pure "instance" $$$ "initialize")
-      ]))))
-
-  , ann (let' "(Object)" .= Core.frame)
-  , ann (pure "(Object)" Core.... ann (Core.edge Import (pure ("Class"))))
-  , ann (let' "Object" .= Core.frame)
-  , ann (pure "Object" Core.... block
-    [ ann (Core.edge Import (pure "(Object)"))
-    , ann (let' "nil?" .= lam' "_" false)
-    , ann (let' "initialize" .= lam' "self" (pure "self"))
-    , ann (let' __semantic_truthy .= lam' "_" (Core.bool True))
-    ])
-
-  , ann (pure "Class" Core.... Core.edge Import (pure "Object"))
-
-  , ann (let' "(NilClass)" .= Core.frame)
-  , ann (pure "(NilClass)" Core.... block
-    [ ann (Core.edge Import (pure "Class"))
-    , ann (Core.edge Import (pure "(Object)"))
-    ])
-  , ann (let' "NilClass" .= Core.frame)
-  , ann (pure "NilClass" Core.... block
-    [ ann (Core.edge Import (pure "(NilClass)"))
-    , ann (Core.edge Import (pure "Object"))
-    , ann (let' "nil?" .= lam' "_" true)
-    , ann (let' __semantic_truthy .= lam' "_" (Core.bool False))
-    ])
-
-  , ann (let' "(TrueClass)" .= Core.frame)
-  , ann (pure "(TrueClass)" Core.... block
-    [ ann (Core.edge Import (pure "Class"))
-    , ann (Core.edge Import (pure "(Object)"))
-    ])
-  , ann (let' "TrueClass" .= Core.frame)
-  , ann (pure "TrueClass" Core.... block
-    [ ann (Core.edge Import (pure "(TrueClass)"))
-    , ann (Core.edge Import (pure "Object"))
+    , Core.record [ ("thing", pure "dep" Core.... "var") ]
     ])
-
-  , ann (let' "(FalseClass)" .= Core.frame)
-  , ann (pure "(FalseClass)" Core.... block
-    [ ann (Core.edge Import (pure "Class"))
-    , ann (Core.edge Import (pure "(Object)"))
-    ])
-  , ann (let' "FalseClass" .= Core.frame)
-  , ann (pure "FalseClass" Core.... block
-    [ ann (Core.edge Import (pure "(FalseClass)"))
-    , ann (Core.edge Import (pure "Object"))
-    , ann (let' __semantic_truthy .= lam' "_" (Core.bool False))
-    ])
-
-  , ann (let' "nil"   .= pure "NilClass"   $$$ "new")
-  , ann (let' "true"  .= pure "TrueClass"  $$$ "new")
-  , ann (let' "false" .= pure "FalseClass" $$$ "new")
-
-  , ann (let' "require" .= lam' "path" (Core.load (pure "path")))
   ]
-  where -- _nil  = pure "nil"
-        true  = pure "true"
-        false = pure "false"
-        self $$$ method = annWith callStack $ lam' "_x" (pure "_x" Core.... pure method $$ pure "_x") $$ self
 
+ruby :: File (Term Core User)
+ruby = fromBody $ annWith callStack (rec (named' __semantic_global) (do' statements))
+  where statements =
+          [ Just "Class" :<- record
+            [ (__semantic_super, Core.record [])
+            , ("new", lam "self"
+              (    "instance" :<- record [ (__semantic_super, var "self") ]
+              >>>= var "instance" $$$ "initialize"))
+            ]
+
+          , Just "(Object)" :<- record [ (__semantic_super, var "Class") ]
+          , Just "Object" :<- record
+            [ (__semantic_super, var "(Object)")
+            , ("nil?", lam "_" (var __semantic_global ... "false"))
+            , ("initialize", lam "self" (var "self"))
+            , (__semantic_truthy, lam "_" (bool True))
+            ]
+
+          , Just "(NilClass)" :<- record
+            -- FIXME: what should we do about multiple import edges like this
+            [ (__semantic_super, var "Class")
+            , (__semantic_super, var "(Object)")
+            ]
+          , Just "NilClass" :<- record
+            [ (__semantic_super, var "(NilClass)")
+            , (__semantic_super, var "Object")
+            , ("nil?", lam "_" (var __semantic_global ... "true"))
+            , (__semantic_truthy, lam "_" (bool False))
+            ]
+
+          , Just "(TrueClass)" :<- record
+            [ (__semantic_super, var "Class")
+            , (__semantic_super, var "(Object)")
+            ]
+          , Just "TrueClass" :<- record
+            [ (__semantic_super, var "(TrueClass)")
+            , (__semantic_super, var "Object")
+            ]
+
+          , Just "(FalseClass)" :<- record
+            [ (__semantic_super, var "Class")
+            , (__semantic_super, var "(Object)")
+            ]
+          , Just "FalseClass" :<- record
+            [ (__semantic_super, var "(FalseClass)")
+            , (__semantic_super, var "Object")
+            , (__semantic_truthy, lam "_" (bool False))
+            ]
+
+          , Just "nil"   :<- var "NilClass"   $$$ "new"
+          , Just "true"  :<- var "TrueClass"  $$$ "new"
+          , Just "false" :<- var "FalseClass" $$$ "new"
+
+          , Just "require" :<- lam "path" (Core.load (var "path"))
+
+          , Nothing :<- var "Class" ... __semantic_super .= var "Object"
+          , Nothing :<- record (statements >>= \ (v :<- _) -> maybe [] (\ v -> [(v, var v)]) v)
+          ]
+        self $$$ method = annWith callStack ("_x" :<- self >>>= var "_x" ... method $$ var "_x")
+        record ... field = annWith callStack (record Core.... field)
+        record bindings = annWith callStack (Core.record bindings)
+        var x = annWith callStack (pure x)
+        lam v b = annWith callStack (Core.lam (named' v) b)
+        a >>> b = annWith callStack (a Core.>>> b)
+        infixr 1 >>>
+        v :<- a >>>= b = annWith callStack (named' v :<- a Core.>>>= b)
+        infixr 1 >>>=
+        do' bindings = fromMaybe Core.unit (foldr bind Nothing bindings)
+          where bind (n :<- a) v = maybe (a >>>) ((>>>=) . (:<- a)) n <$> v <|> Just a
+        bool b = annWith callStack (Core.bool b)
+        a .= b = annWith callStack (a Core..= b)
+
+        __semantic_global = "__semantic_global"
+        __semantic_super  = "__semantic_super"
         __semantic_truthy = "__semantic_truthy"
 
 
 data Analysis address value m = Analysis
   { alloc       :: User -> m address
-  , bind        :: User -> address -> m ()
+  , bind        :: forall a . User -> address -> m a -> m a
   , lookupEnv   :: User -> m (Maybe address)
   , deref       :: address -> m (Maybe value)
   , assign      :: address -> value -> m ()
@@ -221,7 +222,6 @@ data Analysis address value m = Analysis
   , asBool      :: value -> m Bool
   , string      :: Text -> m value
   , asString    :: value -> m Text
-  , frame       :: m value
-  , edge        :: Edge -> address -> m ()
-  , (...)       :: forall a . address -> m a -> m a
+  , record      :: [(User, value)] -> m value
+  , (...)       :: address -> User -> m (Maybe address)
   }
diff --git a/semantic-core/src/Analysis/ImportGraph.hs b/semantic-core/src/Analysis/ImportGraph.hs
index 7247462f17..5e87e38ec1 100644
--- a/semantic-core/src/Analysis/ImportGraph.hs
+++ b/semantic-core/src/Analysis/ImportGraph.hs
@@ -80,7 +80,7 @@ importGraphAnalysis :: ( Alternative m
                     => Analysis User Value m
 importGraphAnalysis = Analysis{..}
   where alloc = pure
-        bind _ _ = pure ()
+        bind _ _ m = m
         lookupEnv = pure . Just
         deref addr = gets (Map.lookup addr) >>= maybe (pure Nothing) (foldMapA (pure . Just)) . nonEmpty . maybe [] Set.toList
         assign addr ty = modify (Map.insertWith (<>) addr (Set.singleton ty))
@@ -91,8 +91,7 @@ importGraphAnalysis = Analysis{..}
         apply eval (Value (Closure loc name body _) _) a = local (const loc) $ do
           addr <- alloc name
           assign addr a
-          bind name addr
-          eval body
+          bind name addr (eval body)
         apply _ f _ = fail $ "Cannot coerce " <> show f <> " to function"
         unit = pure mempty
         bool _ = pure mempty
@@ -100,9 +99,5 @@ importGraphAnalysis = Analysis{..}
         string s = pure (Value (String s) mempty)
         asString (Value (String s) _) = pure s
         asString _ = pure mempty
-        frame = pure mempty
-        edge Core.Import to = do -- FIXME: figure out some other way to do this
-          Loc{locPath=from} <- ask
-          () <$ pure (Value Abstract (Map.singleton from (Set.singleton to)))
-        edge _ _ = pure ()
-        _ ... m = m
+        record fields = pure (Value Abstract (foldMap (valueGraph . snd) fields))
+        _ ... m = pure (Just m)
diff --git a/semantic-core/src/Analysis/Typecheck.hs b/semantic-core/src/Analysis/Typecheck.hs
index 998dc301b6..f2bf865964 100644
--- a/semantic-core/src/Analysis/Typecheck.hs
+++ b/semantic-core/src/Analysis/Typecheck.hs
@@ -73,7 +73,7 @@ instance RightModule Polytype where
 
 
 forAll :: (Eq a, Carrier sig m, Member Polytype sig) => a -> m a -> m a
-forAll n body = send (PForAll (Data.Scope.bind1 n body))
+forAll n body = send (PForAll (abstract1 n body))
 
 forAlls :: (Eq a, Carrier sig m, Member Polytype sig, Foldable t) => t a -> m a -> m a
 forAlls ns body = foldr forAll body ns
@@ -122,12 +122,11 @@ typecheckingAnalysis
      , Member Fresh sig
      , Member (State (Set.Set Constraint)) sig
      , Member (State (Heap User (Term Monotype Meta))) sig
-     , MonadFail m
      )
   => Analysis User (Term Monotype Meta) m
 typecheckingAnalysis = Analysis{..}
   where alloc = pure
-        bind _ _ = pure ()
+        bind _ _ m = m
         lookupEnv = pure . Just
         deref addr = gets (Map.lookup addr) >>= maybe (pure Nothing) (foldMapA (pure . Just)) . nonEmpty . maybe [] Set.toList
         assign addr ty = modify (Map.insertWith (<>) addr (Set.singleton ty))
@@ -149,9 +148,8 @@ typecheckingAnalysis = Analysis{..}
         asBool b = unify (Term Bool) b >> pure True <|> pure False
         string _ = pure (Term String)
         asString s = unify (Term String) s $> mempty
-        frame = fail "unimplemented"
-        edge _ _ = pure ()
-        _ ... m = m
+        record fields = pure (Term (Record (Map.fromList fields)))
+        _ ... m = pure (Just m)
 
 
 data Constraint = Term Monotype Meta :===: Term Monotype Meta
diff --git a/semantic-core/src/Data/Core.hs b/semantic-core/src/Data/Core.hs
index 31f3912caf..65bbbe7ba6 100644
--- a/semantic-core/src/Data/Core.hs
+++ b/semantic-core/src/Data/Core.hs
@@ -2,16 +2,19 @@
              ScopedTypeVariables, StandaloneDeriving, TypeFamilies, TypeOperators, UndecidableInstances #-}
 module Data.Core
 ( Core(..)
-, Edge(..)
-, let'
-, block
+, rec
+, (>>>)
+, unseq
+, unseqs
+, (>>>=)
+, unbind
+, unstatement
+, do'
+, unstatements
+, (:<-)(..)
 , lam
-, lam'
 , lams
-, lams'
 , unlam
-, unseq
-, unseqs
 , ($$)
 , ($$*)
 , unapply
@@ -21,8 +24,7 @@ module Data.Core
 , if'
 , string
 , load
-, edge
-, frame
+, record
 , (...)
 , (.=)
 , ann
@@ -34,9 +36,11 @@ module Data.Core
 import Control.Applicative (Alternative (..))
 import Control.Effect.Carrier
 import Control.Monad.Module
+import Data.Bifunctor (Bifunctor (..))
 import Data.Foldable (foldl')
-import Data.List.NonEmpty
+import Data.List.NonEmpty (NonEmpty (..))
 import Data.Loc
+import Data.Maybe (fromMaybe)
 import Data.Name
 import Data.Scope
 import Data.Stack
@@ -45,14 +49,18 @@ import Data.Text (Text)
 import GHC.Generics (Generic1)
 import GHC.Stack
 
-data Edge = Lexical | Import
-  deriving (Eq, Ord, Show)
-
 data Core f a
-  = Let User
+  -- | Recursive local binding of a name in a scope; strict evaluation of the name in the body will diverge.
+  --
+  --   Simultaneous (and therefore potentially mutually-recursive) bidnings can be made by binding a 'Record' recursively within 'Rec' and projecting from it with ':.'.
+  = Rec (Named (Scope () f a))
   -- | Sequencing without binding; analogous to '>>' or '*>'.
   | f a :>> f a
-  | Lam (Ignored User) (Scope () f a)
+  -- | Sequencing with binding; analogous to '>>='.
+  --
+  --   Bindings made with :>>= are sequential, i.e. the name is not bound within the value, only within the consequence.
+  | Named (f a) :>>= Scope () f a
+  | Lam (Named (Scope () f a))
   -- | Function application; analogous to '$'.
   | f a :$ f a
   | Unit
@@ -61,18 +69,19 @@ data Core f a
   | String Text
   -- | Load the specified file (by path).
   | Load (f a)
-  | Edge Edge (f a)
-  -- | Allocation of a new frame.
-  | Frame
-  | f a :. f a
+  -- | A record mapping some keys to some values.
+  | Record [(User, f a)]
+  -- | Projection from a record.
+  | f a :. User
   -- | Assignment of a value to the reference returned by the lhs.
   | f a := f a
   | Ann Loc (f a)
   deriving (Foldable, Functor, Generic1, Traversable)
 
 infixr 1 :>>
-infixl 9 :$
-infixl 4 :.
+infixr 1 :>>=
+infixl 8 :$
+infixl 9 :.
 infix  3 :=
 
 instance HFunctor Core
@@ -83,69 +92,88 @@ deriving instance (Ord  a, forall a . Eq   a => Eq   (f a)
 deriving instance (Show a, forall a . Show a => Show (f a))          => Show (Core f a)
 
 instance RightModule Core where
-  Let u     >>=* _ = Let u
-  (a :>> b) >>=* f = (a >>= f) :>> (b >>= f)
-  Lam v b   >>=* f = Lam v (b >>=* f)
-  (a :$ b)  >>=* f = (a >>= f) :$ (b >>= f)
-  Unit      >>=* _ = Unit
-  Bool b    >>=* _ = Bool b
-  If c t e  >>=* f = If (c >>= f) (t >>= f) (e >>= f)
-  String s  >>=* _ = String s
-  Load b    >>=* f = Load (b >>= f)
-  Edge e b  >>=* f = Edge e (b >>= f)
-  Frame     >>=* _ = Frame
-  (a :. b)  >>=* f = (a >>= f) :. (b >>= f)
-  (a := b)  >>=* f = (a >>= f) := (b >>= f)
-  Ann l b   >>=* f = Ann l (b >>= f)
+  Rec b      >>=* f = Rec ((>>=* f) <$> b)
+  (a :>> b)  >>=* f = (a >>= f) :>> (b >>= f)
+  (a :>>= b) >>=* f = ((>>= f) <$> a) :>>= (b >>=* f)
+  Lam b      >>=* f = Lam ((>>=* f) <$> b)
+  (a :$ b)   >>=* f = (a >>= f) :$ (b >>= f)
+  Unit       >>=* _ = Unit
+  Bool b     >>=* _ = Bool b
+  If c t e   >>=* f = If (c >>= f) (t >>= f) (e >>= f)
+  String s   >>=* _ = String s
+  Load b     >>=* f = Load (b >>= f)
+  Record fs  >>=* f = Record (map (fmap (>>= f)) fs)
+  (a :. b)   >>=* f = (a >>= f) :. b
+  (a := b)   >>=* f = (a >>= f) := (b >>= f)
+  Ann l b    >>=* f = Ann l (b >>= f)
+
+
+rec :: (Eq a, Carrier sig m, Member Core sig) => Named a -> m a -> m a
+rec (Named u n) b = send (Rec (Named u (abstract1 n b)))
+
+(>>>) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
+a >>> b = send (a :>> b)
+
+infixr 1 >>>
 
+unseq :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
+unseq (Term sig) | Just (a :>> b) <- prj sig = pure (a, b)
+unseq _                                      = empty
 
-let' :: (Carrier sig m, Member Core sig) => User -> m a
-let' = send . Let
+unseqs :: Member Core sig => Term sig a -> NonEmpty (Term sig a)
+unseqs = go
+  where go t = case unseq t of
+          Just (l, r) -> go l <> go r
+          Nothing     -> t :| []
 
-block :: (Foldable t, Carrier sig m, Member Core sig) => t (m a) -> m a
-block = maybe unit getBlock . foldMap (Just . Block)
+(>>>=) :: (Eq a, Carrier sig m, Member Core sig) => (Named a :<- m a) -> m a -> m a
+Named u n :<- a >>>= b = send (Named u a :>>= abstract1 n b)
 
-newtype Block m a = Block { getBlock :: m a }
+infixr 1 >>>=
 
-instance (Carrier sig m, Member Core sig) => Semigroup (Block m a) where
-  Block a <> Block b = Block (send (a :>> b))
+unbind :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a :<- Term sig a, Term sig a)
+unbind n (Term sig) | Just (Named u a :>>= b) <- prj sig = pure (Named u n :<- a, instantiate1 (pure n) b)
+unbind _ _                                               = empty
 
-lam :: (Eq a, Carrier sig m, Member Core sig) => Named a -> m a -> m a
-lam (Named u n) b = send (Lam u (bind1 n b))
+unstatement :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Maybe (Named a) :<- Term sig a, Term sig a)
+unstatement n t = first (first Just) <$> unbind n t <|> first (Nothing :<-) <$> unseq t
 
-lam' :: (Carrier sig m, Member Core sig) => User -> m User -> m User
-lam' u = lam (named' u)
+do' :: (Eq a, Foldable t, Carrier sig m, Member Core sig) => t (Maybe (Named a) :<- m a) -> m a
+do' bindings = fromMaybe unit (foldr bind Nothing bindings)
+  where bind (n :<- a) v = maybe (a >>>) ((>>>=) . (:<- a)) n <$> v <|> Just a
 
-lams :: (Eq a, Foldable t, Carrier sig m, Member Core sig) => t (Named a) -> m a -> m a
-lams names body = foldr lam body names
+unstatements :: (Member Core sig, RightModule sig) => Term sig a -> (Stack (Maybe (Named (Either Int a)) :<- Term sig (Either Int a)), Term sig (Either Int a))
+unstatements = unprefix (unstatement . Left) . fmap Right
 
-lams' :: (Foldable t, Carrier sig m, Member Core sig) => t User -> m User -> m User
-lams' names body = foldr lam' body names
+data a :<- b = a :<- b
+  deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
 
-unlam :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a, Term sig a)
-unlam n (Term sig) | Just (Lam v b) <- prj sig = pure (Named v n, instantiate (const (pure n)) b)
-unlam _ _                                      = empty
+infix 2 :<-
 
-unseq :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
-unseq (Term sig) | Just (a :>> b) <- prj sig = pure (a, b)
-unseq _                                      = empty
+instance Bifunctor (:<-) where
+  bimap f g (a :<- b) = f a :<- g b
 
-unseqs :: Member Core sig => Term sig a -> NonEmpty (Term sig a)
-unseqs = go
-  where go t = case unseq t of
-          Just (l, r) -> go l <> go r
-          Nothing     -> t :| []
+
+lam :: (Eq a, Carrier sig m, Member Core sig) => Named a -> m a -> m a
+lam (Named u n) b = send (Lam (Named u (abstract1 n b)))
+
+lams :: (Eq a, Foldable t, Carrier sig m, Member Core sig) => t (Named a) -> m a -> m a
+lams names body = foldr lam body names
+
+unlam :: (Alternative m, Member Core sig, RightModule sig) => a -> Term sig a -> m (Named a, Term sig a)
+unlam n (Term sig) | Just (Lam b) <- prj sig = pure (n <$ b, instantiate1 (pure n) (namedValue b))
+unlam _ _                                    = empty
 
 ($$) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
 f $$ a = send (f :$ a)
 
-infixl 9 $$
+infixl 8 $$
 
 -- | Application of a function to a sequence of arguments.
 ($$*) :: (Foldable t, Carrier sig m, Member Core sig) => m a -> t (m a) -> m a
 ($$*) = foldl' ($$)
 
-infixl 9 $$*
+infixl 8 $$*
 
 unapply :: (Alternative m, Member Core sig) => Term sig a -> m (Term sig a, Term sig a)
 unapply (Term sig) | Just (f :$ a) <- prj sig = pure (f, a)
@@ -171,16 +199,13 @@ string = send . String
 load :: (Carrier sig m, Member Core sig) => m a -> m a
 load = send . Load
 
-edge :: (Carrier sig m, Member Core sig) => Edge -> m a -> m a
-edge e b = send (Edge e b)
-
-frame :: (Carrier sig m, Member Core sig) => m a
-frame = send Frame
+record :: (Carrier sig m, Member Core sig) => [(User, m a)] -> m a
+record fs = send (Record fs)
 
-(...) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
+(...) :: (Carrier sig m, Member Core sig) => m a -> User -> m a
 a ... b = send (a :. b)
 
-infixl 4 ...
+infixl 9 ...
 
 (.=) :: (Carrier sig m, Member Core sig) => m a -> m a -> m a
 a .= b = send (a := b)
diff --git a/semantic-core/src/Data/Core/Parser.hs b/semantic-core/src/Data/Core/Parser.hs
index 41fd795b15..3ae921dd75 100644
--- a/semantic-core/src/Data/Core/Parser.hs
+++ b/semantic-core/src/Data/Core/Parser.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE TypeOperators #-}
 module Data.Core.Parser
   ( module Text.Trifecta
   , core
@@ -10,8 +11,9 @@ module Data.Core.Parser
 
 import           Control.Applicative
 import qualified Data.Char as Char
-import           Data.Core (Core, Edge(..))
+import           Data.Core ((:<-) (..), Core)
 import qualified Data.Core as Core
+import           Data.Foldable (foldl')
 import           Data.Name
 import           Data.String
 import           Data.Term
@@ -48,44 +50,51 @@ core :: (TokenParsing m, Monad m) => m (Term Core User)
 core = expr
 
 expr :: (TokenParsing m, Monad m) => m (Term Core User)
-expr = atom `chainl1` go where
-  go = choice [ (Core....) <$ dot
-              , (Core.$$)  <$ notFollowedBy dot
-              ]
+expr = ifthenelse <|> lambda <|> rec <|> load <|> assign
+
+assign :: (TokenParsing m, Monad m) => m (Term Core User)
+assign = application <**> (symbolic '=' *> rhs <|> pure id) <?> "assignment"
+  where rhs = flip (Core..=) <$> application
+
+application :: (TokenParsing m, Monad m) => m (Term Core User)
+application = projection `chainl1` (pure (Core.$$))
+
+projection :: (TokenParsing m, Monad m) => m (Term Core User)
+projection = foldl' (Core....) <$> atom <*> many (namedValue <$ dot <*> name)
 
 atom :: (TokenParsing m, Monad m) => m (Term Core User)
 atom = choice
   [ comp
-  , ifthenelse
-  , edge
   , lit
   , ident
-  , assign
   , parens expr
   ]
 
 comp :: (TokenParsing m, Monad m) => m (Term Core User)
-comp = braces (Core.block <$> sepEndByNonEmpty expr semi) <?> "compound statement"
+comp = braces (Core.do' <$> sepEndByNonEmpty statement semi) <?> "compound statement"
+
+statement :: (TokenParsing m, Monad m) => m (Maybe (Named User) :<- Term Core User)
+statement
+  =   try ((:<-) . Just <$> name <* symbol "<-" <*> expr)
+  <|> (Nothing :<-) <$> expr
+  <?> "statement"
 
 ifthenelse :: (TokenParsing m, Monad m) => m (Term Core User)
 ifthenelse = Core.if'
-  <$ reserved "if"   <*> core
-  <* reserved "then" <*> core
-  <* reserved "else" <*> core
+  <$ reserved "if"   <*> expr
+  <* reserved "then" <*> expr
+  <* reserved "else" <*> expr
   <?> "if-then-else statement"
 
-assign :: (TokenParsing m, Monad m) => m (Term Core User)
-assign = (Core..=) <$> try (lvalue <* symbolic '=') <*> core <?> "assignment"
+rec :: (TokenParsing m, Monad m) => m (Term Core User)
+rec = Core.rec <$ reserved "rec" <*> name <* symbolic '=' <*> expr <?> "recursive binding"
 
-edge :: (TokenParsing m, Monad m) => m (Term Core User)
-edge = kw <*> expr where kw = choice [ Core.edge Lexical <$ reserved "lexical"
-                                     , Core.edge Import  <$ reserved "import"
-                                     , Core.load         <$ reserved "load"
-                                     ]
+load :: (TokenParsing m, Monad m) => m (Term Core User)
+load = Core.load <$ reserved "load" <*> expr
 
 lvalue :: (TokenParsing m, Monad m) => m (Term Core User)
 lvalue = choice
-  [ Core.let' . namedValue <$ reserved "let" <*> name
+  [ projection
   , ident
   , parens expr
   ]
@@ -93,20 +102,22 @@ lvalue = choice
 -- * Literals
 
 name :: (TokenParsing m, Monad m) => m (Named User)
-name = named' <$> identifier <?> "name" where
+name = named' <$> identifier <?> "name"
 
 lit :: (TokenParsing m, Monad m) => m (Term Core User)
 lit = let x `given` n = x <$ reserved n in choice
   [ Core.bool True  `given` "#true"
   , Core.bool False `given` "#false"
   , Core.unit       `given` "#unit"
-  , Core.frame      `given` "#frame"
-  , between (string "\"") (string "\"") (Core.string . fromString <$> many ('"' <$ string "\\\"" <|> noneOf "\""))
-  , lambda
+  , record
+  , Core.string <$> stringLiteral
   ] <?> "literal"
 
+record :: (TokenParsing m, Monad m) => m (Term Core User)
+record = Core.record <$ reserved "#record" <*> braces (sepEndBy ((,) <$> identifier <* symbolic ':' <*> expr) comma)
+
 lambda :: (TokenParsing m, Monad m) => m (Term Core User)
-lambda = Core.lam <$ lambduh <*> name <* arrow <*> core <?> "lambda" where
+lambda = Core.lam <$ lambduh <*> name <* arrow <*> expr <?> "lambda" where
   lambduh = symbolic 'λ' <|> symbolic '\\'
   arrow   = symbol "→"   <|> symbol "->"
 
diff --git a/semantic-core/src/Data/Core/Pretty.hs b/semantic-core/src/Data/Core/Pretty.hs
index 92280c0fd7..2bb0170b6b 100644
--- a/semantic-core/src/Data/Core/Pretty.hs
+++ b/semantic-core/src/Data/Core/Pretty.hs
@@ -8,19 +8,19 @@ module Data.Core.Pretty
   , prettyCore
   ) where
 
-import           Control.Effect.Reader
 import           Data.Core
 import           Data.File
+import           Data.Foldable (toList)
 import           Data.Name
 import           Data.Scope
+import           Data.Stack
 import           Data.Term
-import           Data.Text.Prettyprint.Doc (Pretty (..), annotate, softline, (<+>))
-import qualified Data.Text.Prettyprint.Doc as Pretty
+import           Data.Text.Prettyprint.Doc
 import qualified Data.Text.Prettyprint.Doc.Render.String as Pretty
 import qualified Data.Text.Prettyprint.Doc.Render.Terminal as Pretty
 
 showCore :: Term Core User -> String
-showCore = Pretty.renderString . Pretty.layoutSmart Pretty.defaultLayoutOptions . Pretty.unAnnotate . prettyCore Ascii
+showCore = Pretty.renderString . layoutSmart defaultLayoutOptions . unAnnotate . prettyCore Ascii
 
 printCore :: Term Core User -> IO ()
 printCore p = Pretty.putDoc (prettyCore Unicode p) *> putStrLn ""
@@ -31,88 +31,91 @@ showFile = showCore . fileBody
 printFile :: File (Term Core User) -> IO ()
 printFile = printCore . fileBody
 
-type AnsiDoc = Pretty.Doc Pretty.AnsiStyle
+type AnsiDoc = Doc Pretty.AnsiStyle
 
 keyword, symbol, strlit, primitive :: AnsiDoc -> AnsiDoc
 keyword = annotate (Pretty.colorDull Pretty.Cyan)
-symbol  = annotate (Pretty.color Pretty.Yellow)
+symbol  = annotate (Pretty.color     Pretty.Yellow)
 strlit  = annotate (Pretty.colorDull Pretty.Green)
 primitive = keyword . mappend "#"
 
-type Prec = Int
-
 data Style = Unicode | Ascii
 
 name :: User -> AnsiDoc
-name n = encloseIf (needsQuotation n) (symbol "#{") (symbol "}") (pretty n)
-
-with :: (Member (Reader Prec) sig, Carrier sig m) => Prec -> m a -> m a
-with n = local (const n)
-
-inParens :: (Member (Reader Prec) sig, Carrier sig m) => Prec -> m AnsiDoc -> m AnsiDoc
-inParens amount go = do
-  prec <- ask
-  body <- with amount go
-  pure (encloseIf (amount >= prec) (symbol "(") (symbol ")") body)
+name n = if needsQuotation n then enclose (symbol "#{") (symbol "}") (pretty n) else pretty n
 
 prettyCore :: Style -> Term Core User -> AnsiDoc
-prettyCore style = run . runReader @Prec 0 . go
+prettyCore style = precBody . go . fmap name
   where go = \case
-          Var v -> pure (name v)
+          Var v -> atom v
           Term t -> case t of
-            Let a -> pure $ keyword "let" <+> name a
-            a :>> b -> do
-              prec <- ask @Prec
-              fore <- with 12 (go a)
-              aft  <- with 12 (go b)
-
-              let open  = symbol ("{" <> softline)
-                  close = symbol (softline <> "}")
-                  separator = ";" <> Pretty.line
-                  body = fore <> separator <> aft
-
-              pure . Pretty.align $ encloseIf (12 > prec) open close (Pretty.align body)
-
-            Lam n f -> inParens 11 $ do
-              (x, body) <- bind n f
-              pure (lambda <> name x <+> arrow <+> body)
-
-            Frame    -> pure $ primitive "frame"
-            Unit     -> pure $ primitive "unit"
-            Bool b   -> pure $ primitive (if b then "true" else "false")
-            String s -> pure . strlit $ Pretty.viaShow s
-
-            f :$ x -> inParens 11 $ (<+>) <$> go f <*> go x
-
-            If con tru fal -> do
-              con' <- "if"   `appending` go con
-              tru' <- "then" `appending` go tru
-              fal' <- "else" `appending` go fal
-              pure $ Pretty.sep [con', tru', fal']
-
-            Load p   -> "load" `appending` go p
-            Edge Lexical n -> "lexical" `appending` go n
-            Edge Import n -> "import" `appending` go n
-            item :. body   -> inParens 4 $ do
-              f <- go item
-              g <- go body
-              pure (f <> symbol "." <> g)
-
-            lhs := rhs -> inParens 3 $ do
-              f <- go lhs
-              g <- go rhs
-              pure (f <+> symbol "=" <+> g)
+            Rec (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep
+              [ keyword "rec" <+> name x
+              , symbol "=" <+> align (withPrec 0 (go (instantiate1 (pure (name x)) b)))
+              ]
+
+            Lam (Named (Ignored x) b) -> prec 3 . group . nest 2 $ vsep
+              [ lambda <> name x, arrow <+> withPrec 0 (go (instantiate1 (pure (name x)) b)) ]
+
+            Record fs -> atom . group . nest 2 $ vsep [ primitive "record", block ", " (map (uncurry keyValue) fs) ]
+
+            Unit     -> atom $ primitive "unit"
+            Bool b   -> atom $ primitive (if b then "true" else "false")
+            String s -> atom . strlit $ viaShow s
+
+            f :$ x -> prec 8 (withPrec 8 (go f) <+> withPrec 9 (go x))
+
+            If con tru fal -> prec 3 . group $ vsep
+              [ keyword "if"   <+> precBody (go con)
+              , keyword "then" <+> precBody (go tru)
+              , keyword "else" <+> precBody (go fal)
+              ]
+
+            Load p -> prec 3 (keyword "load" <+> withPrec 9 (go p))
+            item :. body -> prec 9 (withPrec 9 (go item) <> symbol "." <> name body)
+
+            lhs := rhs -> prec 3 . group . nest 2 $ vsep
+              [ withPrec 4 (go lhs)
+              , symbol "=" <+> align (withPrec 4 (go rhs))
+              ]
 
             -- Annotations are not pretty-printed, as it lowers the signal/noise ratio too profoundly.
             Ann _ c -> go c
-          where bind (Ignored x) f = (,) x <$> go (instantiate1 (pure x) f)
+            statement ->
+              let (bindings, return) = unstatements (Term statement)
+                  statements = toList (bindings :> (Nothing :<- return))
+                  names = zipWith (\ i (n :<- _) -> maybe (pretty @Int i) (name . namedName) n) [0..] statements
+                  statements' = map (prettyStatement names) statements
+              in atom (block "; " statements')
+        block _ [] = braces mempty
+        block s ss = encloseSep "{ " " }" s ss
+        keyValue x v = name x <+> symbol ":" <+> precBody (go v)
+        prettyStatement names (Just (Named (Ignored u) _) :<- t) = name u <+> arrowL <+> precBody (go (either (names !!) id <$> t))
+        prettyStatement names (Nothing                    :<- t) = precBody (go (either (names !!) id <$> t))
         lambda = case style of
           Unicode -> symbol "λ"
           Ascii   -> symbol "\\"
         arrow = case style of
           Unicode -> symbol "→"
           Ascii   -> symbol "->"
+        arrowL = case style of
+          Unicode -> symbol "←"
+          Ascii   -> symbol "<-"
+
+
+data Prec a = Prec
+  { precLevel :: Maybe Int
+  , precBody  :: a
+  }
+  deriving (Eq, Ord, Show)
+
+prec :: Int -> a -> Prec a
+prec = Prec . Just
 
+atom :: a -> Prec a
+atom = Prec Nothing
 
-appending :: Functor f => AnsiDoc -> f AnsiDoc -> f AnsiDoc
-appending k item = (keyword k <+>) <$> item
+withPrec :: Int -> Prec AnsiDoc -> AnsiDoc
+withPrec d (Prec d' a)
+  | maybe False (d >) d' = parens a
+  | otherwise            = a
diff --git a/semantic-core/src/Data/Name.hs b/semantic-core/src/Data/Name.hs
index d7f644669a..1de0ddc58d 100644
--- a/semantic-core/src/Data/Name.hs
+++ b/semantic-core/src/Data/Name.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE DeriveTraversable, ExistentialQuantification, FlexibleContexts, FlexibleInstances, GeneralizedNewtypeDeriving, LambdaCase, MultiParamTypeClasses, OverloadedLists, OverloadedStrings, StandaloneDeriving, TypeApplications, TypeOperators, UndecidableInstances #-}
+{-# LANGUAGE DeriveTraversable, LambdaCase, OverloadedLists #-}
 module Data.Name
 ( User
 , Named(..)
@@ -10,7 +10,6 @@ module Data.Name
 , reservedNames
 , isSimpleCharacter
 , needsQuotation
-, encloseIf
 ) where
 
 import qualified Data.Char as Char
@@ -45,18 +44,14 @@ instance Ord (Ignored a) where compare _ _ = EQ
 
 
 reservedNames :: HashSet String
-reservedNames = [ "#true", "#false", "let", "#frame", "if", "then", "else"
-                , "lexical", "import", "#unit", "load"]
+reservedNames = [ "#true", "#false", "if", "then", "else"
+                , "#unit", "load", "rec", "#record"]
 
 -- | Returns true if any character would require quotation or if the
 -- name conflicts with a Core primitive.
 needsQuotation :: User -> Bool
 needsQuotation u = HashSet.member (unpack u) reservedNames || Text.any (not . isSimpleCharacter) u
 
-encloseIf :: Monoid m => Bool -> m -> m -> m -> m
-encloseIf True  l r x = l <> x <> r
-encloseIf False _ _ x = x
-
 -- | A ‘simple’ character is, loosely defined, a character that is compatible
 -- with identifiers in most ASCII-oriented programming languages. This is defined
 -- as the alphanumeric set plus @$@ and @_@.
diff --git a/semantic-core/src/Data/Scope.hs b/semantic-core/src/Data/Scope.hs
index 3f591a2d22..63fa2ced12 100644
--- a/semantic-core/src/Data/Scope.hs
+++ b/semantic-core/src/Data/Scope.hs
@@ -6,12 +6,14 @@ module Data.Scope
 , Scope(..)
 , fromScope
 , toScope
-, bind1
-, bind
-, bindEither
+, abstract1
+, abstract
+, abstractEither
 , instantiate1
 , instantiate
 , instantiateEither
+, unprefix
+, unprefixEither
 ) where
 
 import Control.Applicative (liftA2)
@@ -20,6 +22,7 @@ import Control.Monad ((>=>), guard)
 import Control.Monad.Module
 import Control.Monad.Trans.Class
 import Data.Function (on)
+import Data.Stack
 
 data Incr a b
   = Z a
@@ -86,14 +89,14 @@ toScope = Scope . fmap (fmap pure)
 
 
 -- | Bind occurrences of a variable in a term, producing a term in which the variable is bound.
-bind1 :: (Applicative f, Eq a) => a -> f a -> Scope () f a
-bind1 n = bind (guard . (== n))
+abstract1 :: (Applicative f, Eq a) => a -> f a -> Scope () f a
+abstract1 n = abstract (guard . (== n))
 
-bind :: Applicative f => (b -> Maybe a) -> f b -> Scope a f b
-bind f = bindEither (matchMaybe f)
+abstract :: Applicative f => (b -> Maybe a) -> f b -> Scope a f b
+abstract f = abstractEither (matchMaybe f)
 
-bindEither :: Applicative f => (b -> Either a c) -> f b -> Scope a f c
-bindEither f = Scope . fmap (match f) -- FIXME: succ as little of the expression as possible, cf https://twitter.com/ollfredo/status/1145776391826358273
+abstractEither :: Applicative f => (b -> Either a c) -> f b -> Scope a f c
+abstractEither f = Scope . fmap (match f) -- FIXME: succ as little of the expression as possible, cf https://twitter.com/ollfredo/status/1145776391826358273
 
 
 -- | Substitute a term for the free variable in a given term, producing a closed term.
@@ -105,3 +108,25 @@ instantiate f = instantiateEither (either f pure)
 
 instantiateEither :: Monad f => (Either a b -> f c) -> Scope a f b -> f c
 instantiateEither f = unScope >=> incr (f . Left) (>>= f . Right)
+
+
+-- | Unwrap a (possibly-empty) prefix of @a@s wrapping a @t@ using a helper function.
+--
+--   This allows us to peel a prefix of syntax, typically binders, off of a term, returning a stack of prefixing values (e.g. variables) and the outermost subterm rejected by the function.
+unprefix
+  :: (Int -> t -> Maybe (a, t)) -- ^ A function taking the 0-based index into the prefix & the current term, and optionally returning a pair of the prefixing value and the inner subterm.
+  -> t                          -- ^ The initial term.
+  -> (Stack a, t)               -- ^ A stack of prefixing values & the final subterm.
+unprefix from = unprefixEither (matchMaybe . from)
+
+-- | Unwrap a (possibly-empty) prefix of @a@s wrapping a @b@ within a @t@ using a helper function.
+--
+--   Compared to 'unprefix', this allows the helper function to extract inner terms of a different type, for example when @t@ is a right @b@-module.
+unprefixEither
+  :: (Int -> t -> Either (a, t) b) -- ^ A function taking the 0-based index into the prefix & the current term, and returning either a pair of the prefixing value and the next inner subterm of type @t@, or the final inner subterm of type @b@.
+  -> t                             -- ^ The initial term.
+  -> (Stack a, b)                  -- ^ A stack of prefixing values & the final subterm.
+unprefixEither from = go (0 :: Int) Nil
+  where go i bs t = case from i t of
+          Left (b, t) -> go (succ i) (bs :> b) t
+          Right b     -> (bs, b)
diff --git a/semantic-core/test/Generators.hs b/semantic-core/test/Generators.hs
index 667830b956..3ec79e8bef 100644
--- a/semantic-core/test/Generators.hs
+++ b/semantic-core/test/Generators.hs
@@ -6,8 +6,10 @@ module Generators
   , variable
   , boolean
   , lambda
+  , record
   , apply
   , ifthenelse
+  , expr
   ) where
 
 import Prelude hiding (span)
@@ -16,7 +18,7 @@ import Hedgehog hiding (Var)
 import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
 
-import Data.Core
+import qualified Data.Core as Core
 import Data.Name
 import Data.Term
 
@@ -24,34 +26,51 @@ import Data.Term
 -- fresh names for variables, since the length of variable names is not an
 -- interesting property as they parse regardless.
 name :: MonadGen m => m (Named User)
-name = Gen.prune ((Named . Ignored <*> id) <$> names) where
+name = Gen.prune (named' <$> names) where
   names = Gen.text (Range.linear 1 10) Gen.lower
 
-boolean :: MonadGen m => m (Term Core User)
-boolean = bool <$> Gen.bool
+boolean :: MonadGen m => m (Term Core.Core User)
+boolean = Core.bool <$> Gen.bool
 
-variable :: MonadGen m => m (Term Core User)
+variable :: MonadGen m => m (Term Core.Core User)
 variable = pure . namedValue <$> name
 
-ifthenelse :: MonadGen m => m (Term Core User) -> m (Term Core User)
-ifthenelse bod = Gen.subterm3 boolean bod bod if'
+ifthenelse :: MonadGen m => m (Term Core.Core User) -> m (Term Core.Core User)
+ifthenelse bod = Gen.subterm3 boolean bod bod Core.if'
 
-apply :: MonadGen m => m (Term Core User) -> m (Term Core User)
+apply :: MonadGen m => m (Term Core.Core User) -> m (Term Core.Core User)
 apply gen = go where
   go = Gen.recursive
     Gen.choice
-    [ Gen.subterm2 gen gen ($$)]
-    [ Gen.subterm2 go go ($$)  -- balanced
-    , Gen.subtermM go (\x -> lam <$> name <*> pure x)
+    [ Gen.subterm2 gen gen (Core.$$)]
+    [ Gen.subterm2 go go (Core.$$)  -- balanced
+    , Gen.subtermM go (\x -> Core.lam <$> name <*> pure x)
     ]
 
-lambda :: MonadGen m => m (Term Core User) -> m (Term Core User)
+lambda :: MonadGen m => m (Term Core.Core User) -> m (Term Core.Core User)
 lambda bod = do
   arg <- name
-  Gen.subterm bod (lam arg)
+  Gen.subterm bod (Core.lam arg)
 
-atoms :: MonadGen m => [m (Term Core User)]
-atoms = [boolean, variable, pure unit, pure frame]
+record :: MonadGen m => m (Term Core.Core User) -> m (Term Core.Core User)
+record bod = Core.record <$> Gen.list (Range.linear 0 5) ((,) . namedValue <$> name <*> bod)
 
-literal :: MonadGen m => m (Term Core User)
-literal = Gen.recursive Gen.choice atoms [lambda literal]
+atoms :: MonadGen m => [m (Term Core.Core User)]
+atoms = [variable, pure Core.unit, boolean, Core.string <$> Gen.text (Range.linear 1 10) Gen.lower]
+
+literal :: MonadGen m => m (Term Core.Core User)
+literal = Gen.recursive Gen.choice atoms [lambda literal, record literal]
+
+expr :: MonadGen m => m (Term Core.Core User)
+expr = Gen.recursive Gen.choice atoms
+  [ Gen.subtermM expr (\x -> flip Core.rec x <$> name)
+  , Gen.subterm2 expr expr (Core.>>>)
+  , Gen.subtermM2 expr expr (\ x y -> (Core.>>>= y) . (Core.:<- x) <$> name)
+  , lambda expr
+  , Gen.subterm2 expr expr (Core.$$)
+  , Gen.subterm3 expr expr expr Core.if'
+  , Gen.subterm expr Core.load
+  , record expr
+  , Gen.subtermM expr (\ x -> (x Core....) . namedValue <$> name)
+  , Gen.subterm2 expr expr (Core..=)
+  ]
diff --git a/semantic-core/test/Spec.hs b/semantic-core/test/Spec.hs
index 6680cd7505..b877a4a1ef 100644
--- a/semantic-core/test/Spec.hs
+++ b/semantic-core/test/Spec.hs
@@ -41,6 +41,7 @@ parserProps = testGroup "Parsing: roundtripping"
   , testProperty "if/then/else" . prop_roundtrips . Gen.ifthenelse $ Gen.variable
   , testProperty "lambda" . prop_roundtrips $ Gen.lambda Gen.literal
   , testProperty "function application" . prop_roundtrips $ Gen.apply Gen.variable
+  , testProperty "expressions" . prop_roundtrips $ Gen.expr
   ]
 
 -- * Parser specs
@@ -68,7 +69,7 @@ assert_application_left_associative :: Assertion
 assert_application_left_associative = "f g h" `parsesInto` (f $$ g $$ h)
 
 assert_push_left_associative :: Assertion
-assert_push_left_associative = "f.g.h" `parsesInto` (f ... g ... h)
+assert_push_left_associative = "f.g.h" `parsesInto` (f ... "g" ... "h")
 
 assert_ascii_lambda_parse :: Assertion
 assert_ascii_lambda_parse = "\\a -> a" `parsesInto` lam (named' "a") a
@@ -79,12 +80,6 @@ assert_unicode_lambda_parse = "λa → a" `parsesInto` lam (named' "a") a
 assert_quoted_name_parse :: Assertion
 assert_quoted_name_parse = "#{(NilClass)}" `parsesInto` pure "(NilClass)"
 
-assert_let_dot_precedence :: Assertion
-assert_let_dot_precedence = "let a = f.g.h" `parsesInto` (let' "a" .= (f ... g ... h))
-
-assert_let_in_push_precedence :: Assertion
-assert_let_in_push_precedence = "f.let g = h" `parsesInto` (f ... (let' "g" .= h))
-
 parserSpecs :: TestTree
 parserSpecs = testGroup "Parsing: simple specs"
   [ testCase "true/false" assert_booleans_parse
@@ -95,12 +90,12 @@ parserSpecs = testGroup "Parsing: simple specs"
   , testCase "lambda with ASCII syntax" assert_ascii_lambda_parse
   , testCase "lambda with unicode syntax" assert_unicode_lambda_parse
   , testCase "quoted names" assert_quoted_name_parse
-  , testCase "let + dot precedence" assert_let_dot_precedence
-  , testCase "let in push" assert_let_in_push_precedence
   ]
 
 assert_roundtrips :: File (Term Core User) -> Assertion
-assert_roundtrips (File _ core) = parseEither Parse.core (showCore core) @?= Right (stripAnnotations core)
+assert_roundtrips (File _ core) = case parseEither Parse.core (showCore core) of
+  Right v -> v @?= stripAnnotations core
+  Left e -> assertFailure e
 
 parserExamples :: TestTree
 parserExamples = testGroup "Parsing: Eval.hs examples"