diff --git a/src/Juvix/Compiler/Asm/Data/InfoTable.hs b/src/Juvix/Compiler/Asm/Data/InfoTable.hs
index 230ce86794..2c957fe666 100644
--- a/src/Juvix/Compiler/Asm/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Asm/Data/InfoTable.hs
@@ -25,6 +25,8 @@ data FunctionInfo = FunctionInfo
     -- (_functionType))` only if it is 0 (the "function" takes zero arguments)
     -- and the result is a function.
     _functionArgsNum :: Int,
+    -- | length _functionArgNames == _functionArgsNum
+    _functionArgNames :: [Maybe Text],
     _functionType :: Type,
     _functionMaxValueStackHeight :: Int,
     _functionMaxTempStackHeight :: Int,
@@ -39,6 +41,8 @@ data ConstructorInfo = ConstructorInfo
     -- (_constructorType))`. It is stored separately mainly for the benefit of
     -- the interpreter (so it does not have to recompute it every time).
     _constructorArgsNum :: Int,
+    -- | length _constructorArgNames == _constructorArgsNum
+    _constructorArgNames :: [Maybe Text],
     -- | Constructor types are assumed to be fully uncurried, i.e., `uncurryType
     -- _constructorType == _constructorType`
     _constructorType :: Type,
diff --git a/src/Juvix/Compiler/Asm/Extra/Memory.hs b/src/Juvix/Compiler/Asm/Extra/Memory.hs
index b5fb257aa0..22beba8f24 100644
--- a/src/Juvix/Compiler/Asm/Extra/Memory.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Memory.hs
@@ -98,10 +98,10 @@ getDirectRefType :: DirectRef -> Memory -> Maybe Type
 getDirectRefType dr mem = case dr of
   StackRef ->
     topValueStack 0 mem
-  ArgRef off ->
-    getArgumentType off mem
-  TempRef off ->
-    bottomTempStack off mem
+  ArgRef OffsetRef {..} ->
+    getArgumentType _offsetRefOffset mem
+  TempRef OffsetRef {..} ->
+    bottomTempStack _offsetRefOffset mem
 
 getValueType' :: (Member (Error AsmError) r) => Maybe Location -> InfoTable -> Memory -> Value -> Sem r Type
 getValueType' loc tab mem = \case
diff --git a/src/Juvix/Compiler/Asm/Extra/Recursors.hs b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
index f0b9c4594b..cf46bf0227 100644
--- a/src/Juvix/Compiler/Asm/Extra/Recursors.hs
+++ b/src/Juvix/Compiler/Asm/Extra/Recursors.hs
@@ -18,7 +18,8 @@ data RecursorSig m r a = RecursorSig
   { _recursorInfoTable :: InfoTable,
     _recurseInstr :: m -> CmdInstr -> Sem r a,
     _recurseBranch :: m -> CmdBranch -> [a] -> [a] -> Sem r a,
-    _recurseCase :: m -> CmdCase -> [[a]] -> Maybe [a] -> Sem r a
+    _recurseCase :: m -> CmdCase -> [[a]] -> Maybe [a] -> Sem r a,
+    _recurseSave :: m -> CmdSave -> [a] -> Sem r a
   }
 
 makeLenses ''RecursorSig
@@ -43,6 +44,8 @@ recurse' sig = go True
           goNextCmd isTail (x ^. (cmdBranchInfo . commandInfoLocation)) (goBranch (isTail && null t) mem x) t
         Case x ->
           goNextCmd isTail (x ^. (cmdCaseInfo . commandInfoLocation)) (goCase (isTail && null t) mem x) t
+        Save x ->
+          goNextCmd isTail (x ^. (cmdSaveInfo . commandInfoLocation)) (goSave (isTail && null t) mem x) t
 
     goNextCmd :: Bool -> Maybe Location -> Sem r (Memory, a) -> Code -> Sem r (Memory, [a])
     goNextCmd isTail loc mp t = do
@@ -104,16 +107,6 @@ recurse' sig = go True
                 throw $
                   AsmError loc "popping empty value stack"
               return (popValueStack 1 mem)
-            PushTemp -> do
-              when (null (mem ^. memoryValueStack)) $
-                throw $
-                  AsmError loc "popping empty value stack"
-              return $ pushTempStack (topValueStack' 0 mem) (popValueStack 1 mem)
-            PopTemp -> do
-              when (null (mem ^. memoryTempStack)) $
-                throw $
-                  AsmError loc "popping empty temporary stack"
-              return $ popTempStack 1 mem
             Trace ->
               return mem
             Dump ->
@@ -275,6 +268,27 @@ recurse' sig = go True
       where
         loc = cmd ^. (cmdCaseInfo . commandInfoLocation)
 
+    goSave :: Bool -> Memory -> CmdSave -> Sem r (Memory, a)
+    goSave isTail mem cmd@CmdSave {..} = do
+      when (null (mem ^. memoryValueStack)) $
+        throw $
+          AsmError loc "popping empty value stack"
+      let mem1 = pushTempStack (topValueStack' 0 mem) (popValueStack 1 mem)
+      (mem2, a) <- go isTail mem1 _cmdSaveCode
+      a' <- (sig ^. recurseSave) mem cmd a
+      when (not isTail && _cmdSaveIsTail) $
+        throw $
+          AsmError loc "'tsave' not in tail position"
+      when (isTail && not _cmdSaveIsTail) $
+        throw $
+          AsmError loc "'save' in tail position"
+      when (not isTail && null (mem2 ^. memoryTempStack)) $
+        throw $
+          AsmError loc "popping empty temporary stack"
+      return (if isTail then mem2 else popTempStack 1 mem2, a')
+      where
+        loc = _cmdSaveInfo ^. commandInfoLocation
+
     checkBranchInvariant :: Int -> Maybe Location -> Memory -> Memory -> Sem r ()
     checkBranchInvariant k loc mem mem' = do
       unless (length (mem' ^. memoryValueStack) == length (mem ^. memoryValueStack) + k) $
@@ -320,6 +334,8 @@ recurseS' sig = go
           goNextCmd (goBranch si x) t
         Case x ->
           goNextCmd (goCase si x) t
+        Save x ->
+          goNextCmd (goSave si x) t
 
     goNextCmd :: Sem r (StackInfo, a) -> Code -> Sem r (StackInfo, [a])
     goNextCmd mp t = do
@@ -362,10 +378,6 @@ recurseS' sig = go
               return (stackInfoPushValueStack 1 si)
             Pop -> do
               return (stackInfoPopValueStack 1 si)
-            PushTemp -> do
-              return $ stackInfoPushTempStack 1 (stackInfoPopValueStack 1 si)
-            PopTemp -> do
-              return $ stackInfoPopTempStack 1 si
             Trace ->
               return si
             Dump ->
@@ -436,6 +448,14 @@ recurseS' sig = go
       where
         loc = cmd ^. (cmdCaseInfo . commandInfoLocation)
 
+    goSave :: StackInfo -> CmdSave -> Sem r (StackInfo, a)
+    goSave si cmd@CmdSave {..} = do
+      let si1 = stackInfoPushTempStack 1 (stackInfoPopValueStack 1 si)
+      (si2, c) <- go si1 _cmdSaveCode
+      c' <- (sig ^. recurseSave) si cmd c
+      let si' = if _cmdSaveIsTail then si2 else stackInfoPopTempStack 1 si2
+      return (si', c')
+
     checkStackInfo :: Maybe Location -> StackInfo -> StackInfo -> Sem r ()
     checkStackInfo loc si1 si2 =
       when (si1 /= si2) $
@@ -463,7 +483,8 @@ data FoldSig m r a = FoldSig
     _foldAdjust :: a -> a,
     _foldInstr :: m -> CmdInstr -> a -> Sem r a,
     _foldBranch :: m -> CmdBranch -> a -> a -> a -> Sem r a,
-    _foldCase :: m -> CmdCase -> [a] -> Maybe a -> a -> Sem r a
+    _foldCase :: m -> CmdCase -> [a] -> Maybe a -> a -> Sem r a,
+    _foldSave :: m -> CmdSave -> a -> a -> Sem r a
   }
 
 makeLenses ''FoldSig
@@ -499,6 +520,13 @@ foldS' sig si code acc = do
                     Just d -> Just <$> compose' d a'
                     Nothing -> return Nothing
                   (sig ^. foldCase) s cmd as ad a
+              ),
+          _recurseSave = \s cmd br ->
+            return
+              ( \a -> do
+                  let a' = (sig ^. foldAdjust) a
+                  a'' <- compose' br a'
+                  (sig ^. foldSave) s cmd a'' a
               )
         }
 
diff --git a/src/Juvix/Compiler/Asm/Interpreter.hs b/src/Juvix/Compiler/Asm/Interpreter.hs
index 1ff9607fb9..68015e2be3 100644
--- a/src/Juvix/Compiler/Asm/Interpreter.hs
+++ b/src/Juvix/Compiler/Asm/Interpreter.hs
@@ -61,6 +61,15 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
             _ -> case def of
               Just x -> goCode x
               Nothing -> runtimeError "no matching branch"
+      Save CmdSave {..} -> do
+        registerLocation (_cmdSaveInfo ^. commandInfoLocation)
+        v <- popValueStack
+        pushTempStack v
+        if
+            | _cmdSaveIsTail ->
+                goCode _cmdSaveCode
+            | otherwise ->
+                goCode _cmdSaveCode >> popTempStack >> goCode cont
 
     goInstr :: (Member Runtime r) => Maybe Location -> Instruction -> Code -> Sem r ()
     goInstr loc instr cont = case instr of
@@ -109,12 +118,6 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
         goCode cont
       Pop ->
         popValueStack >> goCode cont
-      PushTemp -> do
-        v <- popValueStack
-        pushTempStack v
-        goCode cont
-      PopTemp ->
-        popTempStack >> goCode cont
       Trace -> do
         v <- topValueStack
         logMessage (printVal v)
@@ -225,8 +228,8 @@ runCodeR infoTable funInfo = goCode (funInfo ^. functionCode) >> popLastValueSta
     getDirectRef :: (Member Runtime r) => DirectRef -> Sem r Val
     getDirectRef = \case
       StackRef -> topValueStack
-      ArgRef off -> readArg off
-      TempRef off -> readTemp off
+      ArgRef OffsetRef {..} -> readArg _offsetRefOffset
+      TempRef OffsetRef {..} -> readTemp _offsetRefOffset
 
     popLastValueStack :: (Member Runtime r) => Sem r Val
     popLastValueStack = do
diff --git a/src/Juvix/Compiler/Asm/Language.hs b/src/Juvix/Compiler/Asm/Language.hs
index 037d59730c..465ec42425 100644
--- a/src/Juvix/Compiler/Asm/Language.hs
+++ b/src/Juvix/Compiler/Asm/Language.hs
@@ -45,14 +45,20 @@ data DirectRef
     StackRef
   | -- | ArgRef references an argument in the argument area (0-based offsets).
     --   JVA code: 'arg[<offset>]'.
-    ArgRef Offset
+    ArgRef OffsetRef
   | -- | TempRef references a value in the temporary area (0-based offsets). JVA
     --   code: 'tmp[<offset>]'.
-    TempRef Offset
+    TempRef OffsetRef
+
+data OffsetRef = OffsetRef
+  { _offsetRefOffset :: Offset,
+    _offsetRefName :: Maybe Text
+  }
 
 -- | Constructor field reference. JVA code: '<dref>.<tag>[<offset>]'
 data Field = Field
-  { -- | tag of the constructor being referenced
+  { _fieldName :: Maybe Text,
+    -- | tag of the constructor being referenced
     _fieldTag :: Tag,
     -- | location where the data is stored
     _fieldRef :: DirectRef,
@@ -60,6 +66,7 @@ data Field = Field
   }
 
 makeLenses ''Field
+makeLenses ''OffsetRef
 
 -- | Function call type
 data CallType = CallFun Symbol | CallClosure
@@ -80,10 +87,6 @@ data Instruction
     Push Value
   | -- | Pop the stack. JVA opcode: 'pop'.
     Pop
-  | -- | Push the top of the value stack onto the temporary stack, pop the value
-    -- stack. Used to implement Core.Let and Core.Case. JVA opcodes: 'pusht', 'popt'.
-    PushTemp
-  | PopTemp
   | -- | Print a debug log of the object on top of the stack. Does not pop the
     -- stack. JVA opcode: 'trace'.
     Trace
@@ -220,6 +223,13 @@ data Command
     -- JVA code: 'case <ind> { <tag>: {<code>} ... <tag>: {<code>} default: {<code>} }'
     -- (any branch may be omitted).
     Case CmdCase
+  | -- | Push the top of the value stack onto the temporary stack, pop the value
+    -- stack, execute the nested code, and if not tail recursive then pop the
+    -- temporary stack afterwards. Used to implement Core.Let and Core.Case. JVA
+    -- codes: 'save {<code>}', 'save <name> {<code>}', 'tsave {<code>}', 'tsave
+    -- <name> {<code>}'. The 'tsave' version does not pop the temporary stack
+    -- after executing '<code>' (which is supposed to return).
+    Save CmdSave
 
 newtype CommandInfo = CommandInfo
   { _commandInfoLocation :: Maybe Location
@@ -251,6 +261,13 @@ data CaseBranch = CaseBranch
     _caseBranchCode :: Code
   }
 
+data CmdSave = CmdSave
+  { _cmdSaveInfo :: CommandInfo,
+    _cmdSaveIsTail :: Bool,
+    _cmdSaveName :: Maybe Text,
+    _cmdSaveCode :: Code
+  }
+
 -- | `Code` corresponds to JuvixAsm code for a single function.
 type Code = [Command]
 
@@ -263,3 +280,4 @@ makeLenses ''CmdInstr
 makeLenses ''CmdBranch
 makeLenses ''CmdCase
 makeLenses ''CaseBranch
+makeLenses ''CmdSave
diff --git a/src/Juvix/Compiler/Asm/Pretty/Base.hs b/src/Juvix/Compiler/Asm/Pretty/Base.hs
index 494dbd9559..1b2a8c5fcf 100644
--- a/src/Juvix/Compiler/Asm/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Asm/Pretty/Base.hs
@@ -211,12 +211,16 @@ instance PrettyCode Type where
     TyFun x ->
       ppCode x
 
+ppOffsetRef :: Text -> OffsetRef -> Sem r (Doc Ann)
+ppOffsetRef str OffsetRef {..} =
+  return $ maybe (variable str <> lbracket <> integer _offsetRefOffset <> rbracket) variable _offsetRefName
+
 instance PrettyCode DirectRef where
   ppCode :: DirectRef -> Sem r (Doc Ann)
   ppCode = \case
     StackRef -> return $ variable Str.dollar
-    ArgRef off -> return $ variable Str.arg <> lbracket <> integer off <> rbracket
-    TempRef off -> return $ variable Str.tmp <> lbracket <> integer off <> rbracket
+    ArgRef roff -> ppOffsetRef Str.arg roff
+    TempRef roff -> ppOffsetRef Str.tmp roff
 
 instance PrettyCode Field where
   ppCode :: (Member (Reader Options) r) => Field -> Sem r (Doc Ann)
@@ -273,8 +277,6 @@ instance PrettyCode Instruction where
     StrToInt -> return $ primitive Str.instrStrToInt
     Push val -> (primitive Str.instrPush <+>) <$> ppCode val
     Pop -> return $ primitive Str.instrPop
-    PushTemp -> return $ primitive Str.instrPusht
-    PopTemp -> return $ primitive Str.instrPopt
     Trace -> return $ primitive Str.instrTrace
     Dump -> return $ primitive Str.instrDump
     Failure -> return $ primitive Str.instrFailure
@@ -336,6 +338,10 @@ instance PrettyCode Command where
           return $ brs ++ [d]
         Nothing -> return brs
       return $ primitive Str.case_ <+> name <+> braces' (vsep brs')
+    Save CmdSave {..} -> do
+      c <- ppCodeCode _cmdSaveCode
+      let s = if _cmdSaveIsTail then Str.tsave else Str.save
+      return $ primitive s <+> (maybe mempty ((<> space) . variable) _cmdSaveName) <> braces' c
 
 instance (PrettyCode a) => PrettyCode [a] where
   ppCode x = do
@@ -345,12 +351,14 @@ instance (PrettyCode a) => PrettyCode [a] where
 instance PrettyCode FunctionInfo where
   ppCode FunctionInfo {..} = do
     argtys <- mapM ppCode (typeArgs _functionType)
+    let argnames = map (fmap variable) _functionArgNames
+        args = zipWithExact (\mn ty -> maybe mempty (\n -> n <+> colon <> space) mn <> ty) argnames argtys
     targetty <- ppCode (typeTarget _functionType)
     c <- ppCodeCode _functionCode
     return $
       keyword Str.function
         <+> annotate (AnnKind KNameFunction) (pretty (quoteAsmFunName $ quoteAsmName _functionName))
-          <> encloseSep lparen rparen ", " argtys
+          <> encloseSep lparen rparen ", " args
         <+> colon
         <+> targetty
         <+> braces' c
diff --git a/src/Juvix/Compiler/Asm/Transformation/Prealloc.hs b/src/Juvix/Compiler/Asm/Transformation/Prealloc.hs
index cd5136ca01..20ff3fd0f0 100644
--- a/src/Juvix/Compiler/Asm/Transformation/Prealloc.hs
+++ b/src/Juvix/Compiler/Asm/Transformation/Prealloc.hs
@@ -19,7 +19,8 @@ computeCodePrealloc maxArgsNum tab code = prealloc <$> foldS sig code (0, [])
           _foldAdjust = second (const []),
           _foldInstr = const goInstr,
           _foldBranch = const goBranch,
-          _foldCase = const goCase
+          _foldCase = const goCase,
+          _foldSave = const goSave
         }
 
     goInstr :: CmdInstr -> (Int, Code) -> Sem r (Int, Code)
@@ -77,6 +78,15 @@ computeCodePrealloc maxArgsNum tab code = prealloc <$> foldS sig code (0, [])
                 _cmdCaseDefault = fmap prealloc md
               }
 
+    goSave :: CmdSave -> (Int, Code) -> (Int, Code) -> Sem r (Int, Code)
+    goSave cmd (k, br) (_, c) = return (k, cmd' : c)
+      where
+        cmd' =
+          Save
+            cmd
+              { _cmdSaveCode = br
+              }
+
     prealloc :: (Int, Code) -> Code
     prealloc (0, c) = c
     prealloc (n, c) = mkInstr (Prealloc (InstrPrealloc n)) : c
@@ -100,7 +110,8 @@ checkCodePrealloc maxArgsNum tab code = do
           _foldAdjust = id,
           _foldInstr = const goInstr,
           _foldBranch = const goBranch,
-          _foldCase = const goCase
+          _foldCase = const goCase,
+          _foldSave = const goSave
         }
 
     goInstr :: CmdInstr -> (Int -> Int) -> Sem r (Int -> Int)
@@ -145,6 +156,10 @@ checkCodePrealloc maxArgsNum tab code = do
             k' = min (minimum ks) (fromMaybe k kd)
          in cont k'
 
+    goSave :: CmdSave -> (Int -> Int) -> (Int -> Int) -> Sem r (Int -> Int)
+    goSave _ br cont =
+      return $ cont . br
+
 checkPrealloc :: Options -> InfoTable -> Bool
 checkPrealloc opts tab =
   case run $ runError $ runReader opts sb of
diff --git a/src/Juvix/Compiler/Asm/Transformation/StackUsage.hs b/src/Juvix/Compiler/Asm/Transformation/StackUsage.hs
index 87d4ca34fe..4fec6802f1 100644
--- a/src/Juvix/Compiler/Asm/Transformation/StackUsage.hs
+++ b/src/Juvix/Compiler/Asm/Transformation/StackUsage.hs
@@ -27,6 +27,11 @@ computeFunctionStackUsage tab fi = do
             return
               ( max (si ^. stackInfoValueStackHeight) (max (maximum (map (maximum . map fst) cs)) (maybe 0 (maximum . map fst) md)),
                 max (si ^. stackInfoTempStackHeight) (max (maximum (map (maximum . map snd) cs)) (maybe 0 (maximum . map snd) md))
+              ),
+          _recurseSave = \si _ b ->
+            return
+              ( max (si ^. stackInfoValueStackHeight) (maximum (map fst b)),
+                max (si ^. stackInfoTempStackHeight) (maximum (map snd b))
               )
         }
 
diff --git a/src/Juvix/Compiler/Asm/Transformation/Validate.hs b/src/Juvix/Compiler/Asm/Transformation/Validate.hs
index 215f9c47db..c59596ed14 100644
--- a/src/Juvix/Compiler/Asm/Transformation/Validate.hs
+++ b/src/Juvix/Compiler/Asm/Transformation/Validate.hs
@@ -13,7 +13,8 @@ validateCode tab fi code = do
         { _recursorInfoTable = tab,
           _recurseInstr = \_ _ -> return (),
           _recurseBranch = \_ _ _ _ -> return (),
-          _recurseCase = \_ _ _ _ -> return ()
+          _recurseCase = \_ _ _ _ -> return (),
+          _recurseSave = \_ _ _ -> return ()
         }
 
 validateFunction :: (Member (Error AsmError) r) => InfoTable -> FunctionInfo -> Sem r FunctionInfo
diff --git a/src/Juvix/Compiler/Asm/Translation/FromCore.hs b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
index cb4cd979e8..bc9587f497 100644
--- a/src/Juvix/Compiler/Asm/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
@@ -27,13 +27,22 @@ fromCore tab =
 -- Generate code for a single function.
 genCode :: Core.InfoTable -> Core.FunctionInfo -> FunctionInfo
 genCode infoTable fi =
-  let code =
+  let argnames = map (Just . (^. Core.argumentName)) (fi ^. Core.functionArgsInfo)
+      code =
         DL.toList $
           go
             True
             0
             ( BL.fromList $
-                reverse (map (Ref . DRef . ArgRef) [0 .. fi ^. Core.functionArgsNum - 1])
+                reverse
+                  ( map
+                      (Ref . DRef . ArgRef)
+                      ( zipWithExact
+                          OffsetRef
+                          [0 .. fi ^. Core.functionArgsNum - 1]
+                          argnames
+                      )
+                  )
             )
             (fi ^. Core.functionBody)
    in FunctionInfo
@@ -41,6 +50,7 @@ genCode infoTable fi =
           _functionLocation = fi ^. Core.functionLocation,
           _functionSymbol = fi ^. Core.functionSymbol,
           _functionArgsNum = fi ^. Core.functionArgsNum,
+          _functionArgNames = argnames,
           _functionType = convertType (fi ^. Core.functionArgsNum) (fi ^. Core.functionType),
           _functionCode = code,
           _functionMaxTempStackHeight = -1, -- computed later
@@ -175,9 +185,19 @@ genCode infoTable fi =
 
     goLet :: Bool -> Int -> BinderList Value -> Core.Let -> Code'
     goLet isTail tempSize refs (Core.Let {..}) =
-      DL.append
-        (DL.snoc (go False tempSize refs (_letItem ^. Core.letItemValue)) (mkInstr PushTemp))
-        (snocPopTemp isTail $ go isTail (tempSize + 1) (BL.cons (Ref (DRef (TempRef tempSize))) refs) _letBody)
+      DL.snoc
+        (go False tempSize refs (_letItem ^. Core.letItemValue))
+        ( Save $
+            CmdSave
+              { _cmdSaveInfo = emptyInfo,
+                _cmdSaveIsTail = isTail,
+                _cmdSaveCode = DL.toList $ go isTail (tempSize + 1) (BL.cons (Ref (DRef (TempRef nameRef))) refs) _letBody,
+                _cmdSaveName = Just name
+              }
+        )
+      where
+        name = _letItem ^. Core.letItemBinder . Core.binderName
+        nameRef = OffsetRef tempSize (Just name)
 
     goCase :: Bool -> Int -> BinderList Value -> Core.Case -> Code'
     goCase isTail tempSize refs (Core.Case {..}) =
@@ -217,21 +237,26 @@ genCode infoTable fi =
         compileCaseBranch bindersNum tag body =
           CaseBranch
             tag
-            ( DL.toList $
-                DL.cons (mkInstr PushTemp) $
-                  snocPopTemp isTail $
-                    go
-                      isTail
-                      (tempSize + 1)
-                      ( BL.prepend
-                          ( map
-                              (Ref . ConstrRef . Field tag (TempRef tempSize))
-                              (reverse [0 .. bindersNum - 1])
+            [ Save $
+                CmdSave
+                  { _cmdSaveInfo = emptyInfo,
+                    _cmdSaveIsTail = isTail,
+                    _cmdSaveName = Nothing,
+                    _cmdSaveCode =
+                      DL.toList $
+                        go
+                          isTail
+                          (tempSize + 1)
+                          ( BL.prepend
+                              ( map
+                                  (Ref . ConstrRef . Field Nothing tag (TempRef (OffsetRef tempSize Nothing)))
+                                  (reverse [0 .. bindersNum - 1])
+                              )
+                              refs
                           )
-                          refs
-                      )
-                      body
-            )
+                          body
+                  }
+            ]
 
         compileCaseDefault :: Core.Node -> Code
         compileCaseDefault =
@@ -279,10 +304,6 @@ genCode infoTable fi =
     snocReturn True code = DL.snoc code (mkInstr Return)
     snocReturn False code = code
 
-    snocPopTemp :: Bool -> Code' -> Code'
-    snocPopTemp False code = DL.snoc code (mkInstr PopTemp)
-    snocPopTemp True code = code
-
 -- | Be mindful that JuvixAsm types are explicitly uncurried, while
 -- Core.Stripped types are always curried. If a function takes `n` arguments,
 -- then the first `n` arguments should be uncurried in its JuvixAsm type.
@@ -343,6 +364,7 @@ translateConstructorInfo ci =
       _constructorLocation = ci ^. Core.constructorLocation,
       _constructorTag = ci ^. Core.constructorTag,
       _constructorArgsNum = length (typeArgs ty),
+      _constructorArgNames = ci ^. Core.constructorArgNames,
       _constructorType = ty,
       _constructorInductive = ci ^. Core.constructorInductive,
       _constructorRepresentation = MemRepConstr,
diff --git a/src/Juvix/Compiler/Asm/Translation/FromSource.hs b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
index 90843e96e1..3acf324e40 100644
--- a/src/Juvix/Compiler/Asm/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromSource.hs
@@ -5,6 +5,7 @@ module Juvix.Compiler.Asm.Translation.FromSource
 where
 
 import Control.Monad.Trans.Class (lift)
+import Data.HashMap.Strict qualified as HashMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Asm.Data.InfoTable
 import Juvix.Compiler.Asm.Data.InfoTableBuilder
@@ -15,15 +16,27 @@ import Juvix.Compiler.Asm.Translation.FromSource.Lexer
 import Juvix.Parser.Error
 import Text.Megaparsec qualified as P
 
+type LocalNameMap = HashMap Text DirectRef
+
+localS :: (Member (State s) r) => (s -> s) -> ParsecS r a -> ParsecS r a
+localS update a = do
+  s <- lift get
+  lift $ put (update s)
+  a' <- a
+  lift $ put s
+  return a'
+
 parseText :: Text -> Either MegaparsecError InfoTable
 parseText = runParser ""
 
 runParser :: FilePath -> Text -> Either MegaparsecError InfoTable
 runParser fileName input =
   case run $
-    runInfoTableBuilder $
-      evalTopNameIdGen $
-        P.runParserT parseToplevel fileName input of
+    evalState @Index 0 $
+      evalState @LocalNameMap mempty $
+        runInfoTableBuilder $
+          evalTopNameIdGen $
+            P.runParserT parseToplevel fileName input of
     (_, Left err) -> Left (MegaparsecError err)
     (tbl, Right ()) -> Right tbl
 
@@ -42,12 +55,13 @@ createBuiltinConstr sym btag name ty i =
           _constructorTag = BuiltinTag btag,
           _constructorType = ty,
           _constructorArgsNum = n,
+          _constructorArgNames = replicate n Nothing,
           _constructorInductive = sym,
           _constructorRepresentation = MemRepConstr,
           _constructorFixity = Nothing
         }
 
-declareBuiltins :: (Member InfoTableBuilder r) => ParsecS r ()
+declareBuiltins :: (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) => ParsecS r ()
 declareBuiltins = do
   loc <- curLoc
   let i = mkInterval loc loc
@@ -73,7 +87,7 @@ declareBuiltins = do
   lift $ mapM_ registerConstr constrs
 
 parseToplevel ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r ()
 parseToplevel = do
   declareBuiltins
@@ -82,12 +96,12 @@ parseToplevel = do
   P.eof
 
 statement ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r ()
 statement = statementFunction <|> statementInductive
 
 statementFunction ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r ()
 statementFunction = do
   kw kwFun
@@ -100,7 +114,9 @@ statementFunction = do
     _ -> parseFailure off ("duplicate identifier: " ++ fromText txt)
   when (txt == "main") $
     lift (registerMain sym)
-  argtys <- functionArguments
+  args <- functionArguments
+  let argtys = map snd args
+      argnames = map fst args
   when (txt == "main" && not (null argtys)) $
     parseFailure off "the 'main' function must take zero arguments"
   mrty <- optional typeAnnotation
@@ -111,12 +127,21 @@ statementFunction = do
             _functionLocation = Just i,
             _functionCode = [],
             _functionArgsNum = length argtys,
+            _functionArgNames = argnames,
             _functionType = mkTypeFun argtys (fromMaybe TyDynamic mrty),
             _functionMaxValueStackHeight = -1, -- computed later
             _functionMaxTempStackHeight = -1
           }
   lift $ registerFunction fi0
-  mcode <- (kw delimSemicolon $> Nothing) <|> optional (braces parseCode)
+  let updateNames :: LocalNameMap -> LocalNameMap
+      updateNames names =
+        foldr
+          (\(mn, idx) h -> maybe h (\n -> HashMap.insert n (ArgRef (OffsetRef idx (Just n))) h) mn)
+          names
+          (zip argnames [0 ..])
+  mcode <-
+    (kw delimSemicolon $> Nothing)
+      <|> optional (braces (localS updateNames parseCode))
   let fi = fi0 {_functionCode = fromMaybe [] mcode}
   case idt of
     Just (IdentFwd _) -> do
@@ -135,7 +160,7 @@ statementFunction = do
         lift (registerForward txt sym)
 
 statementInductive ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r ()
 statementInductive = do
   kw kwInductive
@@ -159,16 +184,16 @@ statementInductive = do
   lift $ registerInductive ii {_inductiveConstructors = map (^. constructorTag) ctrs}
 
 functionArguments ::
-  (Member InfoTableBuilder r) =>
-  ParsecS r [Type]
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
+  ParsecS r [(Maybe Text, Type)]
 functionArguments = do
   lparen
-  args <- P.sepBy parseType comma
+  args <- P.sepBy parseArgument comma
   rparen
   return args
 
 constrDecl ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   Symbol ->
   ParsecS r ConstructorInfo
 constrDecl symInd = do
@@ -180,12 +205,14 @@ constrDecl symInd = do
   tag <- lift freshTag
   ty <- typeAnnotation
   let ty' = uncurryType ty
-  let ci =
+      argsNum = length (typeArgs ty')
+      ci =
         ConstructorInfo
           { _constructorName = txt,
             _constructorLocation = Just i,
             _constructorTag = tag,
-            _constructorArgsNum = length (typeArgs ty'),
+            _constructorArgsNum = argsNum,
+            _constructorArgNames = replicate argsNum Nothing,
             _constructorType = ty',
             _constructorInductive = symInd,
             _constructorRepresentation = MemRepConstr,
@@ -195,14 +222,23 @@ constrDecl symInd = do
   return ci
 
 typeAnnotation ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Type
 typeAnnotation = do
   kw kwColon
   parseType
 
+parseArgument :: (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) => ParsecS r (Maybe Text, Type)
+parseArgument = do
+  n <- optional $ P.try $ do
+    txt <- identifier
+    kw kwColon
+    return txt
+  ty <- parseType
+  return (n, ty)
+
 parseType ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Type
 parseType = do
   tys <- typeArguments
@@ -214,7 +250,7 @@ parseType = do
       return (head tys)
 
 typeFun' ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   NonEmpty Type ->
   ParsecS r Type
 typeFun' tyargs = do
@@ -222,7 +258,7 @@ typeFun' tyargs = do
   TyFun . TypeFun tyargs <$> parseType
 
 typeArguments ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r (NonEmpty Type)
 typeArguments = do
   parens (P.sepBy1 parseType comma <&> NonEmpty.fromList)
@@ -233,7 +269,7 @@ typeDynamic :: ParsecS r Type
 typeDynamic = kw kwStar $> TyDynamic
 
 typeNamed ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Type
 typeNamed = do
   off <- P.getOffset
@@ -250,12 +286,12 @@ typeNamed = do
         _ -> parseFailure off ("not a type: " ++ fromText txt)
 
 parseCode ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Code
 parseCode = P.sepEndBy command (kw delimSemicolon)
 
 command ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Command
 command = do
   off <- P.getOffset
@@ -288,10 +324,6 @@ command = do
       mkInstr' loc . Push <$> value
     "pop" ->
       return $ mkInstr' loc Pop
-    "pusht" ->
-      return $ mkInstr' loc PushTemp
-    "popt" ->
-      return $ mkInstr' loc PopTemp
     "trace" ->
       return $ mkInstr' loc Trace
     "dump" ->
@@ -327,11 +359,36 @@ command = do
       def <- optional defaultBranch
       rbrace
       return $ Case (CmdCase (CommandInfo loc) sym brs def)
+    "save" ->
+      parseSave loc False
+    "tsave" ->
+      parseSave loc True
     _ ->
       parseFailure off ("unknown instruction: " ++ fromText txt)
 
+parseSave ::
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
+  Maybe Interval ->
+  Bool ->
+  ParsecS r Command
+parseSave loc isTail = do
+  mn <- optional identifier
+  tmpNum <- lift get
+  let updateNames :: LocalNameMap -> LocalNameMap
+      updateNames mp = maybe mp (\n -> HashMap.insert n (TempRef (OffsetRef tmpNum (Just n))) mp) mn
+  c <- braces (localS @Index (+ 1) $ localS updateNames parseCode)
+  return $
+    Save
+      ( CmdSave
+          { _cmdSaveInfo = CommandInfo loc,
+            _cmdSaveIsTail = isTail,
+            _cmdSaveCode = c,
+            _cmdSaveName = mn
+          }
+      )
+
 value ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Value
 value = integerValue <|> boolValue <|> stringValue <|> unitValue <|> voidValue <|> memValue
 
@@ -357,14 +414,14 @@ voidValue :: ParsecS r Value
 voidValue = kw kwVoid $> ConstVoid
 
 memValue ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Value
 memValue = do
   r <- directRef
   parseField r <|> return (Ref (DRef r))
 
-directRef :: ParsecS r DirectRef
-directRef = stackRef <|> argRef <|> tempRef
+directRef :: (Member (State LocalNameMap) r) => ParsecS r DirectRef
+directRef = stackRef <|> argRef <|> tempRef <|> namedRef
 
 stackRef :: ParsecS r DirectRef
 stackRef = kw kwDollar $> StackRef
@@ -373,26 +430,35 @@ argRef :: ParsecS r DirectRef
 argRef = do
   kw kwArg
   (off, _) <- brackets integer
-  return $ ArgRef (fromInteger off)
+  return $ ArgRef (OffsetRef (fromInteger off) Nothing)
 
 tempRef :: ParsecS r DirectRef
 tempRef = do
   kw kwTmp
   (off, _) <- brackets integer
-  return $ TempRef (fromInteger off)
+  return $ TempRef (OffsetRef (fromInteger off) Nothing)
+
+namedRef :: (Member (State LocalNameMap) r) => ParsecS r DirectRef
+namedRef = do
+  off <- P.getOffset
+  txt <- identifier
+  mr <- lift $ gets (HashMap.lookup txt)
+  case mr of
+    Just r -> return r
+    Nothing -> parseFailure off "undeclared identifier"
 
 parseField ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   DirectRef ->
   ParsecS r Value
 parseField dref = do
   dot
   tag <- constrTag
   (off, _) <- brackets integer
-  return $ Ref (ConstrRef (Field tag dref (fromInteger off)))
+  return $ Ref (ConstrRef (Field Nothing tag dref (fromInteger off)))
 
 constrTag ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Tag
 constrTag = do
   off <- P.getOffset
@@ -403,7 +469,7 @@ constrTag = do
     _ -> parseFailure off "expected a constructor"
 
 indSymbol ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Symbol
 indSymbol = do
   off <- P.getOffset
@@ -414,7 +480,7 @@ indSymbol = do
     _ -> parseFailure off "expected an inductive type"
 
 funSymbol ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Symbol
 funSymbol = do
   off <- P.getOffset
@@ -426,7 +492,7 @@ funSymbol = do
     _ -> parseFailure off "expected a function"
 
 instrAllocClosure ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r InstrAllocClosure
 instrAllocClosure = do
   sym <- funSymbol
@@ -439,7 +505,7 @@ instrExtendClosure = do
   return $ InstrExtendClosure (fromInteger argsNum)
 
 instrCall ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r InstrCall
 instrCall = do
   ct <- parseCallType
@@ -453,7 +519,7 @@ instrCall = do
   return (InstrCall ct argsNum)
 
 parseCallType ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r CallType
 parseCallType = (kw kwDollar $> CallClosure) <|> (CallFun <$> funSymbol)
 
@@ -463,26 +529,26 @@ instrCallClosures = do
   return (InstrCallClosures (fromInteger argsNum))
 
 branchCode ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Code
 branchCode = braces parseCode <|> (command >>= \x -> return [x])
 
 trueBranch ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Code
 trueBranch = do
   symbol "true:"
   branchCode
 
 falseBranch ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Code
 falseBranch = do
   symbol "false:"
   branchCode
 
 caseBranch ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r CaseBranch
 caseBranch = do
   tag <- P.try constrTag
@@ -490,6 +556,6 @@ caseBranch = do
   CaseBranch tag <$> branchCode
 
 defaultBranch ::
-  (Member InfoTableBuilder r) =>
+  (Members '[InfoTableBuilder, State LocalNameMap, State Index] r) =>
   ParsecS r Code
 defaultBranch = symbol "default:" >> branchCode
diff --git a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
index 337a11357a..891e06f6cf 100644
--- a/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
+++ b/src/Juvix/Compiler/Backend/C/Translation/FromReg.hs
@@ -256,6 +256,8 @@ fromRegInstr bNoStack info = \case
     fromBranch x
   Reg.Case x ->
     fromCase x
+  Reg.Block Reg.InstrBlock {..} ->
+    fromRegCode bNoStack info _instrBlockCode
   where
     fromBinaryOp :: Reg.BinaryOp -> Statement
     fromBinaryOp Reg.BinaryOp {..} =
diff --git a/src/Juvix/Compiler/Core/Data/InfoTable.hs b/src/Juvix/Compiler/Core/Data/InfoTable.hs
index b1a6d16677..1ce16579da 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTable.hs
@@ -88,6 +88,7 @@ data ConstructorInfo = ConstructorInfo
     _constructorTag :: Tag,
     _constructorType :: Type,
     _constructorArgsNum :: Int,
+    _constructorArgNames :: [Maybe Text],
     _constructorInductive :: Symbol,
     _constructorFixity :: Maybe Fixity,
     _constructorBuiltin :: Maybe BuiltinConstructor,
diff --git a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
index f04ef8a261..fb8bee0361 100644
--- a/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
+++ b/src/Juvix/Compiler/Core/Data/InfoTableBuilder.hs
@@ -159,12 +159,15 @@ createBuiltinConstr sym tag nameTxt ty cblt =
       _constructorLocation = Nothing,
       _constructorTag = tag,
       _constructorType = ty,
-      _constructorArgsNum = length (typeArgs ty),
+      _constructorArgsNum = argsNum,
+      _constructorArgNames = replicate argsNum Nothing,
       _constructorInductive = sym,
       _constructorFixity = Nothing,
       _constructorBuiltin = cblt,
       _constructorPragmas = mempty
     }
+  where
+    argsNum = length (typeArgs ty)
 
 builtinConstrs ::
   Symbol ->
diff --git a/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs b/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs
index c1dbf24182..14022a8ec9 100644
--- a/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs
+++ b/src/Juvix/Compiler/Core/Data/Stripped/InfoTable.hs
@@ -45,6 +45,7 @@ data ConstructorInfo = ConstructorInfo
     _constructorInductive :: Symbol,
     _constructorTag :: Tag,
     _constructorType :: Type,
+    _constructorArgNames :: [Maybe Text],
     _constructorFixity :: Maybe Fixity
   }
 
diff --git a/src/Juvix/Compiler/Core/Transformation/LetHoisting.hs b/src/Juvix/Compiler/Core/Transformation/LetHoisting.hs
index 59d5188461..711384e63f 100644
--- a/src/Juvix/Compiler/Core/Transformation/LetHoisting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LetHoisting.hs
@@ -2,7 +2,7 @@
 -- transformation assumes:
 -- - There are no LetRecs, Lambdas (other than the ones at the top), nor Match.
 -- - Case nodes do not have binders.
--- - All variables reference either a lambda or a let.
+-- - All variables are bound either by a lambda or a let.
 -- - All let and lambda binders have type Int.
 -- - Let nodes do not appear under Pi binders.
 module Juvix.Compiler.Core.Transformation.LetHoisting
diff --git a/src/Juvix/Compiler/Core/Translation/FromInternal.hs b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
index 2569f98ae0..4afb79f3b8 100644
--- a/src/Juvix/Compiler/Core/Translation/FromInternal.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromInternal.hs
@@ -179,6 +179,7 @@ goConstructor sym ctor = do
             _constructorTag = tag,
             _constructorType = ty,
             _constructorArgsNum = argsNum',
+            _constructorArgNames = replicate argsNum' Nothing,
             _constructorInductive = sym,
             _constructorBuiltin = mblt,
             _constructorFixity = ctorName ^. nameFixity,
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index 7974ddd919..3a3ed40fab 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -221,12 +221,14 @@ constrDecl symInd = do
     parseFailure off ("duplicate identifier: " ++ fromText txt)
   tag <- lift freshTag
   ty <- typeAnnotation
-  let ci =
+  let argsNum = length (typeArgs ty)
+      ci =
         ConstructorInfo
           { _constructorName = txt,
             _constructorLocation = Just i,
             _constructorTag = tag,
-            _constructorArgsNum = length (typeArgs ty),
+            _constructorArgsNum = argsNum,
+            _constructorArgNames = replicate argsNum Nothing,
             _constructorType = ty,
             _constructorInductive = symInd,
             _constructorFixity = Nothing,
diff --git a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
index 00d8d6ca93..c971fb56c1 100644
--- a/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
+++ b/src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs
@@ -143,6 +143,7 @@ translateConstructorInfo ConstructorInfo {..} =
       _constructorInductive = _constructorInductive,
       _constructorTag = _constructorTag,
       _constructorType = translateType _constructorType,
+      _constructorArgNames,
       _constructorFixity
     }
 
diff --git a/src/Juvix/Compiler/Reg/Extra.hs b/src/Juvix/Compiler/Reg/Extra.hs
index 6154630d8b..850db72900 100644
--- a/src/Juvix/Compiler/Reg/Extra.hs
+++ b/src/Juvix/Compiler/Reg/Extra.hs
@@ -58,6 +58,8 @@ computeMaxStackHeight lims = maximum . map go
               )
           )
           (maybe 0 (computeMaxStackHeight lims) _instrCaseDefault)
+      Block InstrBlock {..} ->
+        computeMaxStackHeight lims _instrBlockCode
 
 computeMaxCallClosuresArgsNum :: Code -> Int
 computeMaxCallClosuresArgsNum = maximum . map go
@@ -93,6 +95,8 @@ computeMaxCallClosuresArgsNum = maximum . map go
               )
           )
           (maybe 0 computeMaxCallClosuresArgsNum _instrCaseDefault)
+      Block InstrBlock {..} ->
+        computeMaxCallClosuresArgsNum _instrBlockCode
 
 computeStringMap :: HashMap Text Int -> Code -> HashMap Text Int
 computeStringMap strs = snd . run . execState (HashMap.size strs, strs) . mapM go
@@ -135,6 +139,8 @@ computeStringMap strs = snd . run . execState (HashMap.size strs, strs) . mapM g
         goVal _instrCaseValue
         mapM_ (mapM_ go . (^. caseBranchCode)) _instrCaseBranches
         maybe (return ()) (mapM_ go) _instrCaseDefault
+      Block InstrBlock {..} ->
+        mapM_ go _instrBlockCode
 
     goVal :: (Member (State (Int, HashMap Text Int)) r) => Value -> Sem r ()
     goVal = \case
diff --git a/src/Juvix/Compiler/Reg/Language.hs b/src/Juvix/Compiler/Reg/Language.hs
index 34df7e3443..88e0643cdd 100644
--- a/src/Juvix/Compiler/Reg/Language.hs
+++ b/src/Juvix/Compiler/Reg/Language.hs
@@ -53,6 +53,7 @@ data Instruction
   | Return InstrReturn
   | Branch InstrBranch
   | Case InstrCase
+  | Block InstrBlock
 
 type Code = [Instruction]
 
@@ -169,6 +170,10 @@ data CaseBranch = CaseBranch
     _caseBranchCode :: Code
   }
 
+newtype InstrBlock = InstrBlock
+  { _instrBlockCode :: Code
+  }
+
 makeLenses ''ConstrField
 makeLenses ''BinaryOp
 makeLenses ''InstrAssign
diff --git a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
index 2b3395eb0b..6b293b439e 100644
--- a/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
+++ b/src/Juvix/Compiler/Reg/Translation/FromAsm.hs
@@ -66,7 +66,8 @@ fromAsmFun tab fi =
         { _recursorInfoTable = tab,
           _recurseInstr = fromAsmInstr fi tab,
           _recurseBranch = fromAsmBranch,
-          _recurseCase = fromAsmCase tab
+          _recurseCase = fromAsmCase tab,
+          _recurseSave = fromAsmSave
         }
 
 fromAsmInstr ::
@@ -82,12 +83,6 @@ fromAsmInstr funInfo tab si Asm.CmdInstr {..} =
     Asm.StrToInt -> return $ mkStrToInt (VarRef VarGroupStack n) (VRef $ VarRef VarGroupStack n)
     Asm.Push val -> return $ mkAssign (VarRef VarGroupStack (n + 1)) (mkValue val)
     Asm.Pop -> return Nop
-    Asm.PushTemp ->
-      return $
-        mkAssign
-          (VarRef VarGroupTemp (si ^. Asm.stackInfoTempStackHeight))
-          (VRef $ VarRef VarGroupStack n)
-    Asm.PopTemp -> return Nop
     Asm.Trace -> return $ Trace $ InstrTrace (VRef $ VarRef VarGroupStack n)
     Asm.Dump -> return Dump
     Asm.Failure -> return $ Failure $ InstrFailure (VRef $ VarRef VarGroupStack n)
@@ -174,8 +169,8 @@ fromAsmInstr funInfo tab si Asm.CmdInstr {..} =
     mkVar :: Asm.DirectRef -> VarRef
     mkVar = \case
       Asm.StackRef -> VarRef VarGroupStack n
-      Asm.ArgRef idx -> VarRef VarGroupArgs idx
-      Asm.TempRef idx -> VarRef VarGroupTemp idx
+      Asm.ArgRef Asm.OffsetRef {..} -> VarRef VarGroupArgs _offsetRefOffset
+      Asm.TempRef Asm.OffsetRef {..} -> VarRef VarGroupTemp _offsetRefOffset
 
     mkPrealloc :: Asm.InstrPrealloc -> Instruction
     mkPrealloc Asm.InstrPrealloc {..} =
@@ -306,3 +301,21 @@ fromAsmCase tab si Asm.CmdCase {..} brs def =
     ii =
       fromMaybe impossible $
         HashMap.lookup _cmdCaseInductive (tab ^. Asm.infoInductives)
+
+fromAsmSave ::
+  Asm.StackInfo ->
+  Asm.CmdSave ->
+  Code ->
+  Sem r Instruction
+fromAsmSave si Asm.CmdSave {} block =
+  return $
+    Block $
+      InstrBlock
+        { _instrBlockCode =
+            Assign
+              ( InstrAssign
+                  (VarRef VarGroupTemp (si ^. Asm.stackInfoTempStackHeight))
+                  (VRef $ VarRef VarGroupStack (si ^. Asm.stackInfoValueStackHeight - 1))
+              )
+              : block
+        }
diff --git a/src/Juvix/Extra/Strings.hs b/src/Juvix/Extra/Strings.hs
index f95732bdb7..1abf363cab 100644
--- a/src/Juvix/Extra/Strings.hs
+++ b/src/Juvix/Extra/Strings.hs
@@ -491,6 +491,12 @@ void = "void"
 case_ :: (IsString s) => s
 case_ = "case"
 
+save :: (IsString s) => s
+save = "save"
+
+tsave :: (IsString s) => s
+tsave = "tsave"
+
 caseOn :: (IsString s) => s
 caseOn = "case-on"
 
diff --git a/tests/Asm/positive/test009.jva b/tests/Asm/positive/test009.jva
index b0d2311477..4987828f19 100644
--- a/tests/Asm/positive/test009.jva
+++ b/tests/Asm/positive/test009.jva
@@ -28,16 +28,16 @@ function map(* -> *, list) : list {
   case list {
     nil: ret
     cons: {
-      pusht;
-      push tmp[0].cons[1];
-      push arg[0];
-      call map;
-      push tmp[0].cons[0];
-      push arg[0];
-      call $ 1;
-      alloc cons;
-      popt;
-      ret;
+      tsave {
+        push tmp[0].cons[1];
+        push arg[0];
+        call map;
+        push tmp[0].cons[0];
+        push arg[0];
+        call $ 1;
+        alloc cons;
+        ret;
+      };
     }
   };
 }
@@ -78,36 +78,36 @@ function main() {
   alloc cons;
   push 0;
   alloc cons;
-  pusht;
-  push tmp[0];
-  call null;
-  trace;
-  pop;
-  alloc nil;
-  call null;
-  trace;
-  pop;
-  push tmp[0];
-  call hd;
-  trace;
-  pop;
-  push tmp[0];
-  call tl;
-  trace;
-  pop;
-  push tmp[0];
-  call tl;
-  call hd;
-  trace;
-  pop;
-  push tmp[0];
-  calloc add_one 0;
-  call map;
-  trace;
-  pop;
-  push tmp[0];
-  calloc add_one 0;
-  call map';
-  popt;
+  save {
+    push tmp[0];
+    call null;
+    trace;
+    pop;
+    alloc nil;
+    call null;
+    trace;
+    pop;
+    push tmp[0];
+    call hd;
+    trace;
+    pop;
+    push tmp[0];
+    call tl;
+    trace;
+    pop;
+    push tmp[0];
+    call tl;
+    call hd;
+    trace;
+    pop;
+    push tmp[0];
+    calloc add_one 0;
+    call map;
+    trace;
+    pop;
+    push tmp[0];
+    calloc add_one 0;
+    call map';
+  };
   ret;
 }
diff --git a/tests/Asm/positive/test012.jva b/tests/Asm/positive/test012.jva
index f0a797ac41..191b8dd3fb 100644
--- a/tests/Asm/positive/test012.jva
+++ b/tests/Asm/positive/test012.jva
@@ -2,30 +2,35 @@
 
 function main() {
   push 1;
-  pusht;
-  push 2;
-  pusht;
-  push tmp[1];
-  popt;
-  push tmp[0];
-  add;
-  pusht;
-  push tmp[1];
-  push tmp[1];
-  mul;
-  pusht;
-  push tmp[2];
-  push 2;
-  add;
-  pusht;
-  push tmp[2];
-  push tmp[3];
-  add;
-  pusht;
-  push tmp[2];
-  push tmp[3];
-  push tmp[4];
-  add;
-  add;
-  ret;
+  tsave {
+    push 2;
+    save {
+      push tmp[1];
+    };
+    push tmp[0];
+    add;
+    tsave {
+      push tmp[1];
+      push tmp[1];
+      mul;
+      tsave {
+        push tmp[2];
+        push 2;
+        add;
+        tsave {
+          push tmp[2];
+          push tmp[3];
+          add;
+          tsave {
+            push tmp[2];
+            push tmp[3];
+            push tmp[4];
+            add;
+            add;
+            ret;
+          };
+        };
+      };
+    };
+  };
 }
diff --git a/tests/Asm/positive/test014.jva b/tests/Asm/positive/test014.jva
index b53cc516d2..f744af5ae7 100644
--- a/tests/Asm/positive/test014.jva
+++ b/tests/Asm/positive/test014.jva
@@ -17,52 +17,55 @@ function gen(integer) : tree {
       push 3;
       push arg[0];
       mod;
-      pusht;
-      push tmp[0];
-      push 0;
-      eq;
-      br {
-        true: {
-          push 1;
-          push arg[0];
-          sub;
-          call gen;
-          alloc node1;
-          ret;
-        }
-        false: {
-          push tmp[0];
-          push 1;
-          eq;
-          br {
-            true: {
-              push 1;
-              push arg[0];
-              sub;
-              pusht;
-              push tmp[1];
-              call gen;
-              push tmp[1];
-              call gen;
-              alloc node2;
-              ret;
-            }
-            false: {
-              push 1;
-              push arg[0];
-              sub;
-              pusht;
-              push tmp[1];
-              call gen;
-              push tmp[1];
-              call gen;
-              push tmp[1];
-              call gen;
-              alloc node3;
-              ret;
-            }
-          };
-        }
+      tsave {
+        push tmp[0];
+        push 0;
+        eq;
+        br {
+          true: {
+            push 1;
+            push arg[0];
+            sub;
+            call gen;
+            alloc node1;
+            ret;
+          }
+          false: {
+            push tmp[0];
+            push 1;
+            eq;
+            br {
+              true: {
+                push 1;
+                push arg[0];
+                sub;
+                tsave {
+                  push tmp[1];
+                  call gen;
+                  push tmp[1];
+                  call gen;
+                  alloc node2;
+                  ret;
+                };
+              }
+              false: {
+                push 1;
+                push arg[0];
+                sub;
+                tsave {
+                  push tmp[1];
+                  call gen;
+                  push tmp[1];
+                  call gen;
+                  push tmp[1];
+                  call gen;
+                  alloc node3;
+                  ret;
+                };
+              }
+            };
+          }
+        };
       };
     }
   };
diff --git a/tests/Asm/positive/test017.jva b/tests/Asm/positive/test017.jva
index 3151867032..495e53cb33 100644
--- a/tests/Asm/positive/test017.jva
+++ b/tests/Asm/positive/test017.jva
@@ -18,35 +18,36 @@ function h(integer -> integer, integer -> integer, integer) : integer {
 function f(integer) : integer -> integer {
   push arg[0];
   calloc g 1;
-  pusht;
-  push arg[0];
-  push 0;
-  eq;
-  br {
-    true: {
-      push 10;
-      tcall f;
-    }
-    false: {
-      push 10;
-      push arg[0];
-      lt;
-      br {
-        true: {
-          push 1;
-          push arg[0];
-          sub;
-          call f;
-          push tmp[0];
-          calloc h 2;
-          ret;
-        }
-        false: {
-          push tmp[0];
-          ret;
-        }
-      };
-    }
+  tsave {
+    push arg[0];
+    push 0;
+    eq;
+    br {
+      true: {
+        push 10;
+        tcall f;
+      }
+      false: {
+        push 10;
+        push arg[0];
+        lt;
+        br {
+          true: {
+            push 1;
+            push arg[0];
+            sub;
+            call f;
+            push tmp[0];
+            calloc h 2;
+            ret;
+          }
+          false: {
+            push tmp[0];
+            ret;
+          }
+        };
+      }
+    };
   };
 }
 
diff --git a/tests/Asm/positive/test031.jva b/tests/Asm/positive/test031.jva
index aafeab721c..6cf149f6cb 100644
--- a/tests/Asm/positive/test031.jva
+++ b/tests/Asm/positive/test031.jva
@@ -40,59 +40,64 @@ function f(tree) : integer {
       ret;
     }
     node: {
-      pusht;
-      push tmp[0].node[0];
-      call g;
-      pusht;
-      push tmp[0].node[1];
-      call g;
-      pusht;
-      push tmp[1];
-      case tree {
-        leaf: {
-          pop;
-          push 3;
-          push 0;
-          sub;
-        }
-        node: {
-          pusht;
-          push 32768;
-          push tmp[3].node[1];
-          call f;
-          push tmp[3].node[0];
-          call f;
-          add;
-          mod;
-          popt;
-        }
-      };
-      pusht;
-      push tmp[2];
-      case tree {
-        node: {
-          pusht;
-          push 32768;
-          push tmp[4].node[1];
-          call f;
-          push tmp[4].node[0];
-          call f;
-          add;
-          mod;
-          popt;
-        }
-        default: {
-          pop;
-          push 2;
-        }
+      tsave {
+        push tmp[0].node[0];
+        call g;
+        tsave {
+          push tmp[0].node[1];
+          call g;
+          tsave {
+            push tmp[1];
+            case tree {
+              leaf: {
+                pop;
+                push 3;
+                push 0;
+                sub;
+              }
+              node: {
+                save {
+                  push 32768;
+                  push tmp[3].node[1];
+                  call f;
+                  push tmp[3].node[0];
+                  call f;
+                  add;
+                  mod;
+                };
+              }
+            };
+            tsave {
+              push tmp[2];
+              case tree {
+                node: {
+                  save {
+                    push 32768;
+                    push tmp[4].node[1];
+                    call f;
+                    push tmp[4].node[0];
+                    call f;
+                    add;
+                    mod;
+                  };
+                }
+                default: {
+                  pop;
+                  push 2;
+                }
+              };
+              tsave {
+                push 32768;
+                push tmp[3];
+                push tmp[4];
+                mul;
+                mod;
+                ret;
+              };
+            };
+          };
+        };
       };
-      pusht;
-      push 32768;
-      push tmp[3];
-      push tmp[4];
-      mul;
-      mod;
-      ret;
     }
   };
 }
@@ -125,20 +130,21 @@ function g(tree) : tree {
       push arg[0];
       case tree {
         node: {
-          pusht;
-          push tmp[0].node[0];
-          call isNode;
-          br {
-            true: {
-              push tmp[0].node[1];
-              ret;
-            }
-            false: {
-              push tmp[0].node[1];
-              push tmp[0].node[0];
-              alloc node;
-              ret;
-            }
+          tsave {
+            push tmp[0].node[0];
+            call isNode;
+            br {
+              true: {
+                push tmp[0].node[1];
+                ret;
+              }
+              false: {
+                push tmp[0].node[1];
+                push tmp[0].node[0];
+                alloc node;
+                ret;
+              }
+            };
           };
         }
       };
diff --git a/tests/Asm/positive/test032.jva b/tests/Asm/positive/test032.jva
index cee8c6f04b..01429f3bf3 100644
--- a/tests/Asm/positive/test032.jva
+++ b/tests/Asm/positive/test032.jva
@@ -131,8 +131,9 @@ function pred((* -> *, *) -> *) : (* -> *, *) -> * {
   calloc pred_step 0;
   push arg[0];
   call $ 2;
-  pusht;
-  push tmp[0].pair[0];
+  save {
+    push tmp[0].pair[0];
+  };
   ret;
 }
 
@@ -161,26 +162,27 @@ function fib((* -> *, *) -> *) : (* -> *, *) -> * {
     false: {
       push arg[0];
       call pred;
-      pusht;
-      push tmp[0];
-      call isZero;
-      br {
-        true: {
-          calloc zero 0;
-          calloc succ 1;
-          calloc uncurry 1;
-          ret;
-        }
-        false: {
-          push tmp[0];
-          call pred;
-          call fib;
-          push tmp[0];
-          call fib;
-          calloc add 2;
-          calloc uncurry 1;
-          ret;
-        }
+      tsave {
+        push tmp[0];
+        call isZero;
+        br {
+          true: {
+            calloc zero 0;
+            calloc succ 1;
+            calloc uncurry 1;
+            ret;
+          }
+          false: {
+            push tmp[0];
+            call pred;
+            call fib;
+            push tmp[0];
+            call fib;
+            calloc add 2;
+            calloc uncurry 1;
+            ret;
+          }
+        };
       };
     }
   };
diff --git a/tests/Asm/positive/test036.jva b/tests/Asm/positive/test036.jva
index 3489a79107..3b9540bada 100644
--- a/tests/Asm/positive/test036.jva
+++ b/tests/Asm/positive/test036.jva
@@ -13,44 +13,46 @@ function force(unit -> stream) : stream {
 function filter(integer -> bool, unit -> stream, unit) : stream {
   push arg[1];
   call force;
-  pusht;
-  push tmp[0].cons[0];
-  push arg[0];
-  call $ 1;
-  br {
-    true: {
-      push tmp[0].cons[1];
-      push arg[0];
-      calloc filter 2;
-      push tmp[0].cons[0];
-      alloc cons;
-      ret;
-    }
-    false: {
-      push unit;
-      push tmp[0].cons[1];
-      push arg[0];
-      tcall filter;
-    }
+  tsave {
+    push tmp[0].cons[0];
+    push arg[0];
+    call $ 1;
+    br {
+      true: {
+        push tmp[0].cons[1];
+        push arg[0];
+        calloc filter 2;
+        push tmp[0].cons[0];
+        alloc cons;
+        ret;
+      }
+      false: {
+        push unit;
+        push tmp[0].cons[1];
+        push arg[0];
+        tcall filter;
+      }
+    };
   };
 }
 
 function nth(integer, unit -> stream) : integer {
   push arg[1];
   call force;
-  pusht;
-  push arg[0];
-  push 0;
-  eq;
-  br {
-    true: { push tmp[0].cons[0]; ret; }
-    false: {
-      push tmp[0].cons[1];
-      push 1;
-      push arg[0];
-      sub;
-      tcall nth;
-    }
+  tsave {
+    push arg[0];
+    push 0;
+    eq;
+    br {
+      true: { push tmp[0].cons[0]; ret; }
+      false: {
+        push tmp[0].cons[1];
+        push 1;
+        push arg[0];
+        sub;
+        tcall nth;
+      }
+    };
   };
 }
 
@@ -79,15 +81,16 @@ function indivisible(integer, integer) : bool {
 function eratostenes(unit -> stream, unit) : stream {
   push arg[0];
   call force;
-  pusht;
-  push tmp[0].cons[1];
-  push tmp[0].cons[0];
-  calloc indivisible 1;
-  calloc filter 2;
-  calloc eratostenes 1;
-  push tmp[0].cons[0];
-  alloc cons;
-  ret;
+  tsave {
+    push tmp[0].cons[1];
+    push tmp[0].cons[0];
+    calloc indivisible 1;
+    calloc filter 2;
+    calloc eratostenes 1;
+    push tmp[0].cons[0];
+    alloc cons;
+    ret;
+  };
 }
 
 function primes() : unit -> stream {