diff --git a/app/Compiler.hs b/app/Compiler.hs
index 08e4b24..4f94637 100644
--- a/app/Compiler.hs
+++ b/app/Compiler.hs
@@ -1,5 +1,7 @@
 module Compiler where
 
+import Data.Char (isUpper)
+import Data.Containers.ListUtils (nubOrd)
 import Data.List
 import Interpreter (Code, Datum(..), Id(..), Instr(..), StrTable, strtablize)
 
@@ -10,13 +12,29 @@ data PrlgStr
 
 data PrlgInt
   = CallI Id [PrlgInt]
-  | LiteralI Int --split off vars here later
+  | LiteralI Int
+  | VarI Int Int
+  | VoidI
   deriving (Show)
 
-strtablizePrlg :: StrTable -> PrlgStr -> (StrTable, PrlgInt)
-strtablizePrlg = go
+varname :: String -> Bool
+varname ('_':_) = True
+varname (c:_) = isUpper c
+varname _ = False
+
+varnames :: PrlgStr -> [String]
+varnames (CallS _ xs) = nubOrd $ concatMap varnames xs
+varnames (LiteralS x)
+  | varname x = [x]
+  | otherwise = []
+
+strtablizePrlg :: [String] -> StrTable -> PrlgStr -> (StrTable, PrlgInt)
+strtablizePrlg stab = go
   where
-    go t (LiteralS str) = LiteralI <$> strtablize t str
+    go t (LiteralS str)
+      | str == "_" = (t, VoidI)
+      | Just idx <- elemIndex str stab = VarI idx <$> strtablize t str
+      | otherwise = LiteralI <$> strtablize t str
     go t (CallS str ps) =
       let (t', i) = strtablize t str
        in CallI (Id i $ length ps) <$> mapAccumL go t' ps
@@ -35,6 +53,8 @@ compileGoal x = compileArg x
 compileArg :: PrlgInt -> Code
 compileArg (CallI x args) = U (Struct x) : concatMap compileArg args
 compileArg (LiteralI x) = [U (Atom x)]
+compileArg (VarI x _) = [U (LocalRef x)]
+compileArg VoidI = [U VoidRef]
 
 seqGoals :: [Code] -> Code
 seqGoals [] = [NoGoal]
diff --git a/app/Frontend.hs b/app/Frontend.hs
index 2be4f68..2c92e1f 100644
--- a/app/Frontend.hs
+++ b/app/Frontend.hs
@@ -66,7 +66,8 @@ interpret = (>> return True) . lex
         Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err
         Right prlg -> intern prlg
     intern prlgs = do
-      prlgi <- withStrTable $ flip C.strtablizePrlg prlgs
+      prlgi <-
+        withStrTable $ \st -> C.strtablizePrlg (C.varnames prlgs) st prlgs
       compile prlgi
     compile prlgi
       {- TODO: switch between prove goal/compile clause here -}
@@ -93,18 +94,23 @@ addBuiltins = do
   c <- findAtom "c"
   b0 <- findStruct "b" 0
   any <- findStruct "any" 1
+  eq <- findStruct "=" 2
   modify $ \s ->
     s
       { defs =
           M.fromList
-            [ (a1, [[I.U (I.Atom a), I.NoGoal], [I.U (I.Atom b), I.NoGoal]])
+            [ (eq, [[I.U (I.LocalRef 0),I.U (I.LocalRef 0), I.NoGoal]])
+            , (a1, [[I.U (I.Atom a), I.NoGoal], [I.U (I.Atom b), I.NoGoal]])
             , ( b0
               , [ [I.Goal, I.U (I.Struct a1), I.U (I.Atom c), I.LastCall]
                 , [I.Goal, I.U (I.Struct a1), I.U (I.Atom b), I.LastCall]
                 ])
-            , (any, [[I.U I.VoidVar, I.NoGoal]])
+            , (any, [[I.U I.VoidRef, I.NoGoal]])
             ]
-      , ops = [(",", P.Op 1000 $ P.Infix P.X P.Y)]
+      , ops =
+        [ (",", P.Op 1000 $ P.Infix P.X P.Y)
+        , ("=", P.Op 700 $ P.Infix P.X P.X)
+        ]
       }
 
 interpreterStart :: PrlgEnv ()
diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index 6a80232..b42f079 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -25,7 +25,7 @@ data Id =
 data Datum
   = Atom Int -- unifies a constant
   | Struct Id -- unifies a structure with arity
-  | VoidVar -- in code this unifies with anything; everywhere else this is an unbound variable
+  | VoidRef -- in code this unifies with anything; everywhere else this is an unbound variable
   | LocalRef Int -- local variable idx
   | HeapRef Int -- heap structure idx
   deriving (Show, Eq, Ord)
@@ -47,7 +47,7 @@ data Heap =
   Heap Int (M.Map Int Datum)
   deriving (Show)
 
-emptyHeap = Heap 1 M.empty
+emptyHeap = Heap 0 M.empty
 
 type Scope = M.Map Int Int
 
@@ -154,35 +154,22 @@ proveStep c f i = go i
                 m'
            in cont (map HeapRef $ tail addrs) (Heap nxt' m'')
         {- simple cases first -}
-        unify VoidVar VoidVar = uok
+        unify VoidRef VoidRef = uok
         unify (Atom a) (Atom b)
           | a == b = uok
-        unify VoidVar (Atom _) = uok
-        unify (Atom _) VoidVar = uok
+        unify VoidRef (Atom _) = uok
+        unify (Atom _) VoidRef = uok
         unify (Struct a) (Struct b)
           | a == b = uok
         {- unifying a struct with void must cause us to skip the void -}
-        unify VoidVar (Struct Id {arity = a}) =
-          c i {cur = cur {hed = replicate a (U VoidVar) ++ hs, gol = gs}}
-        unify (Struct Id {arity = a}) VoidVar =
-          c i {cur = cur {hed = hs, gol = replicate a (U VoidVar) ++ gs}}
+        unify VoidRef (Struct Id {arity = a}) =
+          c i {cur = cur {hed = replicate a (U VoidRef) ++ hs, gol = gs}}
+        unify (Struct Id {arity = a}) VoidRef =
+          c i {cur = cur {hed = hs, gol = replicate a (U VoidRef) ++ gs}}
         {- handle local refs; first ignore their combination with voids to save memory -}
-        unify (LocalRef _) VoidVar = uok
-        unify VoidVar (LocalRef _) = uok
+        unify (LocalRef _) VoidRef = uok
+        unify VoidRef (LocalRef _) = uok
         {- allocate heap for LocalRefs and retry with HeapRefs -}
-        unify (LocalRef hv) (LocalRef gv) =
-          allocLocal gv (gvar cur) $ \gvar' heap' addr ->
-            c
-              i
-                { cur =
-                    cur
-                      { hed = U (HeapRef addr) : hs
-                      , hvar = M.insert hv addr (hvar cur)
-                      , gol = U (HeapRef addr) : gs
-                      , gvar = gvar'
-                      , heap = heap'
-                      }
-                }
         unify (LocalRef hv) _ =
           allocLocal hv (hvar cur) $ \hvar' heap' addr ->
             c
@@ -200,8 +187,8 @@ proveStep c f i = go i
                       {gol = U (HeapRef addr) : gs, gvar = gvar', heap = heap'}
                 }
         {- handle heap refs; first ignore their combination with voids again -}
-        unify (HeapRef _) VoidVar = uok
-        unify VoidVar (HeapRef _) = uok
+        unify (HeapRef _) VoidRef = uok
+        unify VoidRef (HeapRef _) = uok
         {- actual HeapRefs, these are dereferenced and then unified; decide between copying and linking -}
         unify (HeapRef hr') g =
           case deref hr' of