diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean
index 9ff3ab2ed..0bc80df72 100644
--- a/Strata/DL/Heap/HEval.lean
+++ b/Strata/DL/Heap/HEval.lean
@@ -156,6 +156,51 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE
     -- Second application to StringFieldAccess - return partially applied
     -- This handles str.fieldName where fieldName is a string literal
     evalStringFieldAccess state2 objExpr e2'
+  | .deferredOp "LengthAccess" _ =>
+    -- First application to LengthAccess - return partially applied
+    (state2, .app (.deferredOp "LengthAccess" none) e2')
+  | .app (.deferredOp "LengthAccess" _) objExpr =>
+    -- Second application to LengthAccess - evaluate
+    evalLengthAccess state2 objExpr e2'
+  | .deferredOp "FieldDelete" _ =>
+    -- First application to FieldDelete - return partially applied
+    (state2, .app (.deferredOp "FieldDelete" none) e2')
+  | .app (.deferredOp "FieldDelete" _) objExpr =>
+    -- Second application to FieldDelete - now we can evaluate
+    -- This handles delete obj[field] where field is dynamic
+    evalFieldDelete state2 objExpr e2'
+  | .deferredOp "ArrayShift" _ =>
+    -- ArrayShift applied once - now we can evaluate
+    evalArrayShift state2 e2'
+  | .deferredOp "ArrayUnshift" _ =>
+    -- First application to ArrayUnshift - return partially applied
+    (state2, .app (.deferredOp "ArrayUnshift" none) e2')
+  | .app (.deferredOp "ArrayUnshift" _) objExpr =>
+    -- Second application to ArrayUnshift - now we can evaluate
+    evalArrayUnshift state2 objExpr e2'
+  -- ArraySlice(obj, start?, end?) handling
+  | .deferredOp "ArraySlice" _ =>
+    -- First application: capture the array object
+    (state2, .app (.deferredOp "ArraySlice" none) e2')
+  | .app (.deferredOp "ArraySlice" _) objExpr =>
+    -- Second application: capture start
+    (state2, .app (.app (.deferredOp "ArraySlice" none) objExpr) e2')
+  | .app (.app (.deferredOp "ArraySlice" _) objExpr) startExpr =>
+    -- Third application: we have obj, start, and end -> evaluate
+    evalArraySlice state2 objExpr startExpr e2'
+
+  | .deferredOp "ArrayConcat" _ =>
+    -- First application to ArrayConcat - return partially applied
+    (state2, .app (.deferredOp "ArrayConcat" none) e2')
+  | .app (.deferredOp "ArrayConcat" _) arr1Expr =>
+    -- Second application to ArrayConcat - now we can evaluate
+    evalArrayConcat state2 arr1Expr e2'
+  | .deferredOp "ArrayJoin" _ =>
+    -- First application to ArrayJoin - return partially applied
+    (state2, .app (.deferredOp "ArrayJoin" none) e2')
+  | .app (.deferredOp "ArrayJoin" _) arrExpr =>
+    -- Second application to ArrayJoin - now we can evaluate
+    evalArrayJoin state2 arrExpr e2'
   | .deferredOp op _ =>
     -- First application to a deferred operation - return partially applied
     (state2, .app (.deferredOp op none) e2')
@@ -219,7 +264,239 @@ partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) :
     -- Field is not a string literal
     (state, .lambda (LExpr.const "error_non_literal_string_field" none))
 
--- Extract a numeric field index from an expression
+
+-- Handle length access for both strings and arrays
+partial def evalLengthAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr :=
+  match fieldExpr with
+  | .lambda (LExpr.const key _) =>
+    if key == "length" then
+      match objExpr with
+      | .lambda (LExpr.const s _) =>
+        -- String length
+        let len := s.length
+        (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int)))
+      | .address addr =>
+        -- Array length
+        match state.heap.get? addr with
+        | some obj =>
+          let len := obj.size
+          (state, .lambda (LExpr.const (toString len) (some Lambda.LMonoTy.int)))
+        | none =>
+          (state, .lambda (LExpr.const "error_invalid_address" none))
+      | _ =>
+        (state, .lambda (LExpr.const "error_not_string_or_array" none))
+    else
+      (state, .lambda (LExpr.const "error_unknown_length_property" none))
+  | _ =>
+    (state, .lambda (LExpr.const "error_non_literal_field" none))
+
+-- Handle field deletion: delete obj[field]
+partial def evalFieldDelete (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr :=
+  -- First try to extract a numeric field index from the field expression
+  match extractFieldIndex fieldExpr with
+  | some fieldIndex =>
+    -- We have a numeric field index, delete the field
+    match objExpr with
+    | .address addr =>
+      -- Delete field from the object at this address
+      match state.deleteField addr fieldIndex with
+      | some newState => (newState, objExpr)  -- Return the object address
+      | none => (state, .lambda (LExpr.const s!"error_cannot_delete_field_{fieldIndex}" none))
+    | _ =>
+      -- First evaluate the object expression to get an address
+      let (state1, objVal) := evalHExpr state objExpr
+      match objVal with
+      | .address addr =>
+        match state1.deleteField addr fieldIndex with
+        | some newState => (newState, objVal)
+        | none => (state1, .lambda (LExpr.const s!"error_cannot_delete_field_{fieldIndex}" none))
+      | _ =>
+        (state1, .lambda (LExpr.const "error_invalid_address_for_delete" none))
+  | none =>
+    -- Can't extract a numeric field index, return error
+    (state, .lambda (LExpr.const "error_field_delete_failed" none))
+
+-- Handle Array.prototype.slice semantics
+partial def evalArraySlice (state : HState) (objExpr startExpr endExpr : HExpr) : HState × HExpr :=
+  -- Ensure we have an address for the array object
+  let (state1, objVal) := evalHExpr state objExpr
+  -- Evaluate start/end arguments to simplify (handle negatives, computed exprs)
+  let (state2, startVal) := evalHExpr state1 startExpr
+  let (state3, endVal) := evalHExpr state2 endExpr
+  let someAddr? : Option Nat := match objVal with
+    | .address addr => some addr
+    | _ => none
+  match someAddr? with
+  | none => (state3, .lambda (LExpr.const "error_array_slice_invalid_object" none))
+  | some addr =>
+    match state3.heap.get? addr with
+    | none => (state3, .lambda (LExpr.const "error_array_slice_invalid_address" none))
+    | some obj =>
+      let len : Nat := obj.size
+      -- Helper to extract integer from Lambda const
+      let extractInt : HExpr → Option Int := fun e =>
+        match e with
+        | .lambda (LExpr.const s _) => s.toInt?
+        | _ => none
+      let resolveIndex (arg : HExpr) (defaultVal : Int) : Nat :=
+        let i : Int := match arg with
+          | .null => defaultVal
+          | _ => (extractInt arg).getD defaultVal
+        let i' : Int := if i < 0 then i + Int.ofNat len else i
+        let clamped : Int :=
+          if i' < 0 then 0
+          else if i' > Int.ofNat len then Int.ofNat len
+          else i'
+        Int.toNat clamped
+      let startIdx : Nat := resolveIndex startVal 0
+      let endIdx   : Nat := resolveIndex endVal (Int.ofNat len)
+      let finalStart := startIdx
+      let finalEnd := if endIdx < startIdx then startIdx else endIdx
+      -- Collect values in [finalStart, finalEnd) and reindex from 0
+      let rec collect (j : Nat) (i : Nat) (acc : List (Nat × HExpr)) : List (Nat × HExpr) :=
+        if i ≥ finalEnd then acc.reverse
+        else
+          match state3.getField addr i with
+          | some v => collect (j+1) (i+1) ((j, v) :: acc)
+          | none   => collect j (i+1) acc
+      let outFields := collect 0 finalStart []
+      -- Allocate a new array with these fields
+      evalHExpr state3 (.alloc (HMonoTy.mkObj outFields.length HMonoTy.int) outFields)
+
+-- Handle array shift: arr.shift() - removes first element and reindexes
+partial def evalArrayShift (state : HState) (objExpr : HExpr) : HState × HExpr :=
+  match objExpr with
+  | .address addr =>
+    match state.getObject addr with
+    | some obj =>
+      -- Get the value at index 0
+      let firstValue := obj.get? 0 |>.getD (.lambda (LExpr.const "undefined" none))
+
+      -- Get all fields and shift them down by 1
+      let fields := obj.toList
+      let shiftedFields := fields.filterMap fun (idx, value) =>
+        if idx > 0 then some (idx - 1, value) else none
+
+      -- Create new object with shifted fields
+      let newObj := Std.HashMap.ofList shiftedFields
+      let newHeap := state.heap.insert addr newObj
+      let newState := { state with heap := newHeap }
+
+      (newState, firstValue)
+    | none => (state, .lambda (LExpr.const "error_invalid_address" none))
+  | _ =>
+    -- Evaluate object expression first
+    let (state1, objVal) := evalHExpr state objExpr
+    evalArrayShift state1 objVal
+
+-- Handle array unshift: arr.unshift(value) - adds element at beginning and reindexes
+partial def evalArrayUnshift (state : HState) (objExpr valueExpr : HExpr) : HState × HExpr :=
+  match objExpr with
+  | .address addr =>
+    match state.getObject addr with
+    | some obj =>
+      -- First evaluate the value expression
+      let (state1, evaluatedValue) := evalHExpr state valueExpr
+
+      -- Get all fields and shift them up by 1
+      let fields := obj.toList
+      let shiftedFields := fields.map fun (idx, value) => (idx + 1, value)
+
+      -- Add new value at index 0
+      let newFields := (0, evaluatedValue) :: shiftedFields
+
+      -- Create new object with all fields
+      let newObj := Std.HashMap.ofList newFields
+      let newHeap := state1.heap.insert addr newObj
+      let newState := { state1 with heap := newHeap }
+
+      -- Return the new length
+      let newLength := newObj.size
+      (newState, .lambda (LExpr.const (toString newLength) (some Lambda.LMonoTy.int)))
+    | none => (state, .lambda (LExpr.const "error_invalid_address" none))
+  | _ =>
+    -- Evaluate object expression first
+    let (state1, objVal) := evalHExpr state objExpr
+    evalArrayUnshift state1 objVal valueExpr
+
+-- Handle array concat: arr1.concat(arr2) - concatenates two arrays, returns new array
+partial def evalArrayConcat (state : HState) (arr1Expr arr2Expr : HExpr) : HState × HExpr :=
+  -- First evaluate both array expressions to get addresses
+  let (state1, arr1Val) := evalHExpr state arr1Expr
+  let (state2, arr2Val) := evalHExpr state1 arr2Expr
+
+  match arr1Val, arr2Val with
+  | .address addr1, .address addr2 =>
+    match state2.getObject addr1, state2.getObject addr2 with
+    | some obj1, some obj2 =>
+      -- Get all fields from arr1
+      let arr1Fields := obj1.toList
+
+      -- Calculate the length of arr1 (highest index + 1)
+      let arr1Length := if arr1Fields.isEmpty then 0 else
+        (arr1Fields.map (·.1)).foldl Nat.max 0 + 1
+
+      -- Get all fields from arr2 and shift their indices by arr1Length
+      let arr2Fields := obj2.toList.map fun (idx, value) => (idx + arr1Length, value)
+
+      -- Combine all fields: arr1's fields followed by shifted arr2's fields
+      let combinedFields := arr1Fields ++ arr2Fields
+
+      -- Allocate a new array with the combined fields
+      let (newState, newAddr) := state2.alloc combinedFields
+
+      (newState, .address newAddr)
+    | _, _ => (state2, .lambda (LExpr.const "error_invalid_address" none))
+  | _, _ =>
+    -- One or both expressions didn't evaluate to addresses
+    (state2, .lambda (LExpr.const "error_invalid_array_for_concat" none))
+
+-- Handle array join: arr.join(separator?) - joins elements into a string
+partial def evalArrayJoin (state : HState) (arrExpr sepExpr : HExpr) : HState × HExpr :=
+  let (state1, arrVal) := evalHExpr state arrExpr
+  let (state2, sepVal) := evalHExpr state1 sepExpr
+  let formatToString : Std.Format → String := fun fmt => fmt.pretty 80
+  let separator : String :=
+    match sepVal with
+    | .null => ","
+    | .lambda (LExpr.const s _) => s
+    | _ =>
+      match sepVal.toLambda? with
+      | some (LExpr.const s _) => s
+      | _ => formatToString (repr sepVal)
+  match arrVal with
+  | .address addr =>
+    match state2.getObject addr with
+    | some _ =>
+      let len := state2.getArrayLength addr
+      let stringOf : HExpr → String := fun value =>
+        match value with
+        | .lambda (LExpr.const s _) => s
+        | .lambda _ => formatToString (repr value)
+        | .address _ => "[object Object]"
+        | .null => ""
+        | _ => formatToString (repr value)
+      let rec collect (idx : Nat) (st : HState) (acc : List String) : HState × List String :=
+        if idx ≥ len then (st, acc.reverse)
+        else
+          match st.getField addr idx with
+          | some rawVal =>
+            let (st1, evaluated) := evalHExpr st rawVal
+            let str := stringOf evaluated
+            collect (idx + 1) st1 (str :: acc)
+          | none =>
+            -- Sparse slot - treated as empty string but still contributes separator
+            collect (idx + 1) st ("" :: acc)
+      let (stateFinal, parts) := collect 0 state2 []
+      let resultString :=
+        match parts with
+        | [] => ""
+        | _ => String.intercalate separator parts
+      (stateFinal, Heap.HExpr.string resultString)
+    | none => (state2, .lambda (LExpr.const "error_invalid_address" none))
+  | _ =>
+    (state2, .lambda (LExpr.const "error_invalid_array_for_join" none))
+
 partial def extractFieldIndex (expr : HExpr) : Option Nat :=
   match expr with
   | .lambda (LExpr.const s _) =>
diff --git a/Strata/DL/Heap/HState.lean b/Strata/DL/Heap/HState.lean
index 4935049fc..c3a7fdee8 100644
--- a/Strata/DL/Heap/HState.lean
+++ b/Strata/DL/Heap/HState.lean
@@ -137,7 +137,7 @@ def getHeapVarNames (state : HState) : List String :=
 -- Allocate a new object in the heap
 def alloc (state : HState) (fields : List (Nat × HExpr)) : HState × Address :=
   let addr := state.nextAddr
-  let obj := Std.HashMap.ofList fields -- I think the fields need to be evaluated
+  let obj := Std.HashMap.ofList fields
   let newHeap := state.heap.insert addr obj
   let newState := { state with heap := newHeap, nextAddr := addr + 1 }
   (newState, addr)
@@ -161,6 +161,16 @@ def setField (state : HState) (addr : Address) (field : Nat) (value : HExpr) : O
     some { state with heap := newHeap }
   | none => none
 
+-- Delete a field from an object in the heap
+def deleteField (state : HState) (addr : Address) (field : Nat) : Option HState :=
+  match state.getObject addr with
+  | some obj =>
+    -- Remove the field from the object (obj is a HashMap, use erase)
+    let newObj := obj.erase field
+    let newHeap := state.heap.insert addr newObj
+    some { state with heap := newHeap }
+  | none => none
+
 -- Check if an address is valid (exists in heap)
 def isValidAddr (state : HState) (addr : Address) : Bool :=
   state.heap.contains addr
@@ -169,6 +179,17 @@ def isValidAddr (state : HState) (addr : Address) : Bool :=
 def getAllAddrs (state : HState) : List Address :=
   state.heap.toList.map (·.1)
 
+-- Get the logical length of an array (highest index + 1, ignoring gaps)
+def getArrayLength (state : HState) (addr : Address) : Nat :=
+  match state.getObject addr with
+  | some obj =>
+    let indices := obj.toList.map (·.1)
+    if indices.isEmpty then
+      0
+    else
+      indices.foldl Nat.max 0 + 1
+  | none => 0
+
 -- Pretty printing helpers
 def heapToString (state : HState) : String :=
   let entries := state.heap.toList
@@ -188,4 +209,4 @@ def toString (state : HState) : String :=
 
 end HState
 
-end Heap
+end Heap
\ No newline at end of file
diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean
index 7183bfcfc..d307a7b24 100644
--- a/Strata/Languages/TypeScript/TS_to_Strata.lean
+++ b/Strata/Languages/TypeScript/TS_to_Strata.lean
@@ -177,9 +177,9 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
     | .TS_IdExpression id =>
       let keyName := id.name
       if !e.computed && keyName == "length" then
-        -- String dot access: str.length
+        -- .length property access - use unified operation that handles both strings and arrays
         let keyExpr := Heap.HExpr.string keyName
-        Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "StringFieldAccess" none) objExpr) keyExpr
+        Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) keyExpr
       else
         -- Dynamic field access: obj[variable]
         let varExpr := translate_expr (.TS_IdExpression id)
@@ -201,10 +201,84 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
     -- Use allocSimple which handles the object type automatically
     Heap.HExpr.allocSimple fields
 
+  | .TS_UnaryExpression e =>
+    let arg := translate_expr e.argument
+    match e.operator with
+    | "-" =>
+      -- Unary minus: -x
+      Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) (Heap.HExpr.int 0)) arg
+    | "+" =>
+      -- Unary plus: +x (just return the argument)
+      arg
+    | "!" =>
+      -- Logical NOT: !x
+      Heap.HExpr.app (Heap.HExpr.deferredOp "Bool.Not" none) arg
+    | _ => panic! s!"Unsupported unary operator: {e.operator}"
+
   | .TS_CallExpression call =>
-    -- Handle function calls - translate to expressions for now
-    -- For now, create a placeholder that will be handled during call statement processing
-    Heap.HExpr.lambda (.fvar s!"call_{call.callee.name}" none)
+    match call.callee with
+      | .TS_MemberExpression member =>
+        -- Handle method calls like arr.push(x) or arr.pop()
+        let objExpr := translate_expr member.object
+        match member.property with
+        | .TS_IdExpression id =>
+          match id.name with
+          | "slice" =>
+            -- arr.slice(start?, end?) - return a new array (deferred op)
+            let startArg := match call.arguments[0]? with
+              | some a => translate_expr a
+              | none => Heap.HExpr.null
+            let endArg := match call.arguments[1]? with
+              | some a => translate_expr a
+              | none => Heap.HExpr.null
+            Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArraySlice" none) objExpr) startArg) endArg
+          | "push" =>
+            -- arr.push(value) - use DynamicFieldAssign with length as index
+            let valueExpr := translate_expr call.arguments[0]!
+            let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+            Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) lengthExpr) valueExpr
+          | "pop" =>
+            -- arr.pop() - read arr[arr.length - 1]
+            let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+            let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1)
+            Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) lastIndexExpr
+          | "shift" =>
+            -- arr.shift() - deferred operation that removes first element and reindexes
+            Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr
+          | "unshift" =>
+            -- arr.unshift(value) - single value only in expression context
+            if call.arguments.size != 1 then
+              panic! s!"unshift with multiple arguments in expression context not supported"
+            else
+              let valueExpr := translate_expr call.arguments[0]!
+              Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr
+          | "concat" =>
+            -- arr.concat(arr2, arr3, ...) - concatenate arrays, returns new array
+            let argExprs := call.arguments.toList.map translate_expr
+            if argExprs.isEmpty then
+              -- concat() with no arguments returns a copy of the original array
+              objExpr
+            else
+              -- Chain concat operations: concat(arr1, arr2, arr3) = concat(concat(arr1, arr2), arr3)
+              argExprs.foldl (fun acc argExpr =>
+                Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayConcat" none) acc) argExpr
+              ) objExpr
+          | "join" =>
+            -- arr.join(separator?) - join elements into a string
+            let separator :=
+              match call.arguments[0]? with
+              | some sepExpr => translate_expr sepExpr
+              | none => Heap.HExpr.string ","
+            Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayJoin" none) objExpr) separator
+          | methodName =>
+            Heap.HExpr.lambda (.fvar s!"call_{methodName}" none)
+        | _ =>
+          Heap.HExpr.lambda (.fvar "call_unknown_method" none)
+      | .TS_IdExpression id =>
+        -- Handle function calls - translate to expressions for now
+        Heap.HExpr.lambda (.fvar s!"call_{id.name}" none)
+      | _ =>
+        panic! s!"Unsupported call expression callee: {repr call.callee}"
 
   | _ => panic! s!"Unimplemented expression: {repr e}"
 
@@ -254,30 +328,123 @@ partial def translate_statement_core
         match decl.declarations[0]? with
         | .none => panic! "VariableDeclarations should have at least one declaration"
         | .some d =>
-          -- Check if this is a function call assignment
-          match d.init with
-          | .TS_CallExpression call =>
-            -- Handle function call assignment: let x = func(args)
-            dbg_trace s!"[DEBUG] Translating TypeScript function call assignment: {d.id.name} = {call.callee.name}(...)"
-            let args := call.arguments.toList.map translate_expr
-            dbg_trace s!"[DEBUG] Function call has {args.length} arguments"
-            let lhs := [d.id.name]  -- Left-hand side variables to store result
-            (ctx, [.cmd (.directCall lhs call.callee.name args)])
-          | _ =>
-            -- Handle simple variable declaration: let x = value
+          let defaultInit :=
             let value := translate_expr d.init
             let ty := get_var_type d.id.typeAnnotation d.init
             (ctx, [.cmd (.init d.id.name ty value)])
 
+          match d.init with
+          | .TS_CallExpression call =>
+            match call.callee with
+            | .TS_IdExpression id =>
+              dbg_trace s!"[DEBUG] Translating TypeScript function call assignment: {d.id.name} = {id.name}(...)"
+              let args := call.arguments.toList.map translate_expr
+              let lhs := [d.id.name]
+              (ctx, [.cmd (.directCall lhs id.name args)])
+            | .TS_MemberExpression member =>
+              match member.property with
+              | .TS_IdExpression methodId =>
+                if methodId.name == "pop" then
+                -- Handle Array.pop() method
+                  let objExpr := translate_expr member.object
+                  let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+                  let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1)
+                  let tempIndexInit := .cmd (.init "temp_pop_index" Heap.HMonoTy.int lastIndexExpr)
+                  let tempIndexVar := Heap.HExpr.lambda (.fvar "temp_pop_index" none)
+                  let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar
+                  let ty := infer_type_from_expr d.init
+                  let initStmt := .cmd (.init d.id.name ty valueExpr)
+                  let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "FieldDelete" none) objExpr) tempIndexVar) Heap.HExpr.null
+                  let deleteStmt := .cmd (.set "temp_delete_result" deleteExpr)
+                  (ctx, [tempIndexInit, initStmt, deleteStmt])
+                else if methodId.name == "shift" then
+                  let objExpr := translate_expr member.object
+                  let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr
+                  let ty := infer_type_from_expr d.init
+                  (ctx, [.cmd (.init d.id.name ty shiftExpr)])
+                else if methodId.name == "unshift" then
+                  -- Handle Array.unshift() with multiple arguments
+                  let objExpr := translate_expr member.object
+                  let valueExprs := call.arguments.toList.map translate_expr
+                  if valueExprs.isEmpty then
+                    defaultInit
+                  else
+                    -- Process all unshifts in reverse order
+                    -- valueExprs = [2, 1], reverse = [1, 2]
+                    -- We want to execute: unshift(1), then unshift(2)
+                    let reversed := valueExprs.reverse
+                    let allButLast := reversed.dropLast
+                    let lastValue := reversed.getLast!
+
+                    let tempStmts := allButLast.map (fun valueExpr =>
+                      let unshiftExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr
+                      (.cmd (.set "temp_unshift_result" unshiftExpr) : TSStrataStatement)
+                    )
+                    -- Last unshift assigns to the variable
+                    let lastUnshiftExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) lastValue
+                    let ty := Heap.HMonoTy.int
+                    let initStmt := .cmd (.init d.id.name ty lastUnshiftExpr)
+                    (ctx, tempStmts ++ [initStmt])
+
+                else
+                  defaultInit
+              | _ => defaultInit
+            | _ => defaultInit
+          | _ => defaultInit
+
       | .TS_ExpressionStatement expr =>
         match expr.expression with
         | .TS_CallExpression call =>
-          -- Handle standalone function call
-          dbg_trace s!"[DEBUG] Translating TypeScript standalone function call: {call.callee.name}(...)"
-          let args := call.arguments.toList.map translate_expr
-          dbg_trace s!"[DEBUG] Function call has {args.length} arguments"
-          let lhs := []  -- No left-hand side for standalone calls
-          (ctx, [.cmd (.directCall lhs call.callee.name args)])
+          match call.callee with
+          | .TS_MemberExpression member =>
+            -- Handle method calls like arr.push(x), arr.pop(), arr.shift(), arr.unshift(x)
+            let objExpr := translate_expr member.object
+            match member.property with
+            | .TS_IdExpression id =>
+              match id.name with
+              | "push" =>
+                -- arr.push(value) - use DynamicFieldAssign
+                let valueExpr := translate_expr call.arguments[0]!
+                let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+                let pushExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) lengthExpr) valueExpr
+                (ctx, [.cmd (.set "temp_push_result" pushExpr)])
+              | "pop" =>
+                -- arr.pop() standalone - read and delete
+                let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+                let lastIndexExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) lengthExpr) (Heap.HExpr.int 1)
+                let tempIndexInit := .cmd (.init "temp_pop_index" Heap.HMonoTy.int lastIndexExpr)
+                let tempIndexVar := Heap.HExpr.lambda (.fvar "temp_pop_index" none)
+                -- Read the value
+                let popExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) tempIndexVar
+                let readStmt := .cmd (.set "temp_pop_result" popExpr)
+                -- Delete the element
+                let deleteExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "FieldDelete" none) objExpr) tempIndexVar
+                let deleteStmt := .cmd (.set "temp_delete_result" deleteExpr)
+                (ctx, [tempIndexInit, readStmt, deleteStmt])
+              | "shift" =>
+                -- arr.shift() standalone
+                let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr
+                (ctx, [.cmd (.set "temp_shift_result" shiftExpr)])
+              | "unshift" =>
+                -- arr.unshift(val1, val2, ...) - expand to multiple single unshift statements
+                let valueExprs := call.arguments.toList.map translate_expr
+                let statements := valueExprs.reverse.map (fun valueExpr =>
+                  let unshiftExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayUnshift" none) objExpr) valueExpr
+                  (.cmd (.set "temp_unshift_result" unshiftExpr) : TSStrataStatement)
+                )
+                (ctx, statements)
+              | methodName =>
+                dbg_trace s!"[DEBUG] Translating method call: {methodName}(...)"
+                (ctx, [])
+            | _ => (ctx, [])
+          | .TS_IdExpression id =>
+            -- Handle standalone function call
+            dbg_trace s!"[DEBUG] Translating TypeScript standalone function call: {id.name}(...)"
+            let args := call.arguments.toList.map translate_expr
+            dbg_trace s!"[DEBUG] Function call has {args.length} arguments"
+            let lhs := []  -- No left-hand side for standalone calls
+            (ctx, [.cmd (.directCall lhs id.name args)])
+          | _ => (ctx, [])
         | .TS_AssignmentExpression assgn =>
           assert! assgn.operator == "="
           match assgn.left with
@@ -527,4 +694,4 @@ def describeTSStrataStatement (stmt: TSStrataStatement) : String :=
 
 --#eval translate_expr (.NumericLiteral {value := 42, extra := {raw := "42", rawValue := 42}, type := "NumericLiteral"})
 
-end TSStrata
+end TSStrata
\ No newline at end of file
diff --git a/Strata/Languages/TypeScript/js_ast.lean b/Strata/Languages/TypeScript/js_ast.lean
index 18efab8b3..64ef40c63 100644
--- a/Strata/Languages/TypeScript/js_ast.lean
+++ b/Strata/Languages/TypeScript/js_ast.lean
@@ -149,7 +149,7 @@ mutual
   deriving Repr, Lean.FromJson, Lean.ToJson
 
   structure TS_CallExpression extends BaseNode where
-    callee : TS_Identifier
+    callee : TS_Expression
     arguments : Array TS_Expression
   deriving Repr, Lean.FromJson, Lean.ToJson
 
@@ -171,6 +171,20 @@ mutual
   deriving Repr, Lean.FromJson, Lean.ToJson
 end
 
+instance : Inhabited TS_Expression where
+  default := .TS_NumericLiteral {
+    value := 0,
+    extra := { rawValue := 0, raw := "0" },
+    type := "NumericLiteral",
+    start_loc := 0,
+    end_loc := 0,
+    loc := {
+      start_loc := { line := 0, column := 0, index := 0 },
+      end_loc := { line := 0, column := 0, index := 0 },
+      identifierName := none
+    }
+  }
+
 structure TS_VariableDeclarator extends BaseNode where
   id : TS_Identifier
   init: TS_Expression
diff --git a/StrataTest/Languages/TypeScript/test_array_concat.ts b/StrataTest/Languages/TypeScript/test_array_concat.ts
new file mode 100644
index 000000000..7221bc310
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_array_concat.ts
@@ -0,0 +1,4 @@
+let arr1 = [1, 2, 3];
+let arr2 = [4, 5, 6];
+
+let combinedArr = arr1.concat(arr2);
\ No newline at end of file
diff --git a/StrataTest/Languages/TypeScript/test_array_join.ts b/StrataTest/Languages/TypeScript/test_array_join.ts
new file mode 100644
index 000000000..a6795887a
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_array_join.ts
@@ -0,0 +1,7 @@
+let arr_to_join: string[] = ["Hello", "world", "from", "Strata"];
+let joined_str1: string = arr_to_join.join();
+let joined_str2: string = arr_to_join.join(" ");
+
+let number_arr: number[] = [1, 2, 3, 4, 5];
+let joined_numbers: string = number_arr.join();
+let joined_numbers_with_dash: string = number_arr.join("-");
diff --git a/StrataTest/Languages/TypeScript/test_array_shift.ts b/StrataTest/Languages/TypeScript/test_array_shift.ts
new file mode 100644
index 000000000..532df7f1f
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_array_shift.ts
@@ -0,0 +1,20 @@
+let numbers1: number[] = [1, 2, 3, 4];
+
+// Shift removes the first element
+let shifted: number | undefined = numbers1.shift();
+
+// Array after shift
+// nums = [2, 3, 4]
+
+// Shift on empty array
+let emptyArr: number[] = [];
+let shiftedEmpty: number | undefined = emptyArr.shift();
+
+// Unshift adds an element to the beginning
+let newLen: number = numbers1.unshift(0);
+
+// Array after unshift
+// nums = [0, 2, 3, 4]
+
+// Unshift multiple elements
+let moreLen: number = numbers1.unshift(-2, 1)
diff --git a/StrataTest/Languages/TypeScript/test_array_slice.ts b/StrataTest/Languages/TypeScript/test_array_slice.ts
new file mode 100644
index 000000000..845120a35
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_array_slice.ts
@@ -0,0 +1,5 @@
+let arr: number[] = [10, 20, 30, 40, 50];
+let slicedArr1: number[] = arr.slice(1, 4);
+let slicedArr2: number[] = arr.slice(2);
+let slicedArr3: number[] = arr.slice();
+let slicedArr4: number[] = arr.slice(-3, -1);
\ No newline at end of file
diff --git a/StrataTest/Languages/TypeScript/test_arrays.ts b/StrataTest/Languages/TypeScript/test_arrays.ts
index 5d1409023..b9a473da7 100644
--- a/StrataTest/Languages/TypeScript/test_arrays.ts
+++ b/StrataTest/Languages/TypeScript/test_arrays.ts
@@ -1,6 +1,6 @@
 // Basic array literal
 // TODO: add assertion tests AST test + verification test (as a user) pre/post-condi
-let numbers: number[] = [1, 2, 3, 4, 5];
+let numbers: number[] = [1, 2, 3, 4];
 
 // Empty array initialization
 let empty: number[] = [];
@@ -21,9 +21,21 @@ numbers[index] = 30;
 let sum: number = numbers[0] + numbers[1];
 let isEqual: boolean = numbers[2] == 3
 
+let strings: string[] = ["hello", "world"];
+
+const numLen: number = numbers.length;
+const strLen: number = strings.length;
+
 // Mixed with objects
 // let data: number[] = [100, 200, 300];
 // let obj = {0: data[0], 1: data[1], 2: data[2]};
 
 // Nested arrays
-// let matrix: number[][] = [[1, 2], [3, 4]];
\ No newline at end of file
+// let matrix: number[][] = [[1, 2], [3, 4]];
+
+// Array Push and Pop
+numbers.push(6);
+let popped: number | undefined = numbers.pop();
+
+// Pop empty array
+empty.pop();
diff --git a/conformance_testing/babel_to_lean.py b/conformance_testing/babel_to_lean.py
index d0cbb08ec..6c92c54bc 100644
--- a/conformance_testing/babel_to_lean.py
+++ b/conformance_testing/babel_to_lean.py
@@ -78,7 +78,7 @@ def parse_conditional_expression(j):
 
 def parse_call_expression(j):
     target_j = {
-        "callee": parse_identifier(j['callee']),
+        "callee": parse_expression(j['callee']),
         "arguments": [parse_expression(arg) for arg in j['arguments']]
     }
     add_missing_node_info(j, target_j)