diff --git a/Strata/DL/Heap/HEval.lean b/Strata/DL/Heap/HEval.lean
index 7901e602..6745c9eb 100644
--- a/Strata/DL/Heap/HEval.lean
+++ b/Strata/DL/Heap/HEval.lean
@@ -149,6 +149,15 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE
     -- Third application to DynamicFieldAssign - now we can evaluate
     -- This handles obj[field] = value where field is dynamic
     evalDynamicFieldAssign state2 objExpr fieldExpr e2'
+  | .deferredOp "DynamicFieldAssignReturnObj" _ =>
+    -- First application to DynamicFieldAssignReturnObj - return partially applied
+    (state2, .app (.deferredOp "DynamicFieldAssignReturnObj" none) e2')
+  | .app (.deferredOp "DynamicFieldAssignReturnObj" _) objExpr =>
+    -- Second application to DynamicFieldAssignReturnObj - return partially applied
+    (state2, .app (.app (.deferredOp "DynamicFieldAssignReturnObj" none) objExpr) e2')
+  | .app (.app (.deferredOp "DynamicFieldAssignReturnObj" _) objExpr) fieldExpr =>
+    -- Third application to DynamicFieldAssignReturnObj - now we can evaluate
+    evalDynamicFieldAssignReturnObj state2 objExpr fieldExpr e2'
   | .deferredOp "StringFieldAccess" _ =>
     -- First application to StringFieldAccess - return partially applied
     (state2, .app (.deferredOp "StringFieldAccess" none) e2')
@@ -170,6 +179,31 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE
     -- This handles delete obj[field] where field is dynamic
     evalFieldDelete state2 objExpr e2'
 
+  | .deferredOp "TypeOf" _ =>
+    -- Unary typeof operator
+    let result : HExpr :=
+      match e2' with
+      | .address _ =>
+        HExpr.string "object"
+      | .null =>
+        HExpr.string "object"
+      | .lambda (LExpr.const _ (some Lambda.LMonoTy.int)) =>
+        HExpr.string "number"
+      | .lambda (LExpr.const _ (some Lambda.LMonoTy.bool)) =>
+        HExpr.string "boolean"
+      | .lambda (LExpr.const _ (some Lambda.LMonoTy.string)) =>
+        HExpr.string "string"
+      | .lambda (LExpr.const _ _) =>
+        HExpr.string "undefined"
+      | _ =>
+        HExpr.string "undefined"
+    (state2, result)
+
+  | .deferredOp "InstanceOf" _ =>
+    (state2, .app (.deferredOp "InstanceOf" none) e2')
+  | .app (.deferredOp "InstanceOf" _) lhsExpr =>
+    evalInstanceOf state2 lhsExpr e2'
+
   | .deferredOp op _ =>
     -- First application to a deferred operation - return partially applied
     (state2, .app (.deferredOp op none) e2')
@@ -193,25 +227,69 @@ partial def evalApp (state : HState) (originalExpr e1 e2 : HExpr) : HState × HE
 
 -- Handle dynamic field access: obj[field] where field is dynamic
 partial def evalDynamicFieldAccess (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, use regular deref
-    evalHExpr state (.deref objExpr fieldIndex)
-  | none =>
-    -- Can't extract a numeric field index, return error
-    (state, .lambda (LExpr.const "error_dynamic_field_access_failed" none))
+  let (s1, objVal) := evalHExpr state objExpr
+  let (s2, keyVal) := evalHExpr s1 fieldExpr
+  match objVal with
+  | .address addr =>
+    match keyVal with
+    | .lambda (LExpr.const k _) =>
+      match k.toNat? with
+      | some n =>
+        match s2.getField addr n with
+        | some v => (s2, v)
+        | none   => (s2, .lambda (LExpr.const s!"error_field_{n}_not_found" none))
+      | none =>
+        match s2.getStringField addr k with
+        | some v => (s2, v)
+        | none   => (s2, .lambda (LExpr.const s!"error_string_field_{k}_not_found" none))
+    | _ => (s2, .lambda (LExpr.const "error_invalid_field_key" none))
+  | .null => (s2, .lambda (LExpr.const "error_null_dereference" none))
+  | _     => (s2, .lambda (LExpr.const "error_invalid_address" none))
 
 -- Handle dynamic field assignment: obj[field] = value where field is dynamic
 partial def evalDynamicFieldAssign (state : HState) (objExpr fieldExpr valueExpr : 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, use regular assign
-    evalHExpr state (.assign objExpr fieldIndex valueExpr)
-  | none =>
-    -- Can't extract a numeric field index, return error
-    (state, .lambda (LExpr.const "error_dynamic_field_assign_failed" none))
+  let (s1, objVal) := evalHExpr state objExpr
+  let (s2, keyVal) := evalHExpr s1 fieldExpr
+  let (s3, valVal) := evalHExpr s2 valueExpr
+  match objVal with
+  | .address addr =>
+    match keyVal with
+    | .lambda (LExpr.const k _) =>
+      match k.toNat? with
+      | some n =>
+        match s3.setField addr n valVal with
+        | some s' => (s', valVal)
+        | none    => (s3, .lambda (LExpr.const s!"error_cannot_update_field_{n}" none))
+      | none =>
+        match s3.setStringField addr k valVal with
+        | some s' => (s', valVal)
+        | none    => (s3, .lambda (LExpr.const s!"error_cannot_update_string_field_{k}" none))
+    | _ => (s3, .lambda (LExpr.const "error_invalid_field_key" none))
+  | .null => (s3, .lambda (LExpr.const "error_null_assignment" none))
+  | _     => (s3, .lambda (LExpr.const "error_invalid_address_assignment" none))
+
+-- Handle dynamic field assignment but return the *object address* to allow chaining
+partial def evalDynamicFieldAssignReturnObj (state : HState) (objExpr fieldExpr valueExpr : HExpr) : HState × HExpr :=
+  let (s1, objVal) := evalHExpr state objExpr
+  let (s2, keyVal) := evalHExpr s1 fieldExpr
+  let (s3, valVal) := evalHExpr s2 valueExpr
+  match objVal with
+  | .address addr =>
+    match keyVal with
+    | .lambda (LExpr.const k _) =>
+      match k.toNat? with
+      | some n =>
+        match s3.setField addr n valVal with
+        | some s' => (s', .address addr)
+        | none    => (s3, .lambda (LExpr.const s!"error_cannot_update_field_{n}" none))
+      | none =>
+        match s3.setStringField addr k valVal with
+        | some s' => (s', .address addr)
+        | none    => (s3, .lambda (LExpr.const s!"error_cannot_update_string_field_{k}" none))
+    | _ => (s3, .lambda (LExpr.const "error_invalid_field_key" none))
+  | .null => (s3, .lambda (LExpr.const "error_null_assignment" none))
+  | _     => (s3, .lambda (LExpr.const "error_invalid_address_assignment" none))
+
 
 -- Handle string field access: str.fieldName where fieldName is a string literal
 partial def evalStringFieldAccess (state : HState) (objExpr fieldExpr : HExpr) : HState × HExpr :=
@@ -288,7 +366,6 @@ partial def evalLengthAccess (state : HState) (objExpr fieldExpr : HExpr) : HSta
 partial def extractFieldIndex (expr : HExpr) : Option Nat :=
   match expr with
   | .lambda (LExpr.const s _) =>
-    -- Try to parse the string as a natural number
     s.toNat?
   | _ => none
 
@@ -305,6 +382,18 @@ partial def evalBinaryOp (state : HState) (op : String) (arg1 arg2 : HExpr) : HS
     -- Partial evaluation - keep as deferred operation
     (state, .app (.app (.deferredOp op none) arg1) arg2)
 
+partial def evalInstanceOf (state : HState) (lhs rhs : HExpr) : HState × HExpr :=
+  let (s1, v)   := evalHExpr state lhs
+  let (s2, _) := evalHExpr s1 rhs
+
+  let result : HExpr :=
+    match v with
+    | .address _ => Heap.HExpr.true
+    | .null      => Heap.HExpr.false
+    | _          => Heap.HExpr.false
+
+  (s2, result)
+
 end
 
 -- Convenience function for evaluation
@@ -318,6 +407,25 @@ namespace HExpr
 def allocSimple (fields : List (Nat × HExpr)) : HExpr :=
   .alloc (HMonoTy.mkObj fields.length HMonoTy.int) fields
 
+def dynamicAssign (obj : HExpr) (key : HExpr) (val : HExpr) : HExpr :=
+  HExpr.app
+    (HExpr.app
+      (HExpr.app (HExpr.deferredOp "DynamicFieldAssign" none) obj)
+      key)
+    val
+
+/-- Like `dynamicAssign`, but evaluates to the *object* so it can be chained. --/
+def dynamicAssignReturnObj (obj : HExpr) (key : HExpr) (val : HExpr) : HExpr :=
+  HExpr.app
+    (HExpr.app
+      (HExpr.app (HExpr.deferredOp "DynamicFieldAssignReturnObj" none) obj)
+      key)
+    val
+
+def dynamicAlloc (numFields : List (Nat × HExpr)) (dynFields : List (HExpr × HExpr)) : HExpr :=
+  let obj0 := allocSimple numFields
+  dynFields.foldl (fun acc (k, v) => dynamicAssignReturnObj acc k v) obj0
+
 end HExpr
 
 end Heap
diff --git a/Strata/DL/Heap/HState.lean b/Strata/DL/Heap/HState.lean
index 9bd07ebf..867c1b75 100644
--- a/Strata/DL/Heap/HState.lean
+++ b/Strata/DL/Heap/HState.lean
@@ -34,6 +34,10 @@ abbrev HeapMemory := Std.HashMap Address HeapObject
 -- Heap variable environment - maps variable names to (type, value) pairs
 abbrev HeapVarEnv := Std.HashMap String (HMonoTy × HExpr)
 
+-- String-keyed fields for objects
+abbrev StringFieldMap := Std.HashMap String HExpr
+abbrev StringFields := Std.HashMap Nat StringFieldMap
+
 /--
 Heap State extending Lambda state with heap memory and heap variable environment.
 -/
@@ -46,9 +50,11 @@ structure HState where
   nextAddr : Address
   -- Heap variable environment (parallel to Lambda's variable environment)
   heapVars : HeapVarEnv
+  -- String-keyed fields: address -> (key -> value)
+  stringFields : StringFields
 
 instance : Repr HState where
-  reprPrec s _ := s!"HState(nextAddr: {s.nextAddr}, heap: <{s.heap.size} objects>, heapVars: <{s.heapVars.size} vars>)"
+  reprPrec s _ := s!"HState(nextAddr: {s.nextAddr}, heap: <{s.heap.size} objects>, heapVars: <{s.heapVars.size} vars>, stringFields: <{s.stringFields.size} props>)"
 
 namespace HState
 
@@ -81,9 +87,10 @@ def empty : HState :=
     | .ok state => state
     | .error _ => lambdaState  -- Fallback to basic state if factory addition fails
   { lambdaState := lambdaStateWithFactory,
-    heap := Std.HashMap.empty,
+    heap := Std.HashMap.emptyWithCapacity,
     nextAddr := 1,  -- Start addresses from 1 (0 can represent null)
-    heapVars := Std.HashMap.empty }
+    heapVars := Std.HashMap.emptyWithCapacity,
+    stringFields := Std.HashMap.emptyWithCapacity }
 
 -- Heap Variable Environment Operations
 
@@ -173,6 +180,19 @@ def deleteField (state : HState) (addr : Address) (field : Nat) : Option HState
     some { state with heap := newHeap }
   | none => none
 
+-- String field operations (for objects with string-keyed fields)
+def getStringField (s : HState) (addr : Nat) (key : String) : Option HExpr :=
+  match s.stringFields.get? addr with
+  | some m => m.get? key
+  | none => none
+
+-- Set a string field in an object
+def setStringField (s : HState) (addr : Nat) (key : String) (val : HExpr) : Option HState :=
+  let existing : StringFieldMap := (s.stringFields.get? addr).getD (Std.HashMap.emptyWithCapacity)
+  let updated := existing.insert key val
+  some { s with stringFields := s.stringFields.insert addr updated }
+
+
 -- Check if an address is valid (exists in heap)
 def isValidAddr (state : HState) (addr : Address) : Bool :=
   state.heap.contains addr
@@ -198,6 +218,29 @@ def heapVarsToString (state : HState) : String :=
 def toString (state : HState) : String :=
   s!"{state.heapToString}\n{state.heapVarsToString}"
 
+-- Return all string-keyed fields for an address as an association list
+def getAllStringFields (s : HState) (addr : Nat) : List (String × HExpr) :=
+  match s.stringFields.get? addr with
+  | some m => m.toList
+  | none => []
+
+-- Return all fields (numeric and string) as string-keyed pairs
+def getAllFieldsAsStringPairs (s : HState) (addr : Nat) : List (String × HExpr) :=
+  let numeric : List (String × HExpr) :=
+    match s.getObject addr with
+    | some obj => obj.toList.map (fun (i, v) => (s!"{i}", v))
+    | none => []
+  let strk   : List (String × HExpr) := s.getAllStringFields addr
+  -- string keys should override numeric if the same string exists
+  let merged := Id.run do
+    let mut map : Std.HashMap String HExpr := Std.HashMap.emptyWithCapacity
+    for (k, v) in numeric do
+      map := map.insert k v
+    for (k, v) in strk do
+      map := map.insert k v
+    pure map
+  merged.toList
+
 end HState
 
 end Heap
diff --git a/Strata/DL/Heap/HeapStrataEval.lean b/Strata/DL/Heap/HeapStrataEval.lean
index ba2642ea..117ec131 100644
--- a/Strata/DL/Heap/HeapStrataEval.lean
+++ b/Strata/DL/Heap/HeapStrataEval.lean
@@ -151,21 +151,16 @@ mutual
     | _ => none  -- Other expressions not supported yet
 
   partial def extractObjectAsJson (state : HState) (addr : Address) : Option Lean.Json :=
-    match state.getObject addr with
-    | some obj =>
-      -- Convert heap object (field index -> HExpr) to JSON object
-      let fields := obj.toList
-      let jsonFields := fields.filterMap fun (fieldIndex, fieldExpr) =>
-        match extractConcreteValueWithState state fieldExpr with
-        | some fieldJson =>
-          -- Use field index as string key for now
-          some (toString fieldIndex, fieldJson)
-        | none => none
-
-      -- Sort fields by key for consistency
-      let sortedFields := jsonFields.toArray.qsort (fun a b => a.1 < b.1) |>.toList
-      some (Lean.Json.mkObj sortedFields)
-    | none => none
+    -- Merge numeric fields and string-keyed fields from the heap
+    let pairs : List (String × HExpr) := state.getAllFieldsAsStringPairs addr
+    -- Encode each field value recursively
+    let jsonFields : List (String × Lean.Json) := pairs.filterMap fun (k, v) =>
+      match extractConcreteValueWithState state v with
+      | some j => some (k, j)
+      | none   => none
+    -- Sort for stable output
+    let sortedFields := jsonFields.toArray.qsort (fun a b => a.1 < b.1) |>.toList
+    some (Lean.Json.mkObj sortedFields)
 
   -- Legacy function for backward compatibility
   partial def extractConcreteValue (expr : HExpr) : Option String :=
diff --git a/Strata/Languages/TypeScript/TS_to_Strata.lean b/Strata/Languages/TypeScript/TS_to_Strata.lean
index e87de49c..5d94e23c 100644
--- a/Strata/Languages/TypeScript/TS_to_Strata.lean
+++ b/Strata/Languages/TypeScript/TS_to_Strata.lean
@@ -75,6 +75,7 @@ def Option_TS_TSTypeKeyword_to_str (i: Option TS_TSTypeKeyword) : String :=
     | .TS_TSBooleanKeyword _ => "TS_TSBooleanKeyword"
     | .TS_TSStringKeyword _ => "TS_TSStringKeyword"
     | .TS_TSArrayType _ => "TS_TSArrayType"
+    | .TS_TSTypeLiteral _ => "TS_TSTypeLiteral"
   | .none => panic! "Unimplemented"
 
 -- Helper to extract type from optional type annotation
@@ -93,10 +94,14 @@ partial def infer_type_from_expr (expr: TS_Expression) : Heap.HMonoTy :=
   | .TS_BinaryExpression e =>
     match e.operator with
     | "+" | "-" | "*" | "/" | "%" => Heap.HMonoTy.int
-    | "==" | "<=" | "<" | ">=" | ">" => Heap.HMonoTy.bool
+    | "==" | "<=" | "<" | ">=" | ">" | "instanceof" => Heap.HMonoTy.bool
     | _ => Heap.HMonoTy.int  -- Default
   | .TS_LogicalExpression _ => Heap.HMonoTy.bool
   | .TS_ConditionalExpression e => infer_type_from_expr e.consequent  -- Use consequent type
+  | .TS_UnaryExpression e =>
+    match e.operator with
+    | "typeof" => Heap.HMonoTy.string
+    | _ => Heap.HMonoTy.int  -- Default
   | _ => Heap.HMonoTy.int  -- Default fallback
 
 -- Get type for variable declaration, preferring annotation over inference
@@ -125,6 +130,7 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
     | "<" => Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) lhs) rhs
     | ">=" => Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Ge" none) lhs) rhs
     | ">" => Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Gt" none) lhs) rhs
+    | "instanceof" => Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "InstanceOf" none) lhs) rhs
     | _ => panic! s!"Unsupported binary operator: {e.operator}"
 
   | .TS_LogicalExpression e =>
@@ -142,6 +148,14 @@ 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 =>
+    let arg := translate_expr e.argument
+    match e.operator with
+    | "typeof" =>
+      Heap.HExpr.app (Heap.HExpr.deferredOp "TypeOf" 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!
@@ -191,15 +205,28 @@ partial def translate_expr (e: TS_Expression) : Heap.HExpr :=
       Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) fieldExpr
 
   | .TS_ObjectExpression e =>
-    -- Translate {1: value1, 5: value5} to heap allocation
-    let fields := e.properties.toList.map (fun prop =>
-      let key := match prop.key with
-        | .TS_NumericLiteral numLit => Float.floor numLit.value |>.toUInt64.toNat
-        | _ => panic! s!"Expected numeric literal as object key, got: {repr prop.key}"
-      let value := translate_expr prop.value
-      (key, value))
-    -- Use allocSimple which handles the object type automatically
-    Heap.HExpr.allocSimple fields
+    -- Collect numeric props for allocSimple, and *one* list of dynamic (keyExpr,valueExpr)
+    let (numProps, dynProps) :=
+      e.properties.toList.foldl
+        (fun (ns, ds) prop =>
+          let v := translate_expr prop.value
+          match prop.key with
+          | .TS_NumericLiteral numLit =>
+              let idx := Float.floor numLit.value |>.toUInt64.toNat
+              ((idx, v) :: ns, ds)
+          | .TS_StringLiteral strLit =>
+              -- string-literal key becomes a constant string expression
+              (ns, (Heap.HExpr.string strLit.value, v) :: ds)
+          | .TS_IdExpression id =>
+              -- non-computed identifier key like { name: ... } becomes field "name"
+              (ns, (Heap.HExpr.string id.name, v) :: ds)
+          | other =>
+              -- computed key: use the translated expression as dynamic key
+              (ns, (translate_expr other, v) :: ds))
+        ([], [])
+
+    let obj := Heap.HExpr.dynamicAlloc (numProps.reverse) (dynProps.reverse)
+    obj
 
   | .TS_CallExpression call =>
     match call.callee with
@@ -250,10 +277,10 @@ partial def translate_statement_core
   (ct: ControlTargets := {}) : TranslationContext × List TSStrataStatement :=
     match s with
       | .TS_FunctionDeclaration funcDecl =>
-      -- Translate function definition
-      dbg_trace s!"[DEBUG] Translating TypeScript function definition: {funcDecl.id.name}"
-      dbg_trace s!"[DEBUG] Function parameters: {funcDecl.params.toList.map (·.name)}"
-      dbg_trace s!"[DEBUG] Function body has statements"
+        -- Translate function definition
+        dbg_trace s!"[DEBUG] Translating TypeScript function definition: {funcDecl.id.name}"
+        dbg_trace s!"[DEBUG] Function parameters: {funcDecl.params.toList.map (·.name)}"
+        dbg_trace s!"[DEBUG] Function body has statements"
 
       let (bodyCtx, funcBody) := match funcDecl.body with
           | .TS_BlockStatement blockStmt =>
@@ -314,7 +341,7 @@ partial def translate_statement_core
               match member.property with
               | .TS_IdExpression methodId =>
                 if methodId.name == "pop" then
-                -- Handle Array.pop() method
+                  -- 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)
@@ -326,6 +353,157 @@ partial def translate_statement_core
                   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 == "map" then
+                  -- Handle Array.map()
+                  let objExpr := translate_expr member.object
+                  let (cbName, ctxAfterCb) :=
+                    match call.arguments[0]? with
+                    | some (.TS_FunctionExpression fexpr) =>
+                      let funcName := s!"__anon_map_func_{fexpr.start_loc}_{fexpr.end_loc}"
+                      let funcBody := match fexpr.body with
+                        | .TS_BlockStatement blockStmt =>
+                          (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten
+                        | _ => panic! s!"Expected block statement as function body, got: {repr fexpr.body}"
+                      let strataFunc : CallHeapStrataFunction := {
+                        name := funcName,
+                        params := fexpr.params.toList.map (·.name),
+                        body := funcBody,
+                        returnType := none
+                      }
+                      let newCtx := ctx.addFunction strataFunc
+                      (funcName, newCtx)
+                    | some (.TS_ArrowFunctionExpression aexpr) =>
+                      let funcName := s!"__anon_map_arrow_{aexpr.start_loc}_{aexpr.end_loc}"
+                      let funcBody := match aexpr.body with
+                        | .TS_BlockStatement blockStmt =>
+                          (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten
+                        | _ => panic! s!"Expected block statement as function body, got: {repr aexpr.body}"
+                      let strataFunc : CallHeapStrataFunction := {
+                        name := funcName,
+                        params := aexpr.params.toList.map (·.name),
+                        body := funcBody,
+                        returnType := none
+                      }
+                      let newCtx := ctx.addFunction strataFunc
+                      (funcName, newCtx)
+                    | some (.TS_IdExpression fid) =>
+                      (fid.name, ctx)
+                    | _ => panic! "map(callback) expects a function or identifier as the first argument"
+
+                  -- Initialize destination array variable (bind to declared identifier)
+                  let dstVar := d.id.name
+                  let initDst : TSStrataStatement := .cmd (.init dstVar Heap.HMonoTy.addr (Heap.HExpr.allocSimple []))
+
+                  -- idx/len
+                  let idxVar := s!"temp_map_idx_{member.start_loc}"
+                  let lenVar := s!"temp_map_len_{member.start_loc}"
+                  let initIdx : TSStrataStatement := .cmd (.init idxVar Heap.HMonoTy.int (Heap.HExpr.int 0))
+                  let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+                  let initLen : TSStrataStatement := .cmd (.init lenVar Heap.HMonoTy.int lengthExpr)
+
+                  -- guard idx < len
+                  let idxRef := Heap.HExpr.lambda (.fvar idxVar none)
+                  let lenRef := Heap.HExpr.lambda (.fvar lenVar none)
+                  let guard := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) idxRef) lenRef
+
+                  -- value = obj[idx]; ret = cb(value, idx, obj); dst[idx] = ret; idx++
+                  let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) idxRef
+                  let retVar := s!"temp_map_ret_{member.start_loc}"
+                  let callCb : TSStrataStatement := .cmd (.directCall [retVar] cbName [valueExpr, idxRef, objExpr])
+
+                  let dstRef := Heap.HExpr.lambda (.fvar dstVar none)
+                  let assignExpr :=
+                    Heap.HExpr.app
+                      (Heap.HExpr.app
+                        (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) dstRef)
+                        idxRef)
+                      (Heap.HExpr.lambda (.fvar retVar none))
+                  let writeStmt : TSStrataStatement := .cmd (.set "temp_map_assign_result" assignExpr)
+
+                  let nextIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) idxRef) (Heap.HExpr.int 1)
+                  let incIdx : TSStrataStatement := .cmd (.set idxVar nextIdx)
+
+                  let loopBody : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [callCb, writeStmt, incIdx] }
+
+                  (ctxAfterCb, [initDst, initIdx, initLen, .loop guard none none loopBody])
+                else if methodId.name == "filter" then
+                  -- Handle Array.filter()
+                  let objExpr := translate_expr member.object
+                  let (cbName, ctxAfterCb) :=
+                    match call.arguments[0]? with
+                    | some (.TS_FunctionExpression fexpr) =>
+                      let funcName := s!"__anon_filter_func_{fexpr.start_loc}_{fexpr.end_loc}"
+                      let funcBody := match fexpr.body with
+                        | .TS_BlockStatement blockStmt =>
+                          (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten
+                        | _ => panic! s!"Expected block statement as function body, got: {repr fexpr.body}"
+                      let strataFunc : CallHeapStrataFunction := {
+                        name := funcName,
+                        params := fexpr.params.toList.map (·.name),
+                        body := funcBody,
+                        returnType := none
+                      }
+                      let newCtx := ctx.addFunction strataFunc
+                      (funcName, newCtx)
+                    | some (.TS_ArrowFunctionExpression aexpr) =>
+                      let funcName := s!"__anon_filter_arrow_{aexpr.start_loc}_{aexpr.end_loc}"
+                      let funcBody := match aexpr.body with
+                        | .TS_BlockStatement blockStmt =>
+                          (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten
+                        | _ => panic! s!"Expected block statement as function body, got: {repr aexpr.body}"
+                      let strataFunc : CallHeapStrataFunction := {
+                        name := funcName,
+                        params := aexpr.params.toList.map (·.name),
+                        body := funcBody,
+                        returnType := none
+                      }
+                      let newCtx := ctx.addFunction strataFunc
+                      (funcName, newCtx)
+                    | some (.TS_IdExpression fid) =>
+                      (fid.name, ctx)
+                    | _ => panic! "filter(callback) expects a function or identifier as the first argument"
+
+                  -- Initialize destination array variable (bind to declared identifier)
+                  let dstVar := d.id.name
+                  let initDst : TSStrataStatement := .cmd (.init dstVar Heap.HMonoTy.addr (Heap.HExpr.allocSimple []))
+
+                  -- idx/len
+                  let idxVar := s!"temp_filter_idx_{member.start_loc}"
+                  let lenVar := s!"temp_filter_len_{member.start_loc}"
+                  let outIdxVar := s!"temp_filter_outidx_{member.start_loc}"
+                  let initIdx : TSStrataStatement := .cmd (.init idxVar Heap.HMonoTy.int (Heap.HExpr.int 0))
+                  let initOutIdx : TSStrataStatement := .cmd (.init outIdxVar Heap.HMonoTy.int (Heap.HExpr.int 0))
+                  let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+                  let initLen : TSStrataStatement := .cmd (.init lenVar Heap.HMonoTy.int lengthExpr)
+
+                  -- guard idx < len
+                  let idxRef := Heap.HExpr.lambda (.fvar idxVar none)
+                  let lenRef := Heap.HExpr.lambda (.fvar lenVar none)
+                  let outIdxRef := Heap.HExpr.lambda (.fvar outIdxVar none)
+                  let guard := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) idxRef) lenRef
+
+                  -- value = obj[idx]; cond = cb(value, idx, obj); if cond then dst[outIdx] = value; outIdx++; idx++
+                  let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) idxRef
+                  let condVar := s!"temp_filter_cond_{member.start_loc}"
+                  let callCb : TSStrataStatement := .cmd (.directCall [condVar] cbName [valueExpr, idxRef, objExpr])
+                  let dstRef := Heap.HExpr.lambda (.fvar dstVar none)
+                  let assignExpr :=
+                    Heap.HExpr.app
+                      (Heap.HExpr.app
+                        (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) dstRef)
+                        outIdxRef)
+                      valueExpr
+                  let writeStmt : TSStrataStatement := .cmd (.set "temp_filter_assign_result" assignExpr)
+                  let incOutIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) outIdxRef) (Heap.HExpr.int 1)
+                  let incOutIdxStmt : TSStrataStatement := .cmd (.set outIdxVar incOutIdx)
+                  let condRef := Heap.HExpr.lambda (.fvar condVar none)
+                  let thenBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [writeStmt, incOutIdxStmt] }
+                  let elseBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [] }
+                  let iteStmt : TSStrataStatement := .ite condRef thenBlk elseBlk
+                  let nextIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) idxRef) (Heap.HExpr.int 1)
+                  let incIdx : TSStrataStatement := .cmd (.set idxVar nextIdx)
+                  let loopBody : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [callCb, iteStmt, incIdx] }
+                  (ctxAfterCb, [initDst, initIdx, initOutIdx, initLen, .loop guard none none loopBody])
                 else
                   defaultInit
               | _ => defaultInit
@@ -389,10 +567,10 @@ partial def translate_statement_core
                 | "push" =>
                   match call.arguments[0]? with
                   | some a =>
-                    let valueExpr := translate_expr a
-                    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)])
+                      let valueExpr := translate_expr a
+                      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)])
                   | none => panic! "push() expects 1 argument"
                 | "pop" =>
                   -- arr.pop() standalone - read and delete
@@ -403,8 +581,8 @@ partial def translate_statement_core
                   -- 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.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) objExpr) tempIndexVar) Heap.HExpr.null
+                  -- Delete the element (use FieldDelete so the index is removed instead of set to null)
+                  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])
                 | "forEach" =>
@@ -460,6 +638,155 @@ partial def translate_statement_core
                   let loopBody : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [callCb, incIdx] }
 
                   (ctxAfterCb, [initIdx, initLen, .loop guard none none loopBody])
+                | "map" =>
+                  -- arr.map(callback)
+                  dbg_trace s!"[DEBUG] Translating arr.map(callback) method call"
+                  let (cbName, ctxAfterCb) :=
+                    match call.arguments[0]? with
+                    | some (.TS_FunctionExpression fexpr) =>
+                      let funcName := s!"__anon_map_func_{fexpr.start_loc}_{fexpr.end_loc}"
+                      let funcBody := match fexpr.body with
+                        | .TS_BlockStatement blockStmt =>
+                          (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten
+                        | _ => panic! s!"Expected block statement as function body, got: {repr fexpr.body}"
+                      let strataFunc : CallHeapStrataFunction := {
+                        name := funcName,
+                        params := fexpr.params.toList.map (·.name),
+                        body := funcBody,
+                        returnType := none
+                      }
+                      let newCtx := ctx.addFunction strataFunc
+                      (funcName, newCtx)
+                    | some (.TS_ArrowFunctionExpression aexpr) =>
+                      let funcName := s!"__anon_map_arrow_{aexpr.start_loc}_{aexpr.end_loc}"
+                      let funcBody := match aexpr.body with
+                        | .TS_BlockStatement blockStmt =>
+                          (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten
+                        | _ => panic! s!"Expected block statement as function body, got: {repr aexpr.body}"
+                      let strataFunc : CallHeapStrataFunction := {
+                        name := funcName,
+                        params := aexpr.params.toList.map (·.name),
+                        body := funcBody,
+                        returnType := none
+                      }
+                      let newCtx := ctx.addFunction strataFunc
+                      (funcName, newCtx)
+                    | some (.TS_IdExpression fid) =>
+                      (fid.name, ctx)
+                    | _ => panic! "map(callback) expects a function or identifier as the first argument"
+
+                  -- Prepare destination array to hold mapped values
+                  let dstVar := s!"temp_map_arr_{member.start_loc}"
+                  let initDst : TSStrataStatement :=
+                    .cmd (.init dstVar Heap.HMonoTy.addr (Heap.HExpr.allocSimple []))
+                  -- idx/len like forEach
+                  let idxVar := s!"temp_map_idx_{member.start_loc}"
+                  let lenVar := s!"temp_map_len_{member.start_loc}"
+                  let initIdx : TSStrataStatement := .cmd (.init idxVar Heap.HMonoTy.int (Heap.HExpr.int 0))
+                  let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+                  let initLen : TSStrataStatement := .cmd (.init lenVar Heap.HMonoTy.int lengthExpr)
+                  -- Build guard: idx < len
+                  let idxRef := Heap.HExpr.lambda (.fvar idxVar none)
+                  let lenRef := Heap.HExpr.lambda (.fvar lenVar none)
+                  let guard := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) idxRef) lenRef
+                  -- Loop body: value = obj[idx] ,ret = cb(value, idx, obj), dst[idx] = ret, idx = idx + 1
+                  let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) idxRef
+                  let retVar := s!"temp_map_ret_{member.start_loc}"
+                  let callCb : TSStrataStatement := .cmd (.directCall [retVar] cbName [valueExpr, idxRef, objExpr])
+
+                  let dstRef := Heap.HExpr.lambda (.fvar dstVar none)
+                  let assignExpr :=
+                    Heap.HExpr.app
+                      (Heap.HExpr.app
+                        (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) dstRef)
+                        idxRef)
+                      (Heap.HExpr.lambda (.fvar retVar none))
+                  let writeStmt : TSStrataStatement := .cmd (.set "temp_map_assign_result" assignExpr)
+
+                  let nextIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) idxRef) (Heap.HExpr.int 1)
+                  let incIdx : TSStrataStatement := .cmd (.set idxVar nextIdx)
+
+                  let loopBody : Imperative.Block TSStrataExpression TSStrataCommand :=
+                    { ss := [callCb, writeStmt, incIdx] }
+
+                  (ctxAfterCb, [initDst, initIdx, initLen, .loop guard none none loopBody])
+                | "filter" =>
+                  -- arr.filter(callback)
+                  dbg_trace s!"[DEBUG] Translating arr.filter(callback) method call"
+                  let (cbName, ctxAfterCb) :=
+                    match call.arguments[0]? with
+                    | some (.TS_FunctionExpression fexpr) =>
+                      let funcName := s!"__anon_filter_func_{fexpr.start_loc}_{fexpr.end_loc}"
+                      let funcBody := match fexpr.body with
+                        | .TS_BlockStatement blockStmt =>
+                          (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten
+                        | _ => panic! s!"Expected block statement as function body, got: {repr fexpr.body}"
+                      let strataFunc : CallHeapStrataFunction := {
+                        name := funcName,
+                        params := fexpr.params.toList.map (·.name),
+                        body := funcBody,
+                        returnType := none
+                      }
+                      let newCtx := ctx.addFunction strataFunc
+                      (funcName, newCtx)
+                    | some (.TS_ArrowFunctionExpression aexpr) =>
+                      let funcName := s!"__anon_filter_arrow_{aexpr.start_loc}_{aexpr.end_loc}"
+                      let funcBody := match aexpr.body with
+                        | .TS_BlockStatement blockStmt =>
+                          (blockStmt.body.toList.map (fun stmt => translate_statement_core stmt ctx ct |>.snd)).flatten
+                        | _ => panic! s!"Expected block statement as function body, got: {repr aexpr.body}"
+                      let strataFunc : CallHeapStrataFunction := {
+                        name := funcName,
+                        params := aexpr.params.toList.map (·.name),
+                        body := funcBody,
+                        returnType := none
+                      }
+                      let newCtx := ctx.addFunction strataFunc
+                      (funcName, newCtx)
+                    | some (.TS_IdExpression fid) =>
+                      (fid.name, ctx)
+                    | _ => panic! "filter(callback) expects a function or identifier as the first argument"
+
+                  -- Prepare destination array to hold filtered values
+                  let dstVar := s!"temp_filter_arr_{member.start_loc}"
+                  let initDst : TSStrataStatement :=
+                    .cmd (.init dstVar Heap.HMonoTy.addr (Heap.HExpr.allocSimple []))
+                  -- idx/len and output idx
+                  let idxVar := s!"temp_filter_idx_{member.start_loc}"
+                  let lenVar := s!"temp_filter_len_{member.start_loc}"
+                  let outIdxVar := s!"temp_filter_outidx_{member.start_loc}"
+                  let initIdx : TSStrataStatement := .cmd (.init idxVar Heap.HMonoTy.int (Heap.HExpr.int 0))
+                  let initOutIdx : TSStrataStatement := .cmd (.init outIdxVar Heap.HMonoTy.int (Heap.HExpr.int 0))
+                  let lengthExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "LengthAccess" none) objExpr) (Heap.HExpr.string "length")
+                  let initLen : TSStrataStatement := .cmd (.init lenVar Heap.HMonoTy.int lengthExpr)
+                  -- Build guard: idx < len
+                  let idxRef := Heap.HExpr.lambda (.fvar idxVar none)
+                  let lenRef := Heap.HExpr.lambda (.fvar lenVar none)
+                  let outIdxRef := Heap.HExpr.lambda (.fvar outIdxVar none)
+                  let guard := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Lt" none) idxRef) lenRef
+                  -- Loop body: value = obj[idx], cond = cb(value, idx, obj), if cond then dst[outIdx] = value; outIdx++; idx++
+                  let valueExpr := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAccess" none) objExpr) idxRef
+                  let condVar := s!"temp_filter_cond_{member.start_loc}"
+                  let callCb : TSStrataStatement := .cmd (.directCall [condVar] cbName [valueExpr, idxRef, objExpr])
+                  let dstRef := Heap.HExpr.lambda (.fvar dstVar none)
+                  let assignExpr :=
+                    Heap.HExpr.app
+                      (Heap.HExpr.app
+                        (Heap.HExpr.app (Heap.HExpr.deferredOp "DynamicFieldAssign" none) dstRef)
+                        outIdxRef)
+                      valueExpr
+                  let writeStmt : TSStrataStatement := .cmd (.set "temp_filter_assign_result" assignExpr)
+                  let incOutIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) outIdxRef) (Heap.HExpr.int 1)
+                  let incOutIdxStmt : TSStrataStatement := .cmd (.set outIdxVar incOutIdx)
+                  let condRef := Heap.HExpr.lambda (.fvar condVar none)
+                  let thenBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [writeStmt, incOutIdxStmt] }
+                  let elseBlk : Imperative.Block TSStrataExpression TSStrataCommand := { ss := [] }
+                  let iteStmt : TSStrataStatement := .ite condRef thenBlk elseBlk
+                  let nextIdx := Heap.HExpr.app (Heap.HExpr.app (Heap.HExpr.deferredOp "Int.Add" none) idxRef) (Heap.HExpr.int 1)
+                  let incIdx : TSStrataStatement := .cmd (.set idxVar nextIdx)
+                  let loopBody : Imperative.Block TSStrataExpression TSStrataCommand :=
+                    { ss := [callCb, iteStmt, incIdx] }
+                  (ctxAfterCb, [initDst, initIdx, initOutIdx, initLen, .loop guard none none loopBody])
                 | methodName =>
                   dbg_trace s!"[DEBUG] Translating method call: {methodName}(...)"
                   (ctx, [])
@@ -695,26 +1022,28 @@ 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) :=
+      | .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,
@@ -724,16 +1053,16 @@ partial def translate_statement_core
                 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
+        -- 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 }
+        -- 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])
+        -- 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 }
diff --git a/Strata/Languages/TypeScript/js_ast.lean b/Strata/Languages/TypeScript/js_ast.lean
index 1c4e6c4f..c3558d01 100644
--- a/Strata/Languages/TypeScript/js_ast.lean
+++ b/Strata/Languages/TypeScript/js_ast.lean
@@ -46,22 +46,31 @@ mutual
     | TS_TSBooleanKeyword : TS_TSBooleanKeyword → TS_TSTypeKeyword
     | TS_TSStringKeyword : TS_TSStringKeyword → TS_TSTypeKeyword
     | TS_TSArrayType : TS_TSArrayType → TS_TSTypeKeyword
+    | TS_TSTypeLiteral : TS_TSTypeLiteral → TS_TSTypeKeyword
   deriving Repr, Lean.FromJson, Lean.ToJson
 
   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
+  structure TS_TSPropertySignature extends BaseNode where
+    key : String
+    typeAnnotation : Option TS_TSTypeKeyword
+  deriving Repr, Lean.FromJson, Lean.ToJson
+
+  structure TS_TSTypeLiteral extends BaseNode where
+    members : Array TS_TSPropertySignature
+  deriving Repr, Lean.FromJson, Lean.ToJson
 end
 
 structure TS_TSTypeAnnotation extends BaseNode where
   typeAnnotation : Option TS_TSTypeKeyword
 deriving Repr, Lean.FromJson, Lean.ToJson
 
+structure TS_TSUnionType extends BaseNode where
+  types : Array TS_TSTypeKeyword
+deriving Repr, Lean.FromJson, Lean.ToJson
+
 structure TS_Identifier extends BaseNode where
   name : String
   typeAnnotation : Option TS_TSTypeAnnotation
@@ -271,6 +280,11 @@ mutual
     cases : Array TS_SwitchCase
   deriving Repr, Lean.FromJson, Lean.ToJson
 
+  structure TS_TypeAliasDeclaration extends BaseNode where
+    id : TS_Identifier
+    typeAnnotation : TS_TSUnionType
+  deriving Repr, Lean.FromJson, Lean.ToJson
+
   inductive TS_Statement where
     | TS_IfStatement : TS_IfStatement → TS_Statement
     | TS_VariableDeclaration : TS_VariableDeclaration → TS_Statement
@@ -284,6 +298,7 @@ mutual
     | TS_BreakStatement : TS_BreakStatement → TS_Statement
     | TS_SwitchStatement : TS_SwitchStatement → TS_Statement
     | TS_ContinueStatement: TS_ContinueStatement -> TS_Statement
+    | TS_TypeAliasDeclaration : TS_TypeAliasDeclaration → TS_Statement
   deriving Repr, Lean.FromJson, Lean.ToJson
 end
 
diff --git a/StrataTest/Languages/TypeScript/test_arrays_iterations.ts b/StrataTest/Languages/TypeScript/test_arrays_iterations.ts
index 7ff09fde..cd43c273 100644
--- a/StrataTest/Languages/TypeScript/test_arrays_iterations.ts
+++ b/StrataTest/Languages/TypeScript/test_arrays_iterations.ts
@@ -1,5 +1,14 @@
+// forEach
 let arr = [1, 2, 3, 4, 5];
 
 arr.forEach((value: number, index: number) => {
     arr[index] = value * 2;
 });
+
+// map
+let mappedArr = arr.map((value: number) => {return value + 1});
+
+// filter
+let filteredArr = arr.filter((value: number) => {
+    return value > 5;
+});
\ No newline at end of file
diff --git a/StrataTest/Languages/TypeScript/test_intersection_types.ts b/StrataTest/Languages/TypeScript/test_intersection_types.ts
new file mode 100644
index 00000000..901e984e
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_intersection_types.ts
@@ -0,0 +1,9 @@
+type A = { name: string };
+type B = { age: number };
+
+type Person = A & B;
+
+const p: Person = {
+    name: "Julia",
+    age: 23,
+};
\ No newline at end of file
diff --git a/StrataTest/Languages/TypeScript/test_obj_string_prop.ts b/StrataTest/Languages/TypeScript/test_obj_string_prop.ts
new file mode 100644
index 00000000..aa8163c1
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_obj_string_prop.ts
@@ -0,0 +1,6 @@
+// Test objects with string key-value
+let str_obj = {
+    "name": "Strata",
+    "type": "Testing",
+    "version": "1.0"
+}
\ No newline at end of file
diff --git a/StrataTest/Languages/TypeScript/test_type_alias.ts b/StrataTest/Languages/TypeScript/test_type_alias.ts
new file mode 100644
index 00000000..cd157d30
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_type_alias.ts
@@ -0,0 +1,5 @@
+type ID = string | number;
+
+// Variable declarations using the alias
+let userId: ID = 101;
+let orderId: ID = "ORD_2025";
\ No newline at end of file
diff --git a/StrataTest/Languages/TypeScript/test_type_guards.ts b/StrataTest/Languages/TypeScript/test_type_guards.ts
new file mode 100644
index 00000000..f9546065
--- /dev/null
+++ b/StrataTest/Languages/TypeScript/test_type_guards.ts
@@ -0,0 +1,7 @@
+// typeof
+let repoName = "Strata";
+let typeOfRepoName = typeof repoName;
+
+// instanceof
+let obj = { name: "Strata" };
+let isObject = obj instanceof Object;
\ No newline at end of file
diff --git a/conformance_testing/babel_to_lean.py b/conformance_testing/babel_to_lean.py
index a45d6461..df35640e 100644
--- a/conformance_testing/babel_to_lean.py
+++ b/conformance_testing/babel_to_lean.py
@@ -36,8 +36,48 @@ def parse_ts_type(j):
         inner = {"elementType": tagged_elem}
         add_missing_node_info(j, inner)
         return {"TS_TSArrayType": inner}
+    elif t == "TSTypeLiteral":
+        # Support object type literals like { x: number; y: string }
+        members = []
+        for m in j.get("members", []):
+            m_type = m.get("type")
+            if m_type == "TSPropertySignature":
+                key_node = m.get("key")
+                key_name = None
+                if key_node is not None:
+                    key_kind = key_node.get("type")
+                    if key_kind == "Identifier":
+                        key_name = key_node.get("name")
+                    elif key_kind == "StringLiteral":
+                        key_name = key_node.get("value")
+                # Fallback to empty string if we couldn't extract a name
+                if key_name is None:
+                    key_name = ""
+
+                # Property type annotation is a TSTypeAnnotation node wrapping an inner TS* node
+                ts_type_ann = None
+                type_ann_node = m.get("typeAnnotation")
+                if type_ann_node is not None:
+                    inner_ann = type_ann_node.get("typeAnnotation")
+                    if inner_ann is not None:
+                        ts_type_ann = parse_ts_type(inner_ann)
+
+                member_inner = {
+                    "key": key_name,
+                    "typeAnnotation": ts_type_ann
+                }
+                add_missing_node_info(m, member_inner)
+                members.append(member_inner)
+            else:
+                print("Unsupported TSTypeElement in TSTypeLiteral: " + str(m_type), file=sys.stderr)
+
+        inner = { "members": members }
+        add_missing_node_info(j, inner)
+        return { "TS_TSTypeLiteral": inner }
     elif t == "TSAnyKeyword" or t is None:
         return None
+    elif t == "TSUnionType":
+        return None
     else:
         print("Unsupported type annotation type: " + str(t), file=sys.stderr)
         return None
@@ -62,7 +102,8 @@ def parse_binary_expression(j):
 
 def parse_unary_expression(j):
     target_j = {
-        "argument": parse_expression(j['argument'])
+        "argument": parse_expression(j['argument']),
+        "operator": j['operator']
     }
     add_missing_node_info(j, target_j)
     return target_j
@@ -346,6 +387,29 @@ def parse_break_statement(j):
     }
     add_missing_node_info(j, target_j)
     return target_j
+    
+def parse_type_alias_declaration(j):
+    type_ann_node = j["typeAnnotation"]
+    ann_type = type_ann_node.get("type")
+
+    if ann_type == "TSUnionType":
+        inner_types = type_ann_node.get("types", [])
+        tagged_types = [parse_ts_type(tnode) for tnode in inner_types]
+    else:
+        single = parse_ts_type(type_ann_node)
+        tagged_types = [single] if single is not None else []
+
+    union_struct = {
+        "types": tagged_types
+    }
+    add_missing_node_info(type_ann_node, union_struct)
+
+    target_j = {
+        "id": parse_identifier(j["id"]),
+        "typeAnnotation": union_struct,
+    }
+    add_missing_node_info(j, target_j)
+    return target_j
 
 def parse_statement(j):
     match j['type']:
@@ -382,6 +446,8 @@ def parse_statement(j):
         # case "ForInStatement":
         # case "ForOfStatement":
         # case "ClassDeclaration":
+        case "TSTypeAliasDeclaration":
+            return {"TS_TypeAliasDeclaration": parse_type_alias_declaration(j)}
         case _:
             print("Unsupported statement type: " + j['type'], file=sys.stderr)
             return j