diff --git a/app/Builtins.hs b/app/Builtins.hs
index 272eca2..b4d6b8d 100644
--- a/app/Builtins.hs
+++ b/app/Builtins.hs
@@ -19,13 +19,13 @@ addBuiltins = do
     s
       { defs =
           M.fromList
-            [ (eq, [[U (LocalRef 0), U (LocalRef 0), NoGoal]])
+            [ (eq, [[U (LocalRef 0 Nothing), U (LocalRef 0 Nothing), NoGoal]])
             , (a1, [[U (Atom a), NoGoal], [U (Atom b), NoGoal]])
             , ( b0
               , [ [Goal, U (Struct a1), U (Atom c), LastCall]
                 , [Goal, U (Struct a1), U (Atom b), LastCall]
                 ])
-            , (any, [[U VoidRef, NoGoal]])
+            , (any, [[U (VoidRef Nothing), NoGoal]])
             ]
       , ops = [(O.xfy "," 1000), (O.xfx "=" 700)]
       }
diff --git a/app/Code.hs b/app/Code.hs
index 3488f0b..94e8ce3 100644
--- a/app/Code.hs
+++ b/app/Code.hs
@@ -6,9 +6,9 @@ import IR (Id(..))
 data Datum
   = Atom Int -- unifies a constant
   | Struct Id -- unifies a structure with arity
-  | VoidRef -- unifies with anything
-  | LocalRef Int -- code-local variable idx (should not occur on heap)
-  | HeapRef Int -- heap structure idx
+  | VoidRef (Maybe Int) -- unifies with anything (references may refer to variable names)
+  | LocalRef Int (Maybe Int) -- code-local variable idx (should not occur on heap)
+  | HeapRef Int (Maybe Int) -- heap structure idx
   deriving (Show, Eq, Ord)
 
 data Instr
diff --git a/app/Compiler.hs b/app/Compiler.hs
index b3294a1..e9bd7f4 100644
--- a/app/Compiler.hs
+++ b/app/Compiler.hs
@@ -3,31 +3,38 @@ module Compiler where
 import Data.Char (isUpper)
 import Data.Containers.ListUtils (nubOrd)
 import Data.List
+import qualified Data.Map as M
 
 import Code (Code, Datum(..), Instr(..))
-import IR (Id(..), PrlgInt(..), PrlgStr(..), StrTable, strtablize)
+import IR (Id(..), PrlgInt(..), PrlgStr(..), StrTable(..), strtablize)
+
+internPrlg :: StrTable -> PrlgStr -> (StrTable, PrlgInt)
+internPrlg = go
+  where
+    go t (LiteralS str) = 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
 
 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]
+varIds :: StrTable -> PrlgInt -> [Int]
+varIds st (CallI _ xs) = nubOrd $ concatMap (varIds st) xs
+varIds (StrTable _ _ st) (LiteralI x)
+  | Just s <- st M.!? x
+  , varname s = [x]
   | otherwise = []
 
-internPrlg :: [String] -> StrTable -> PrlgStr -> (StrTable, PrlgInt)
-internPrlg stab = go
-  where
-    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
+variablizePrlg :: Int -> [Int] -> PrlgInt -> PrlgInt
+variablizePrlg void vs (CallI id ps) =
+  CallI id $ map (variablizePrlg void vs) ps
+variablizePrlg void vs (LiteralI i)
+  | i == void = VoidI i
+  | Just idx <- elemIndex i vs = VarI idx i
+  | otherwise = LiteralI i
 
 compileGoals :: Id -> PrlgInt -> [Code]
 compileGoals andop = go
@@ -43,8 +50,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]
+compileArg (VarI x i) = [U (LocalRef x $ Just i)]
+compileArg (VoidI i) = [U (VoidRef $ Just i)]
 
 seqGoals :: [Code] -> Code
 seqGoals [] = [NoGoal]
@@ -52,13 +59,3 @@ seqGoals [[Cut]] = [Cut, NoGoal]
 seqGoals [x] = [Goal] ++ x ++ [LastCall]
 seqGoals [x, [Cut]] = [Goal] ++ x ++ [LastCall, Cut]
 seqGoals (x:xs) = [Goal] ++ x ++ [Call] ++ seqGoals xs
-
-compileClause :: Id -> Id -> PrlgInt -> Code
-compileClause proveop andop = go
-  where
-    go :: PrlgInt -> Code
-    go h@(CallI x args)
-      | x == proveop
-      , [head, goals] <- args =
-        compileGoal head ++ seqGoals (compileGoals andop goals)
-      | otherwise = compileGoal h ++ seqGoals []
diff --git a/app/Frontend.hs b/app/Frontend.hs
index a17a85c..1adf39b 100644
--- a/app/Frontend.hs
+++ b/app/Frontend.hs
@@ -45,13 +45,15 @@ interpret = (>> return True) . lex
         Left err -> liftIO $ putStrLn $ "expression parsing: " ++ err
         Right prlg -> intern prlg
     intern prlgs = do
-      prlgi <- withStrTable $ \st -> C.internPrlg (C.varnames prlgs) st prlgs
-      compile prlgi
-    compile prlgi
-      {- TODO: switch between prove goal/compile clause here -}
-     = do
+      prlgi <- withStrTable $ \st -> C.internPrlg st prlgs
+      underscore <- findAtom "_"
+      prlgv <-
+        withStrTable $ \st ->
+          (st, C.variablizePrlg underscore (C.varIds st prlgi) prlgi)
+      compile prlgv
+    compile prlgv = do
       commaId <- findStruct "," 2
-      let code = C.seqGoals $ C.compileGoals commaId prlgi
+      let code = C.seqGoals $ C.compileGoals commaId prlgv
       execute code
     execute code = do
       ds <- gets defs
diff --git a/app/IR.hs b/app/IR.hs
index 50c7493..e1aa9ba 100644
--- a/app/IR.hs
+++ b/app/IR.hs
@@ -18,7 +18,7 @@ data PrlgInt
   = CallI Id [PrlgInt]
   | LiteralI Int
   | VarI Int Int
-  | VoidI
+  | VoidI Int
   deriving (Show)
 
 data StrTable =
diff --git a/app/Interpreter.hs b/app/Interpreter.hs
index c29b701..da00301 100644
--- a/app/Interpreter.hs
+++ b/app/Interpreter.hs
@@ -63,7 +63,7 @@ proveStep c f i = go i
         {- heap tools -}
         deref x =
           case hmap M.!? x of
-            Just (HeapRef x') ->
+            Just (HeapRef x' _) ->
               if x == x'
                 then FreeRef x'
                 else deref x'
@@ -74,7 +74,7 @@ proveStep c f i = go i
         newHeapVars n (Heap nxt m) =
           let addrs = [nxt + i - 1 | i <- [1 .. n]]
            in ( Heap (nxt + n) $
-                foldr (uncurry M.insert) m $ zip addrs (map HeapRef addrs)
+                foldr (uncurry M.insert) m [(a, HeapRef a Nothing) | a <- addrs]
               , addrs)
         allocLocal reg scope cont
           | Just addr <- scope M.!? reg = cont scope heap addr
@@ -83,47 +83,62 @@ proveStep c f i = go i
         newHeapStruct addr s@(Struct Id {arity = arity}) cont =
           let (Heap nxt' m', addrs) = newHeapVars (arity + 1) heap
               m'' =
-                M.insert addr (HeapRef $ head addrs) . M.insert (head addrs) s $
+                M.insert addr (HeapRef (head addrs) Nothing) .
+                M.insert (head addrs) s $
                 m'
-           in cont (map HeapRef $ tail addrs) (Heap nxt' m'')
+           in cont [HeapRef a Nothing | a <- tail addrs] (Heap nxt' m'')
         {- simple cases first -}
-        unify VoidRef VoidRef = uok
+        unify (VoidRef _) (VoidRef _) = uok
         unify (Atom a) (Atom b)
           | a == b = uok
-        unify VoidRef (Atom _) = uok
-        unify (Atom _) VoidRef = 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 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}}
+        unify (VoidRef _) (Struct Id {arity = a}) =
+          c
+            i
+              { cur =
+                  cur {hed = replicate a (U $ VoidRef Nothing) ++ hs, gol = gs}
+              }
+        unify (Struct Id {arity = a}) (VoidRef _) =
+          c
+            i
+              { cur =
+                  cur {hed = hs, gol = replicate a (U $ VoidRef Nothing) ++ gs}
+              }
         {- handle local refs; first ignore their combination with voids to save memory -}
-        unify (LocalRef _) VoidRef = uok
-        unify VoidRef (LocalRef _) = uok
+        unify (LocalRef _ _) (VoidRef _) = uok
+        unify (VoidRef _) (LocalRef _ _) = uok
         {- allocate heap for LocalRefs and retry with HeapRefs -}
-        unify (LocalRef hv) _ =
+        unify (LocalRef hv ident) _ =
           allocLocal hv (hvar cur) $ \hvar' heap' addr ->
             c
               i
                 { cur =
                     cur
-                      {hed = U (HeapRef addr) : hs, hvar = hvar', heap = heap'}
+                      { hed = U (HeapRef addr ident) : hs
+                      , hvar = hvar'
+                      , heap = heap'
+                      }
                 }
-        unify _ (LocalRef gv) =
+        unify _ (LocalRef gv ident) =
           allocLocal gv (gvar cur) $ \gvar' heap' addr ->
             c
               i
                 { cur =
                     cur
-                      {gol = U (HeapRef addr) : gs, gvar = gvar', heap = heap'}
+                      { gol = U (HeapRef addr ident) : gs
+                      , gvar = gvar'
+                      , heap = heap'
+                      }
                 }
         {- handle heap refs; first ignore their combination with voids again -}
-        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 =
+        unify (HeapRef _ _) (VoidRef _) = uok
+        unify (VoidRef _) (HeapRef _ _) = uok
+        {- actual HeapRefs, these are dereferenced and then unified (sometimes with copying) -}
+        unify (HeapRef hr' hident) g =
           case deref hr' of
             FreeRef hr ->
               case g of
@@ -139,10 +154,10 @@ proveStep c f i = go i
                                cur
                                  {hed = map U nhs ++ hs, gol = gs, heap = nheap}
                            })
-                HeapRef gr' ->
+                HeapRef gr' _ ->
                   case deref gr' of
-                    FreeRef gr -> setHeap hr (HeapRef gr)
-                    BoundRef addr _ -> setHeap hr (HeapRef addr)
+                    FreeRef gr -> setHeap hr (HeapRef gr hident)
+                    BoundRef addr _ -> setHeap hr (HeapRef addr hident)
                     _ -> ifail "dangling goal ref (from head ref)"
             BoundRef _ atom@(Atom a) -> unify atom g
             BoundRef addr struct@(Struct Id {arity = arity}) ->
@@ -152,12 +167,13 @@ proveStep c f i = go i
                       cur
                         { hed =
                             U struct :
-                            [U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ hs
+                            [U (HeapRef (addr + i) Nothing) | i <- [1 .. arity]] ++
+                            hs
                         , gol = U g : gs
                         }
                   }
             _ -> ifail "dangling head ref"
-        unify h (HeapRef gr') =
+        unify h (HeapRef gr' gident) =
           case deref gr' of
             FreeRef gr ->
               case h of
@@ -182,7 +198,8 @@ proveStep c f i = go i
                         { hed = U h : hs
                         , gol =
                             U struct :
-                            [U (HeapRef $ addr + i) | i <- [1 .. arity]] ++ gs
+                            [U (HeapRef (addr + i) Nothing) | i <- [1 .. arity]] ++
+                            gs
                         }
                   }
             _ -> ifail "dangling goal ref"