diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean
index 9ff3ab2ed..9a61b9d4f 100644
--- a/Strata/DL/Heap/HEval.lean
+++ b/Strata/DL/Heap/HEval.lean
@@ -156,6 +156,55 @@ 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'
+
+  -- 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 "ArrayShift" _ =>
+    -- ArrayShift applied once - now we can evaluate
+    evalArrayShift state2 e2'
+  | .deferredOp "ObjectKeys" _ =>
+    -- ObjectKeys applied once - now we can evaluate
+    evalObjectKeys 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'
+  | .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 +268,261 @@ 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
+
+partial def evalObjectKeys (state : HState) (objExpr : HExpr) : HState × HExpr :=
+  match objExpr with
+  | .address addr =>
+    match state.getObject addr with
+    | some obj =>
+      -- Get all field indices and sort them
+      let indices := obj.toList.map (·.1) |>.toArray.qsort (· < ·)
+
+      -- Create array with indices as integer values
+      let keyFields := indices.toList.mapIdx fun arrayIdx fieldIdx =>
+        (arrayIdx, .lambda (LExpr.const (toString fieldIdx) (some Lambda.LMonoTy.int)))
+
+      -- Allocate new array with the keys
+      let (newState, newAddr) := state.alloc keyFields
+      (newState, .address newAddr)
+    | none => (state, .lambda (LExpr.const "error_invalid_address" none))
+  | _ =>
+    -- Evaluate object expression first
+    let (state1, objVal) := evalHExpr state objExpr
+    evalObjectKeys 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 _) =>
@@ -255,4 +558,4 @@ def allocSimple (fields : List (Nat × HExpr)) : HExpr :=
 
 end HExpr
 
-end Heap
+end Heap
\ No newline at end of file
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 404c91635..0bb9a3980 100644
--- a/Strata/Languages/TypeScript/TS_to_Strata.lean
+++ b/Strata/Languages/TypeScript/TS_to_Strata.lean
@@ -142,6 +142,18 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
     -- Use deferred conditional instead of toLambda? checks
     Heap.HExpr.deferredIte guard consequent alternate
 
+  | .TS_UnaryExpression e =>
+    match e.operator with
+    | "-" =>
+      -- Numeric negation: translate as 0 - arg
+      let arg := translate_expr e.argument
+      Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Sub" none) (Heap.HExpr.int 0)) arg
+    | "!" =>
+      -- Logical not: use Bool.Not deferred op
+      let arg := translate_expr e.argument
+      Heap.HExpr.app (Heap.HExpr.deferredOp "Bool.Not" none) arg
+    | op => panic! s!"Unsupported unary operator: {op}"
+
   | .TS_NumericLiteral n =>
     dbg_trace s!"[DEBUG] Translating numeric literal value={n.value}, raw={n.extra.raw}, rawValue={n.extra.rawValue}"
     Heap.HExpr.int n.extra.raw.toInt!
@@ -177,9 +189,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)
@@ -202,9 +214,69 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
     Heap.HExpr.allocSimple fields
 
   | .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}"
 
   | .TS_FunctionExpression e =>
   -- Translate function definition
@@ -270,15 +342,69 @@ 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)])
+            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 =>
+              let objExpr := translate_expr member.object
+              match member.property with
+              | .TS_IdExpression id =>
+                match id.name with
+                | "pop" =>
+                  -- Handle Array.pop() method
+                  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 := get_var_type d.id.typeAnnotation 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])
+                | "shift" =>
+                  -- Handle Array.shift() method
+                  let shiftExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ArrayShift" none) objExpr
+                  let ty := get_var_type d.id.typeAnnotation d.init
+                  (ctx, [.cmd (.init d.id.name ty shiftExpr)])
+                | "unshift" =>
+                  -- Handle Array.unshift() with multiple arguments
+                  let valueExprs := call.arguments.toList.map translate_expr
+                  if valueExprs.isEmpty then
+                    let value := translate_expr d.init
+                    let ty := get_var_type d.id.typeAnnotation d.init
+                    (ctx, [.cmd (.init d.id.name ty value)])
+                  else
+                    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)
+                    )
+                    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])
+                | methodName =>
+                  dbg_trace s!"[DEBUG] Translating method call assignment: {d.id.name} = obj.{methodName}(...)"
+                  let value := translate_expr d.init
+                  let ty := get_var_type d.id.typeAnnotation d.init
+                  (ctx, [.cmd (.init d.id.name ty value)])
+              | _ =>
+                let value := translate_expr d.init
+                let ty := get_var_type d.id.typeAnnotation d.init
+                (ctx, [.cmd (.init d.id.name ty value)])
+            | _ =>
+              let value := translate_expr d.init
+              let ty := get_var_type d.id.typeAnnotation d.init
+              (ctx, [.cmd (.init d.id.name ty value)])
+
           | .TS_FunctionExpression funcExpr =>
             -- Handle function expression assignment: let x = function(...) { ... }
             let funcName := d.id.name
@@ -291,14 +417,14 @@ partial def translate_statement_core
               name := funcName,
               params := funcExpr.params.toList.map (·.name),
               body := funcBody,
-              returnType := none  -- We'll infer this later if needed
+              returnType := none
             }
             let newCtx := ctx.addFunction strataFunc
             dbg_trace s!"[DEBUG] Added function '{funcName}' to context"
-            -- Initialize variable to the function reference
             let ty := get_var_type d.id.typeAnnotation d.init
             let funcRef := Heap.HExpr.lambda (.fvar funcName none)
             (newCtx, [.cmd (.init d.id.name ty funcRef)])
+
           | .TS_ArrowFunctionExpression funcExpr =>
             -- Handle arrow function assignment: let x = (args) => { ... }
             let funcName := d.id.name
@@ -311,14 +437,14 @@ partial def translate_statement_core
               name := funcName,
               params := funcExpr.params.toList.map (·.name),
               body := funcBody,
-              returnType := none  -- We'll infer this later if needed
+              returnType := none
             }
             let newCtx := ctx.addFunction strataFunc
             dbg_trace s!"[DEBUG] Added arrow function '{funcName}' to context"
-            -- Initialize variable to the function reference
             let ty := get_var_type d.id.typeAnnotation d.init
             let funcRef := Heap.HExpr.lambda (.fvar funcName none)
             (newCtx, [.cmd (.init d.id.name ty funcRef)])
+
           | _ =>
             -- Handle simple variable declaration: let x = value
             let value := translate_expr d.init
@@ -328,12 +454,56 @@ partial def translate_statement_core
       | .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
@@ -415,7 +585,6 @@ partial def translate_statement_core
                 let fieldExpr := translate_expr member.property
                 let assignExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) fieldExpr) valueExpr
                 (ctx, [.cmd (.set "temp_assign_result" assignExpr)])
-          --| _ => panic! s!"Unsupported assignment target: {repr assgn.left}"
         | .TS_FunctionExpression funcExpr =>
           -- Handle standalone function expression (immediately invoked function expression - IIFE)
           let funcName := s!"__anon_func_{funcExpr.start_loc}_{funcExpr.end_loc}"
@@ -557,115 +726,218 @@ partial def translate_statement_core
         let bodyBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := bodyStmts }
         (bodyCtx, [ initBreakFlag, .loop combinedCondition none none bodyBlock ])
 
-        | .TS_ForStatement forStmt =>
-          dbg_trace s!"[DEBUG] Translating for statement at loc {forStmt.start_loc}-{forStmt.end_loc}"
-
-          let continueLabel := s!"for_continue_{forStmt.start_loc}"
-          let breakLabel := s!"for_break_{forStmt.start_loc}"
-          let breakFlagVar := s!"for_break_flag_{forStmt.start_loc}"
-
-          -- Initialize break flag to false
-          let initBreakFlag : TSStrataStatement := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false)
-
-          -- init phase
-          let (_, initStmts) := translate_statement_core (.TS_VariableDeclaration forStmt.init) ctx
-          -- guard (test)
-          let guard := translate_expr forStmt.test
-          -- body (first translate loop body with break support)
-          let (ctx1, bodyStmts) :=
-              translate_statement_core forStmt.body ctx
-                { continueLabel? := some continueLabel, breakLabel? := some breakLabel, breakFlagVar? := some breakFlagVar }
-          -- update (translate expression into statements following ExpressionStatement style)
-          let (_, updateStmts) :=
-              translate_statement_core
-                (.TS_ExpressionStatement {
-                  expression := .TS_AssignmentExpression forStmt.update,
-                  start_loc := forStmt.start_loc,
-                  end_loc := forStmt.end_loc,
-                  loc := forStmt.loc,
-                  type := "TS_AssignmentExpression"
-                }) ctx1
-
-          -- Modify loop condition to include break flag check: (original_condition && !break_flag)
-          let breakFlagExpr := Heap.HExpr.lambda (.fvar breakFlagVar none)
-          let combinedCondition := Heap.HExpr.deferredIte breakFlagExpr Heap.HExpr.false guard
-
-          -- assemble loop body (body + update)
-          let loopBody : Imperative.Block TSStrataExpression TSStrataCommand :=
-            { ss := bodyStmts ++ updateStmts }
-
-          -- output: init break flag, init statements, then a loop statement
-          (ctx1, [initBreakFlag] ++ initStmts ++ [ .loop combinedCondition none none loopBody])
-
-        | .TS_SwitchStatement switchStmt =>
-          -- Handle switch statement: switch discriminant { cases }
-
-          -- Process all cases in their original order, separating regular from default
-          let allCases := switchStmt.cases.toList
-          let (regularCaseStmts, defaultStmts) := allCases.foldl (fun (regCases, defStmts) case =>
-            match case.test with
-            | some expr =>
-              -- Regular case
-              let discrimExpr := translate_expr switchStmt.discriminant
-              let caseValue := translate_expr expr
-              let testExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Eq" none) discrimExpr) caseValue
-              let (caseCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt =>
-                let (newCtx, newStmts) := translate_statement_core stmt accCtx
-                (newCtx, accStmts ++ newStmts)) (ctx, [])
-              (regCases ++ [(testExpr, stmts)], defStmts)
-            | none =>
-              -- Default case
-              let (defaultCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt =>
-                let (newCtx, newStmts) := translate_statement_core stmt accCtx
-                (newCtx, accStmts ++ newStmts)) (ctx, [])
-              (regCases, stmts)
-          ) ([], [])
-
-          -- Build nested if-then-else structure for regular cases
-          let rec build_cases (cases: List (Heap.HExpr × List TSStrataStatement)) (defaultStmts: List TSStrataStatement) : TSStrataStatement :=
-            match cases with
-            | [] =>
-              -- No regular cases, just execute default if it exists
-              let defaultBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts }
-              .block "default" defaultBlock
-            | [(test, stmts)] =>
-              let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts }
-              let elseBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts }
-              .ite test thenBlock elseBlock
-            | (test, stmts) :: rest =>
-              let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts }
-              let elseBlock := build_cases rest defaultStmts
-              let elseBlockWrapped : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [elseBlock] }
-              .ite test thenBlock elseBlockWrapped
-
-          let switchStructure := build_cases regularCaseStmts defaultStmts
-          (ctx, [switchStructure])
-
-        | .TS_ContinueStatement cont =>
+      | .TS_ForInStatement forInStmt =>
+        dbg_trace s!"[DEBUG] Translating for-in statement at loc {forInStmt.start_loc}-{forInStmt.end_loc}"
+
+        let continueLabel := s!"forin_continue_{forInStmt.start_loc}"
+        let breakLabel := s!"forin_break_{forInStmt.start_loc}"
+        let breakFlagVar := s!"forin_break_flag_{forInStmt.start_loc}"
+
+        let keyVarName := match forInStmt.left.declarations[0]? with
+          | some decl => decl.id.name
+          | none => panic! "for-in must have loop variable"
+
+        let objExpr := translate_expr forInStmt.right
+
+        let keysVar := s!"__keys_{forInStmt.start_loc}"
+        let indexVar := s!"__index_{forInStmt.start_loc}"
+        let lengthVar := s!"__length_{forInStmt.start_loc}"
+
+        let keysExpr := Heap.HExpr.app (Heap.HExpr.deferredOp "ObjectKeys" none) objExpr
+        let initKeys := .cmd (.init keysVar Heap.HMonoTy.addr keysExpr)
+
+        let keysVarExpr := Heap.HExpr.lambda (.fvar keysVar none)
+        let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) keysVarExpr) (Heap.HExpr.string "length")
+        let initLength := .cmd (.init lengthVar Heap.HMonoTy.int lengthExpr)
+
+        let initIndex := .cmd (.init indexVar Heap.HMonoTy.int (Heap.HExpr.int 0))
+
+        let initBreakFlag := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false)
+
+        let indexVarExpr := Heap.HExpr.lambda (.fvar indexVar none)
+        let lengthVarExpr := Heap.HExpr.lambda (.fvar lengthVar none)
+        let indexCheck := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) indexVarExpr) lengthVarExpr
+        let breakFlagExpr := Heap.HExpr.lambda (.fvar breakFlagVar none)
+        let guard := Heap.HExpr.deferredIte breakFlagExpr Heap.HExpr.false indexCheck
+
+        let getCurrentKey := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) keysVarExpr) indexVarExpr
+        let setKeyVar := .cmd (.init keyVarName Heap.HMonoTy.int getCurrentKey)
+
+        let (bodyCtx, userBodyStmts) := translate_statement_core forInStmt.body ctx
+          { continueLabel? := some continueLabel,
+            breakLabel? := some breakLabel,
+            breakFlagVar? := some breakFlagVar }
+
+        let incrementExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) indexVarExpr) (Heap.HExpr.int 1)
+        let incrementIndex := .cmd (.set indexVar incrementExpr)
+
+        let loopBodyStmts := [setKeyVar] ++ userBodyStmts ++ [incrementIndex]
+        let bodyBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := loopBodyStmts }
+
+        (bodyCtx, [initBreakFlag, initKeys, initLength, initIndex, .loop guard none none bodyBlock])
+
+      | .TS_ForOfStatement forOfStmt =>
+        dbg_trace s!"[DEBUG] Translating for-of statement at loc {forOfStmt.start_loc}-{forOfStmt.end_loc}"
+
+        let continueLabel := s!"forof_continue_{forOfStmt.start_loc}"
+        let breakLabel := s!"forof_break_{forOfStmt.start_loc}"
+        let breakFlagVar := s!"forof_break_flag_{forOfStmt.start_loc}"
+
+        -- Extract loop variable name
+        let valueVarName := match forOfStmt.left.declarations[0]? with
+          | some decl => decl.id.name
+          | none => panic! "for-of must have loop variable"
+
+        -- Array to iterate over
+        let arrExpr := translate_expr forOfStmt.right
+
+        -- Create temporary variables for iteration
+        let indexVar := s!"__index_{forOfStmt.start_loc}"
+        let lengthVar := s!"__length_{forOfStmt.start_loc}"
+
+        -- Get length of array
+        let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) arrExpr) (Heap.HExpr.string "length")
+        let initLength := .cmd (.init lengthVar Heap.HMonoTy.int lengthExpr)
+
+        -- Initialize index to 0
+        let initIndex := .cmd (.init indexVar Heap.HMonoTy.int (Heap.HExpr.int 0))
+
+        -- Initialize break flag
+        let initBreakFlag := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false)
+
+        -- Loop guard: index < length && !breakFlag
+        let indexVarExpr := Heap.HExpr.lambda (.fvar indexVar none)
+        let lengthVarExpr := Heap.HExpr.lambda (.fvar lengthVar none)
+        let indexCheck := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) indexVarExpr) lengthVarExpr
+        let breakFlagExpr := Heap.HExpr.lambda (.fvar breakFlagVar none)
+        let guard := Heap.HExpr.deferredIte breakFlagExpr Heap.HExpr.false indexCheck
+
+        let getCurrentValue := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) arrExpr) indexVarExpr
+        let setValueVar := .cmd (.set valueVarName getCurrentValue)
+
+        let (bodyCtx, userBodyStmts) := translate_statement_core forOfStmt.body ctx
+          { continueLabel? := some continueLabel,
+            breakLabel? := some breakLabel,
+            breakFlagVar? := some breakFlagVar }
+
+        let incrementExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) indexVarExpr) (Heap.HExpr.int 1)
+        let incrementIndex := .cmd (.set indexVar incrementExpr)
+
+        let initValueVar := .cmd (.init valueVarName Heap.HMonoTy.int (Heap.HExpr.int 0))
+
+        let loopBodyStmts := [setValueVar] ++ userBodyStmts ++ [incrementIndex]
+        let bodyBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := loopBodyStmts }
+
+        (bodyCtx, [initBreakFlag, initLength, initIndex, initValueVar, .loop guard none none bodyBlock])
+      | .TS_ForStatement forStmt =>
+        dbg_trace s!"[DEBUG] Translating for statement at loc {forStmt.start_loc}-{forStmt.end_loc}"
+
+        let continueLabel := s!"for_continue_{forStmt.start_loc}"
+        let breakLabel := s!"for_break_{forStmt.start_loc}"
+        let breakFlagVar := s!"for_break_flag_{forStmt.start_loc}"
+
+        -- Initialize break flag to false
+        let initBreakFlag : TSStrataStatement := .cmd (.init breakFlagVar Heap.HMonoTy.bool Heap.HExpr.false)
+
+        -- init phase
+        let (_, initStmts) := translate_statement_core (.TS_VariableDeclaration forStmt.init) ctx
+        -- guard (test)
+        let guard := translate_expr forStmt.test
+        -- body (first translate loop body with break support)
+        let (ctx1, bodyStmts) :=
+            translate_statement_core forStmt.body ctx
+              { continueLabel? := some continueLabel, breakLabel? := some breakLabel, breakFlagVar? := some breakFlagVar }
+        -- update (translate expression into statements following ExpressionStatement style)
+        let (_, updateStmts) :=
+            translate_statement_core
+              (.TS_ExpressionStatement {
+                expression := .TS_AssignmentExpression forStmt.update,
+                start_loc := forStmt.start_loc,
+                end_loc := forStmt.end_loc,
+                loc := forStmt.loc,
+                type := "TS_AssignmentExpression"
+              }) ctx1
+
+        -- Modify loop condition to include break flag check: (original_condition && !break_flag)
+        let breakFlagExpr := Heap.HExpr.lambda (.fvar breakFlagVar none)
+        let combinedCondition := Heap.HExpr.deferredIte breakFlagExpr Heap.HExpr.false guard
+
+        -- assemble loop body (body + update)
+        let loopBody : Imperative.Block TSStrataExpression TSStrataCommand :=
+          { ss := bodyStmts ++ updateStmts }
+
+        -- output: init break flag, init statements, then a loop statement
+        (ctx1, [initBreakFlag] ++ initStmts ++ [ .loop combinedCondition none none loopBody])
+
+      | .TS_SwitchStatement switchStmt =>
+        -- Handle switch statement: switch discriminant { cases }
+
+        -- Process all cases in their original order, separating regular from default
+        let allCases := switchStmt.cases.toList
+        let (regularCaseStmts, defaultStmts) := allCases.foldl (fun (regCases, defStmts) case =>
+          match case.test with
+          | some expr =>
+            -- Regular case
+            let discrimExpr := translate_expr switchStmt.discriminant
+            let caseValue := translate_expr expr
+            let testExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Eq" none) discrimExpr) caseValue
+            let (caseCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt =>
+              let (newCtx, newStmts) := translate_statement_core stmt accCtx
+              (newCtx, accStmts ++ newStmts)) (ctx, [])
+            (regCases ++ [(testExpr, stmts)], defStmts)
+          | none =>
+            -- Default case
+            let (defaultCtx, stmts) := case.consequent.foldl (fun (accCtx, accStmts) stmt =>
+              let (newCtx, newStmts) := translate_statement_core stmt accCtx
+              (newCtx, accStmts ++ newStmts)) (ctx, [])
+            (regCases, stmts)
+        ) ([], [])
+
+        -- Build nested if-then-else structure for regular cases
+        let rec build_cases (cases: List (Heap.HExpr × List TSStrataStatement)) (defaultStmts: List TSStrataStatement) : TSStrataStatement :=
+          match cases with
+          | [] =>
+            -- No regular cases, just execute default if it exists
+            let defaultBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts }
+            .block "default" defaultBlock
+          | [(test, stmts)] =>
+            let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts }
+            let elseBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := defaultStmts }
+            .ite test thenBlock elseBlock
+          | (test, stmts) :: rest =>
+            let thenBlock : Imperative.Block TSStrataExpression TSStrataCommand := { ss := stmts }
+            let elseBlock := build_cases rest defaultStmts
+            let elseBlockWrapped : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [elseBlock] }
+            .ite test thenBlock elseBlockWrapped
+
+        let switchStructure := build_cases regularCaseStmts defaultStmts
+        (ctx, [switchStructure])
+
+      | .TS_ContinueStatement cont =>
+        let tgt :=
+          match ct.continueLabel? with
+          | some lab => lab
+          | none     =>
+              dbg_trace "[WARN] `continue` encountered outside of a loop; emitting goto to __unbound_continue";
+              "__unbound_continue"
+        (ctx, [ .goto tgt ])
+
+      | .TS_BreakStatement brk =>
+        -- Handle break statement if loop context fails to handle it
+        dbg_trace "[WARN] `break` statement not handled by pattern matching";
+        match ct.breakFlagVar? with
+        | some flagVar =>
+          -- Set break flag to true as fallback
+          (ctx, [ .cmd (.set flagVar Heap.HExpr.true) ])
+        | none =>
+          dbg_trace "[WARN] `break` encountered outside of a loop; using fallback goto";
           let tgt :=
-            match ct.continueLabel? with
+            match ct.breakLabel? with
             | some lab => lab
-            | none     =>
-                dbg_trace "[WARN] `continue` encountered outside of a loop; emitting goto to __unbound_continue";
-                "__unbound_continue"
+            | none     => "__unbound_break"
           (ctx, [ .goto tgt ])
 
-        | .TS_BreakStatement brk =>
-          -- Handle break statement if loop context fails to handle it
-          dbg_trace "[WARN] `break` statement not handled by pattern matching";
-          match ct.breakFlagVar? with
-          | some flagVar =>
-            -- Set break flag to true as fallback
-            (ctx, [ .cmd (.set flagVar Heap.HExpr.true) ])
-          | none =>
-            dbg_trace "[WARN] `break` encountered outside of a loop; using fallback goto";
-            let tgt :=
-              match ct.breakLabel? with
-              | some lab => lab
-              | none     => "__unbound_break"
-            (ctx, [ .goto tgt ])
-
-        | _ => panic! s!"Unimplemented statement: {repr s}"
+      | _ => panic! s!"Unimplemented statement: {repr s}"
 
 -- Translate TypeScript statements to TypeScript-Strata statements
 partial def translate_statement (s: TS_Statement) (ctx : TranslationContext) : TranslationContext × List TSStrataStatement :=
@@ -714,8 +986,4 @@ def describeTSStrataStatement (stmt: TSStrataStatement) : String :=
   | .goto label _ =>
     s!"goto {label}"
 
-
-
---#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 73568e381..9861150c4 100644
--- a/Strata/Languages/TypeScript/js_ast.lean
+++ b/Strata/Languages/TypeScript/js_ast.lean
@@ -51,11 +51,6 @@ mutual
   structure TS_TSArrayType extends BaseNode where
     elementType : TS_TSTypeKeyword
   deriving Repr, Lean.FromJson, Lean.ToJson
-
-  -- TODO: Array not as a type?
-  -- structure TS_TSArrayType extends BaseNode where
-    -- elementType : TS_TSTypeKeyword
-  -- deriving Repr, Lean.FromJson, Lean.ToJson
 end
 
 structure TS_TSTypeAnnotation extends BaseNode where
@@ -67,7 +62,6 @@ structure TS_Identifier extends BaseNode where
   typeAnnotation : Option TS_TSTypeAnnotation
 deriving Repr, Lean.FromJson, Lean.ToJson
 
-
 structure TS_Parameter extends BaseNode where
   name : String
   typeAnnotation : TS_TSTypeAnnotation
@@ -95,7 +89,51 @@ deriving Repr, Lean.FromJson, Lean.ToJson
 structure TS_NullLiteral extends BaseNode where
 deriving Repr, Lean.FromJson, Lean.ToJson
 
+structure TS_Comment extends BaseNode where
+deriving Repr, Lean.FromJson, Lean.ToJson
+
 mutual
+  inductive TS_Expression where
+    | TS_BinaryExpression : TS_BinaryExpression → TS_Expression
+    | TS_ConditionalExpression : TS_ConditionalExpression → TS_Expression
+    | TS_LogicalExpression : TS_LogicalExpression → TS_Expression
+    | TS_AssignmentExpression : TS_AssignmentExpression → TS_Expression
+    | TS_NumericLiteral : TS_NumericLiteral → TS_Expression
+    | TS_BooleanLiteral : TS_BooleanLiteral → TS_Expression
+    | TS_StringLiteral : TS_StringLiteral → TS_Expression
+    | TS_NullLiteral : TS_NullLiteral → TS_Expression
+    | TS_IdExpression : TS_Identifier → TS_Expression
+    | TS_UnaryExpression: TS_UnaryExpression → TS_Expression
+    | TS_ObjectExpression: TS_ObjectExpression → TS_Expression
+    | TS_ArrayExpression: TS_ArrayExpression → TS_Expression
+    | TS_MemberExpression: TS_MemberExpression → TS_Expression
+    | TS_CallExpression: TS_CallExpression → TS_Expression
+    | TS_FunctionExpression: TS_FunctionExpression → TS_Expression
+    | TS_ArrowFunctionExpression: TS_ArrowFunctionExpression → TS_Expression
+  deriving Repr, Lean.FromJson, Lean.ToJson
+
+  inductive TS_Statement where
+    | TS_IfStatement : TS_IfStatement → TS_Statement
+    | TS_VariableDeclaration : TS_VariableDeclaration → TS_Statement
+    | TS_ExpressionStatement : TS_ExpressionStatement → TS_Statement
+    | TS_BlockStatement : TS_BlockStatement → TS_Statement
+    | TS_ThrowStatement : TS_ThrowStatement → TS_Statement
+    | TS_ReturnStatement : TS_ReturnStatement → TS_Statement
+    | TS_FunctionDeclaration : TS_FunctionDeclaration → TS_Statement
+    | TS_ForStatement : TS_ForStatement → TS_Statement
+    | TS_WhileStatement: TS_WhileStatement → TS_Statement
+    | TS_BreakStatement : TS_BreakStatement → TS_Statement
+    | TS_SwitchStatement : TS_SwitchStatement → TS_Statement
+    | TS_ContinueStatement: TS_ContinueStatement → TS_Statement
+    | TS_ForInStatement : TS_ForInStatement → TS_Statement
+    | TS_ForOfStatement : TS_ForOfStatement → TS_Statement
+  deriving Repr, Lean.FromJson, Lean.ToJson
+
+  inductive TS_AssignmentIdentifier where
+    | TS_Identifier : TS_Identifier → TS_AssignmentIdentifier
+    | TS_MemberExpression: TS_MemberExpression → TS_AssignmentIdentifier
+  deriving Repr, Lean.FromJson, Lean.ToJson
+
   structure TS_MemberExpression extends BaseNode where
     object: TS_Expression
     property: TS_Expression
@@ -109,9 +147,9 @@ mutual
   deriving Repr, Lean.FromJson, Lean.ToJson
 
   structure TS_ConditionalExpression extends BaseNode where
-      test : TS_Expression
-      consequent : TS_Expression
-      alternate : TS_Expression
+    test : TS_Expression
+    consequent : TS_Expression
+    alternate : TS_Expression
   deriving Repr, Lean.FromJson, Lean.ToJson
 
   structure TS_LogicalExpression extends BaseNode where
@@ -120,10 +158,6 @@ mutual
     right : TS_Expression
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-  inductive TS_AssignmentIdentifier where
-    | TS_Identifier : TS_Identifier → TS_AssignmentIdentifier
-    | TS_MemberExpression: TS_MemberExpression → TS_AssignmentIdentifier
-
   structure TS_AssignmentExpression extends BaseNode where
     operator: String
     left: TS_AssignmentIdentifier
@@ -137,7 +171,6 @@ mutual
 
   structure TS_ObjectProperty extends BaseNode where
     method: Bool
-    -- Key can be any expression (NumericLiteral, StringLiteral, etc.)
     key: TS_Expression
     computed: Bool
     shorthand: Bool
@@ -153,15 +186,11 @@ 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
 
   structure TS_FunctionExpression extends BaseNode where
-    -- id : TS_Identifier
-    -- expression : Bool
-    -- generator : Bool
-    -- async : Bool
     params : Array TS_Identifier
     body: TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
@@ -171,26 +200,6 @@ mutual
     body: TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-  inductive TS_Expression where
-    | TS_BinaryExpression : TS_BinaryExpression → TS_Expression
-    | TS_ConditionalExpression : TS_ConditionalExpression → TS_Expression
-    | TS_LogicalExpression : TS_LogicalExpression → TS_Expression
-    | TS_AssignmentExpression : TS_AssignmentExpression → TS_Expression
-    | TS_NumericLiteral : TS_NumericLiteral → TS_Expression
-    | TS_BooleanLiteral : TS_BooleanLiteral → TS_Expression
-    | TS_StringLiteral : TS_StringLiteral → TS_Expression
-    | TS_NullLiteral : TS_NullLiteral → TS_Expression
-    | TS_IdExpression : TS_Identifier → TS_Expression
-    | TS_UnaryExpression: TS_UnaryExpression → TS_Expression
-    | TS_ObjectExpression: TS_ObjectExpression → TS_Expression
-    | TS_ArrayExpression: TS_ArrayExpression → TS_Expression
-    | TS_MemberExpression: TS_MemberExpression → TS_Expression
-    | TS_CallExpression: TS_CallExpression → TS_Expression
-    | TS_FunctionExpression: TS_FunctionExpression → TS_Expression
-    | TS_ArrowFunctionExpression: TS_ArrowFunctionExpression → TS_Expression
-  deriving Repr, Lean.FromJson, Lean.ToJson
-
-
   structure TS_VariableDeclarator extends BaseNode where
     id : TS_Identifier
     init: TS_Expression
@@ -212,11 +221,9 @@ mutual
     argument: TS_Expression
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-
   structure TS_BlockStatement extends BaseNode where
     body : Array TS_Statement
     directives : Array String := #[]
-    -- innerComments is an array of comments
   deriving Repr, Lean.FromJson, Lean.ToJson
 
   structure TS_IfStatement extends BaseNode where
@@ -225,11 +232,8 @@ mutual
     alternate : Option TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-  /-- A single `case` (or `default` when `test = none`) inside a switch. -/
   structure TS_SwitchCase extends BaseNode where
-    /-- `some expr` for `case expr:`, `none` for `default:` --/
     test : Option TS_Expression
-    /-- statements executed for this case (often end with a BreakStatement) --/
     consequent : Array TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
 
@@ -253,7 +257,6 @@ mutual
     label: Option TS_Identifier
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-  /- TODO: Add support for for(let a=0, b=0;a!=0 and b!=0;a++,b++) -/
   structure TS_ForStatement extends BaseNode where
     init: TS_VariableDeclaration
     test: TS_Expression
@@ -261,36 +264,41 @@ mutual
     body: TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-  /-- `break;` (labels optional; ESTree uses null when absent) -/
   structure TS_BreakStatement extends BaseNode where
     label : Option TS_Identifier := none
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-  /-- `switch (discriminant) { cases... }` -/
   structure TS_SwitchStatement extends BaseNode where
     discriminant : TS_Expression
     cases : Array TS_SwitchCase
   deriving Repr, Lean.FromJson, Lean.ToJson
 
-  inductive TS_Statement where
-    | TS_IfStatement : TS_IfStatement → TS_Statement
-    | TS_VariableDeclaration : TS_VariableDeclaration → TS_Statement
-    | TS_ExpressionStatement : TS_ExpressionStatement → TS_Statement
-    | TS_BlockStatement : TS_BlockStatement → TS_Statement
-    | TS_ThrowStatement : TS_ThrowStatement → TS_Statement
-    | TS_ReturnStatement : TS_ReturnStatement → TS_Statement
-    | TS_FunctionDeclaration : TS_FunctionDeclaration → TS_Statement
-    | TS_ForStatement : TS_ForStatement → TS_Statement
-    | TS_WhileStatement: TS_WhileStatement -> TS_Statement
-    | TS_BreakStatement : TS_BreakStatement → TS_Statement
-    | TS_SwitchStatement : TS_SwitchStatement → TS_Statement
-    | TS_ContinueStatement: TS_ContinueStatement -> TS_Statement
+  structure TS_ForInStatement extends BaseNode where
+    left: TS_VariableDeclaration
+    right: TS_Expression
+    body: TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
-end
 
-structure TS_Comment extends BaseNode where
-deriving Repr, Lean.FromJson, Lean.ToJson
+  structure TS_ForOfStatement extends BaseNode where
+    left: TS_VariableDeclaration
+    right: TS_Expression
+    body: TS_Statement
+  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_Program extends BaseNode where
   sourceType : String
@@ -311,8 +319,6 @@ def test_json_to_x (x: Lean.Json) : IO Unit :=
   let e: Except String TS_Expression := Lean.FromJson.fromJson? x
   IO.println s!"{repr e}"
 
--- #eval test_json_to_x example_expression
-
 def loadJsonFile (path : System.FilePath) : IO TS_File := do
   let contents ← IO.FS.readFile path
   let json ← match Lean.Json.parse contents with
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/StrataTest/Languages/TypeScript/test_for_in.ts b/StrataTest/Languages/TypeScript/test_for_in.ts
new file mode 100644
index 000000000..4abc2b766
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_for_in.ts
@@ -0,0 +1,5 @@
+let obj = {0: 10, 1: 20, 2: 30};
+let sum = 0;
+for (let key in obj) {
+    sum = sum + obj[key];
+}
\ No newline at end of file
diff --git a/StrataTest/Languages/TypeScript/test_for_of.ts b/StrataTest/Languages/TypeScript/test_for_of.ts
new file mode 100644
index 000000000..742789823
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_for_of.ts
@@ -0,0 +1,5 @@
+let arr = [10, 20, 30];
+let sum = 0;
+for (let value of arr) {
+    sum = sum + value;
+}
\ No newline at end of file
diff --git a/conformance_testing/babel_to_lean.py b/conformance_testing/babel_to_lean.py
index eeae71e76..a04dbd190 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)
@@ -133,9 +133,6 @@ def parse_member_expression(j):
     add_missing_node_info(j, target_j)
     return target_j
 
-    add_missing_node_info(j, target_j)
-    return target_j
-
 def parse_array_expression(j):
     # Normalize Babel ArrayExpression: keep only non-null elements and parse each
     elems = []
@@ -319,6 +316,78 @@ def parse_for_statement(j):
     add_missing_node_info(j, target_j)
     return target_j
 
+def parse_for_in_statement(j):
+    target_body = parse_statement(j['body'])
+
+    left_decl = j['left']
+
+    # For-in declarators don't have init, so provide a null literal
+    declarators = []
+    for d in left_decl.get('declarations', []):
+        decl_dict = {
+            "id": parse_identifier(d['id']),
+            "init": {"TS_NullLiteral": {
+                "type": "NullLiteral",
+                "start": d.get('start', 0),
+                "end": d.get('end', 0),
+                "loc": d.get('loc', {})
+            }}  # Provide dummy null expression
+        }
+        add_missing_node_info(d, decl_dict)
+        declarators.append(decl_dict)
+
+    target_left = {
+        "type": "VariableDeclaration",
+        "declarations": declarators,
+        "kind": left_decl.get('kind')
+    }
+    add_missing_node_info(left_decl, target_left)
+
+    target_j = {
+        "left": target_left,
+        "right": parse_expression(j['right']),
+        "body": target_body
+    }
+    add_missing_node_info(j, target_j)
+
+    return target_j
+
+def parse_for_of_statement(j):
+    target_body = parse_statement(j['body'])
+
+    # Parse left as bare TS_VariableDeclaration structure
+    left_decl = j['left']
+
+    declarators = []
+    for d in left_decl.get('declarations', []):
+        decl_dict = {
+            "id": parse_identifier(d['id']),
+            "init": {"TS_NullLiteral": {
+                "type": "NullLiteral",
+                "start": d.get('start', 0),
+                "end": d.get('end', 0),
+                "loc": d.get('loc', {})
+            }}
+        }
+        add_missing_node_info(d, decl_dict)
+        declarators.append(decl_dict)
+
+    target_left = {
+        "type": "VariableDeclaration",
+        "declarations": declarators,
+        "kind": left_decl.get('kind')
+    }
+    add_missing_node_info(left_decl, target_left)
+
+    target_j = {
+        "left": target_left,
+        "right": parse_expression(j['right']),
+        "body": target_body
+    }
+    add_missing_node_info(j, target_j)
+
+    return target_j
+
 def parse_switch_statement(j):
     target_j = {
         "discriminant": parse_expression(j['discriminant']),
@@ -379,8 +448,10 @@ def parse_statement(j):
         # case "DoWhileStatement":
         case "ForStatement":
             return {"TS_ForStatement": parse_for_statement(j)}
-        # case "ForInStatement":
-        # case "ForOfStatement":
+        case "ForInStatement":
+            return {"TS_ForInStatement": parse_for_in_statement(j)}
+        case "ForOfStatement":
+            return {"TS_ForOfStatement": parse_for_of_statement(j)}
         # case "ClassDeclaration":
         case _:
             print("Unsupported statement type: " + j['type'], file=sys.stderr)