diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean
index 901dbeb9..df18115e 100644
--- a/Strata/DDM/AST.lean
+++ b/Strata/DDM/AST.lean
@@ -90,6 +90,9 @@ inductive TypeExprF (α : Type) where
 | ident (ann : α) (name : QualifiedIdent) (args : Array (TypeExprF α))
   /-- A bound type variable at the given deBruijn index in the context. -/
 | bvar (ann : α) (index : Nat)
+  /-- A polymorphic type variable (universally quantified).
+      Used for polymorphic function type parameters -/
+| tvar (ann : α) (name : String)
   /-- A reference to a global variable along with any arguments to ensure it is well-typed. -/
 | fvar (ann : α) (fvar : FreeVarIndex) (args : Array (TypeExprF α))
   /-- A function type. -/
@@ -101,6 +104,7 @@ namespace TypeExprF
 def ann {α} : TypeExprF α → α
 | .ident ann _ _ => ann
 | .bvar ann _ => ann
+| .tvar ann _ => ann
 | .fvar ann _ _ => ann
 | .arrow ann _ _ => ann
 
@@ -112,6 +116,7 @@ protected def incIndices {α} (tp : TypeExprF α) (count : Nat) : TypeExprF α :
   | .ident n i args => .ident n i (args.attach.map fun ⟨e, _⟩ => e.incIndices count)
   | .fvar n f args => .fvar n f (args.attach.map fun ⟨e, _⟩ => e.incIndices count)
   | .bvar n idx => .bvar n (idx + count)
+  | .tvar n name => .tvar n name  -- tvar doesn't use indices
   | .arrow n a r => .arrow n (a.incIndices count) (r.incIndices count)
 
 /-- Return true if type expression has a bound variable. -/
@@ -119,6 +124,7 @@ protected def hasUnboundVar {α} (bindingCount : Nat := 0) : TypeExprF α → Bo
 | .ident _ _ args => args.attach.any (fun ⟨e, _⟩ => e.hasUnboundVar bindingCount)
 | .fvar _ _ args => args.attach.any (fun ⟨e, _⟩ => e.hasUnboundVar bindingCount)
 | .bvar _ idx => idx ≥ bindingCount
+| .tvar _ _ => true
 | .arrow _ a r => a.hasUnboundVar bindingCount || r.hasUnboundVar bindingCount
 termination_by e => e
 
@@ -135,6 +141,7 @@ protected def instTypeM {m α} [Monad m] (d : TypeExprF α) (bindings : α → N
   | .ident n i a =>
     .ident n i <$> a.attach.mapM (fun ⟨e, _⟩ => e.instTypeM bindings)
   | .bvar n idx => bindings n idx
+  | .tvar n name => pure (.tvar n name)
   | .fvar n idx a => .fvar n idx <$> a.attach.mapM (fun ⟨e, _⟩ => e.instTypeM bindings)
   | .arrow n a b => .arrow n <$> a.instTypeM bindings <*> b.instTypeM bindings
 termination_by d
@@ -472,6 +479,15 @@ def scopeDatatypeIndex (metadata : Metadata) : Option (Nat × Nat) :=
   | some #[.catbvar nameIdx, .catbvar typeParamsIdx] => some (nameIdx, typeParamsIdx)
   | some _ => panic! s!"Unexpected argument count to scopeDatatype"
 
+/-- Returns the typeArgs index if @[scopeTypeVars] is present.
+    Used for polymorphic function declarations where type parameters should be
+    added as .tvar bindings. -/
+def scopeTypeVarsIndex (metadata : Metadata) : Option Nat :=
+  match metadata[q`StrataDDL.scopeTypeVars]? with
+  | none => none
+  | some #[.catbvar typeArgsIdx] => some typeArgsIdx
+  | some _ => panic! s!"Unexpected argument count to scopeTypeVars"
+
 /-- Returns the index of the value in the binding for the given variable of the scope to use. -/
 private def resultIndex (metadata : Metadata) : Option Nat :=
   match metadata[MetadataAttr.scopeName]? with
@@ -510,8 +526,12 @@ generate types.
 inductive PreType where
   /-- A dialect defined type. -/
 | ident (ann : SourceRange) (name : QualifiedIdent) (args : Array PreType)
-  /-- A bound type variable at the given deBruijn index in the context. -/
+  /-- A bound type variable at the given deBruijn index in the context.
+      Used for type alias parameters -/
 | bvar (ann : SourceRange) (index : Nat)
+  /-- A polymorphic type variable (universally quantified).
+      Used for polymorphic function type parameters -/
+| tvar (ann : SourceRange) (name : String)
   /-- A reference to a global variable along with any arguments to ensure it is well-typed. -/
 | fvar (ann : SourceRange) (fvar : FreeVarIndex) (args : Array PreType)
   /-- A function type. -/
@@ -526,6 +546,7 @@ namespace PreType
 def ann : PreType → SourceRange
 | .ident ann _ _ => ann
 | .bvar ann _ => ann
+| .tvar ann _ => ann
 | .fvar ann _ _ => ann
 | .arrow ann _ _ => ann
 | .funMacro ann _ _ => ann
@@ -533,6 +554,7 @@ def ann : PreType → SourceRange
 def ofType : TypeExprF SourceRange → PreType
 | .ident loc name args => .ident loc name (args.map fun a => .ofType a)
 | .bvar loc idx => .bvar loc idx
+| .tvar loc name => .tvar loc name
 | .fvar loc idx args => .fvar loc idx (args.map fun a => .ofType a)
 | .arrow loc a r => .arrow loc (.ofType a) (.ofType r)
 termination_by tp => tp
@@ -696,6 +718,18 @@ def argScopeDatatypeLevel (argDecls : ArgDecls) (level : Fin argDecls.size) : Op
     else
       panic! s!"scopeDatatype name index {nameIdx} out of bounds ({level.val})"
 
+/-- Returns the typeArgs level if @[scopeTypeVars] is present.
+    This is used for polymorphic function declarations where type parameters like `<a, b>`
+    should be added as .tvar bindings when parsing parameter types and return type. -/
+def argScopeTypeVarsLevel (argDecls : ArgDecls) (level : Fin argDecls.size) : Option (Fin level.val) :=
+  match argDecls[level].metadata.scopeTypeVarsIndex with
+  | none => none
+  | some typeArgsIdx =>
+    if h : typeArgsIdx < level.val then
+      some ⟨level.val - (typeArgsIdx + 1), by omega⟩
+    else
+      panic! s!"scopeTypeVars typeArgs index {typeArgsIdx} out of bounds ({level.val})"
+
 end ArgDecls
 
 /--
@@ -752,10 +786,10 @@ structure ConstructorInfo where
 
 /--
 Build a TypeExpr reference to the datatype with type parameters, using
-`.fvar` for the datatype's GlobalContext index.
+`.fvar` for the datatype's GlobalContext index and `.tvar` for type parameters.
 -/
 def mkDatatypeTypeRef (ann : SourceRange) (datatypeIndex : FreeVarIndex) (typeParams : Array String) : TypeExpr :=
-  let typeArgs := typeParams.mapIdx fun i _ => TypeExprF.bvar ann i
+  let typeArgs := typeParams.map fun name => TypeExprF.tvar ann name
   TypeExprF.fvar ann datatypeIndex typeArgs
 
 /--
diff --git a/Strata/DDM/BuiltinDialects/StrataDDL.lean b/Strata/DDM/BuiltinDialects/StrataDDL.lean
index 417a84af..8c0a7437 100644
--- a/Strata/DDM/BuiltinDialects/StrataDDL.lean
+++ b/Strata/DDM/BuiltinDialects/StrataDDL.lean
@@ -171,6 +171,8 @@ def StrataDDL : Dialect := BuiltinM.create! "StrataDDL" #[initDialect] do
    used for recursive datatype definitions where the datatype name must be visible when parsing constructor field types (e.g., `tail: List` in
    `Cons(head: int, tail: List)`) -/
   declareMetadata { name := "scopeDatatype", args := #[.mk "name" .ident, .mk "typeParams" .ident] }
+  -- Metadata for bringing type variable names into scope as .tvar bindings.
+  declareMetadata { name := "scopeTypeVars", args := #[.mk "typeArgs" .ident] }
 
 end Strata
 end
diff --git a/Strata/DDM/Elab/Core.lean b/Strata/DDM/Elab/Core.lean
index e67e56b7..2091862b 100644
--- a/Strata/DDM/Elab/Core.lean
+++ b/Strata/DDM/Elab/Core.lean
@@ -54,6 +54,7 @@ partial def expandMacros (m : DialectMap) (f : PreType) (args : Nat → Option A
   | .arrow loc a b => .arrow loc <$> expandMacros m a args <*> expandMacros m b args
   | .fvar loc i a => .fvar loc i <$> a.mapM fun e => expandMacros m e args
   | .bvar loc idx => pure (.bvar loc idx)
+  | .tvar loc name => pure (.tvar loc name)
   | .funMacro loc i r => do
     let r ← expandMacros m r args
     match args i with
@@ -77,7 +78,7 @@ the head is in a normal form.
 -/
 partial def hnf (tctx : TypingContext) (e : TypeExpr) : TypeExpr :=
   match e with
-  | .arrow .. | .ident .. => e
+  | .arrow .. | .ident .. | .tvar .. => e
   | .fvar _ idx args =>
     let gctx := tctx.globalContext
     match gctx.kindOf! idx with
@@ -94,6 +95,7 @@ partial def hnf (tctx : TypingContext) (e : TypeExpr) : TypeExpr :=
       assert! d.isGround
       hnf (tctx.drop (idx + 1)) d
     | .type _ _ none => e
+    | .tvar _ _ => e
     | _ => panic! "Expected a type"
 
 /--
@@ -176,6 +178,9 @@ def resolveTypeBinding (tctx : TypingContext) (loc : SourceRange) (name : String
     if let .type loc [] _ := k then
       let info : TypeInfo := { inputCtx := tctx, loc := loc, typeExpr := .bvar loc idx, isInferred := false }
       return .node (.ofTypeInfo info) #[]
+    else if let .tvar loc tvarName := k then
+      let info : TypeInfo := { inputCtx := tctx, loc := loc, typeExpr := .tvar loc tvarName, isInferred := false }
+      return .node (.ofTypeInfo info) #[]
     else
       logErrorMF loc mf!"Expected a type instead of {k}"
       return default
@@ -326,7 +331,7 @@ N.B. This expects that macros have already been expanded in e.
 -/
 partial def headExpandTypeAlias (gctx : GlobalContext) (e : TypeExpr) : TypeExpr :=
   match e with
-  | .arrow .. | .ident .. | .bvar .. => e
+  | .arrow .. | .ident .. | .bvar .. | .tvar .. => e
   | .fvar _ idx args =>
     match gctx.kindOf! idx with
     | .expr _ => panic! "Type free variable bound to expression."
@@ -347,6 +352,10 @@ partial def checkExpressionType (tctx : TypingContext) (itype rtype : TypeExpr)
   let itype := tctx.hnf itype
   let rtype := tctx.hnf rtype
   match itype, rtype with
+  -- tvar matches anything (dialect responsible for typechecking)
+  | .tvar _ n1, .tvar _ n2 => return n1 == n2
+  | .tvar _ _, _ => return true
+  | _, .tvar _ _ => return true
   | .ident _ iq ia, .ident _ rq ra =>
     if p : iq = rq ∧ ia.size = ra.size then do
       for i in Fin.range ia.size do
@@ -468,9 +477,12 @@ partial def unifyTypes
       if !(← checkExpressionType tctx inferredType info.typeExpr) then
         logErrorMF exprLoc mf!"Expression has type {withBindings tctx.bindings (mformat inferredType)} when {withBindings tctx.bindings (mformat info.typeExpr)} expected."
       pure args
+  | .tvar _ _ =>
+    -- tvar nodes are passed through without attempting unification
+    pure args
   | .arrow _ ea er =>
     match inferredType with
-    | .ident .. | .bvar .. | .fvar .. =>
+    | .ident .. | .bvar .. | .fvar .. | .tvar .. =>
       logErrorMF exprLoc mf!"Expected {expectedType} when {inferredType} found"
       pure args
     | .arrow _ ia ir =>
@@ -752,6 +764,12 @@ def translateBindingKind (tree : Tree) : ElabM BindingKind := do
             else
               logErrorMF nameLoc mf!"Unexpected arguments to type variable {name}."
               return default
+          else if let .tvar loc tvarName := k then
+            if tpArgs.isEmpty then
+              return .expr (.tvar loc tvarName)
+            else
+              logErrorMF nameLoc mf!"Unexpected arguments to type variable {name}."
+              return default
           else
             logErrorMF nameLoc mf!"Expected a type instead of {k}"
             return default
@@ -795,12 +813,15 @@ def evalBindingSpec
     let (bindings, success) ← runChecked <| elabArgIndex initSize args b.argsIndex fun argLoc b =>
           match b.kind with
           | .expr tp =>
-            pure (b.ident, tp)
+            pure (some (b.ident, tp))
+          | .tvar .. =>
+            pure none
           | .type .. | .cat _ => do
             logError argLoc "Expecting expressions in variable binding"
-            pure default
+            pure none
     if !success then
       return default
+    let bindings := bindings.filterMap id
     let typeTree := args[b.typeIndex.toLevel]
     let kind ←
           match typeTree.info with
@@ -827,6 +848,8 @@ def evalBindingSpec
           match b.kind with
           | .type _ [] _ =>
             pure ()
+          | .tvar _ _ =>
+            pure ()
           | .type .. | .expr _ | .cat _ => do
             logError argLoc s!"{b.ident} must be have type Type instead of {repr b.kind}."
           return b.ident
@@ -955,6 +978,33 @@ def unwrapTree (tree : Tree) (unwrap : Bool) : Arg :=
     | .ofBytesInfo info => .bytes info.loc info.val
     | _ => tree.arg  -- Fallback for non-unwrappable types
 
+/--
+Extract type variable names from a TypeArgs tree (or Option TypeArgs).
+TypeArgs is an operation `type_args` with one child that is `CommaSepBy Ident`.
+Option TypeArgs wraps this in an OptionInfo node.
+-/
+def extractTypeVarNames (tree : Tree) : Array String :=
+  let innerTree :=
+    match tree.info with
+    | .ofOptionInfo _ =>
+      match tree.children[0]? with
+      | none => none
+      | some t => some t
+    | _ => some tree
+  match innerTree with
+  | none => #[]
+  | some typeArgsTree =>
+    -- typeArgsTree should be the type_args operation
+    -- Its first child should be CommaSepBy Ident
+    match typeArgsTree.children[0]? with
+    | none => #[]
+    | some commaSepTree =>
+      -- commaSepTree has CommaSepInfo with children that are Ident trees
+      commaSepTree.children.filterMap fun identTree =>
+        match identTree.info with
+        | .ofIdentInfo info => some info.val
+        | _ => none
+
 mutual
 
 partial def elabOperation (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
@@ -1017,21 +1067,43 @@ partial def runSyntaxElaborator
             | .ofIdentInfo info => info.val
             | _ => panic! "Expected identifier for datatype name"
           let baseCtx := typeParamsT.resultContext
+          -- Extract type parameter names from the bindings
+          let typeParamNames := baseCtx.bindings.toArray.filterMap fun b =>
+            match b.kind with
+            | .type _ [] _ => some b.ident
+            | _ => none
           -- Add the datatype name to the GlobalContext as a type
           let gctx := baseCtx.globalContext
           let gctx :=
             if datatypeName ∈ gctx then gctx
-            else gctx.push datatypeName (GlobalKind.type [] none)
-          -- Create a new typing context with the updated GlobalContext
-          pure (baseCtx.withGlobalContext gctx)
+            else gctx.push datatypeName (GlobalKind.type typeParamNames.toList none)
+          -- Add .tvar bindings for type parameters
+          let loc := typeParamsT.info.loc
+          let tctx := typeParamNames.foldl (init := baseCtx.withGlobalContext gctx) fun ctx name =>
+            ctx.push { ident := name, kind := .tvar loc name }
+          pure tctx
         | _, _ => continue
       | none =>
-        match ae.contextLevel with
-        | some idx =>
-          match trees[idx] with
-          | some t => pure t.resultContext
+        -- Check for typeVarsScope (polymorphic function type parameters)
+        match ae.typeVarsScope with
+        | some typeArgsLevel =>
+          match trees[typeArgsLevel] with
+          | some typeArgsTree =>
+            -- Extract identifiers from TypeArgs and add as .tvar bindings
+            let baseCtx := typeArgsTree.resultContext
+            let typeVarNames := extractTypeVarNames typeArgsTree
+            let tctx := typeVarNames.foldl (init := baseCtx) fun ctx name =>
+              let loc := typeArgsTree.info.loc
+              ctx.push { ident := name, kind := .tvar loc name }
+            pure tctx
           | none => continue
-        | none => pure tctx0
+        | none =>
+          match ae.contextLevel with
+          | some idx =>
+            match trees[idx] with
+            | some t => pure t.resultContext
+            | none => continue
+          | none => pure tctx0
     let astx := args[ae.syntaxLevel]
     let expectedKind := argDecls[argLevel].kind
     match expectedKind with
@@ -1209,6 +1281,9 @@ partial def elabExpr (tctx : TypingContext) (stx : Syntax) : ElabM Tree := do
       | .type _ _params _ =>
         logErrorMF loc mf!"{name} is a type when an expression is required."
         return default
+      | .tvar _ _ =>
+        logErrorMF loc mf!"{name} is a type variable when an expression is required."
+        return default
       | .cat c =>
         logErrorMF loc mf!"{name} has category {c} when an expression is required."
         return default
diff --git a/Strata/DDM/Elab/DialectM.lean b/Strata/DDM/Elab/DialectM.lean
index a10d4d11..bd572b3a 100644
--- a/Strata/DDM/Elab/DialectM.lean
+++ b/Strata/DDM/Elab/DialectM.lean
@@ -29,6 +29,7 @@ private def foldBoundTypeVars {α} (tp : PreType) (init : α) (f : α → Nat 
   | .ident _ _ a => a.attach.foldl (init := init) fun r ⟨e, _⟩ => e.foldBoundTypeVars r f
   | .fvar _ _ a => a.attach.foldl (init := init) fun r ⟨e, _⟩ => e.foldBoundTypeVars r f
   | .bvar _ i => f init i
+  | .tvar _ _ => init
   | .arrow _ a r => r.foldBoundTypeVars (a.foldBoundTypeVars init f) f
   | .funMacro _ _ r => r.foldBoundTypeVars init f
 
diff --git a/Strata/DDM/Elab/SyntaxElab.lean b/Strata/DDM/Elab/SyntaxElab.lean
index 0f73a6cf..8d09f916 100644
--- a/Strata/DDM/Elab/SyntaxElab.lean
+++ b/Strata/DDM/Elab/SyntaxElab.lean
@@ -27,6 +27,9 @@ structure ArgElaborator where
   -- Datatype scope: (nameLevel, typeParamsLevel) for recursive datatype definitions
   -- When set, the datatype name is added to the typing context as a type
   datatypeScope : Option (Fin argLevel × Fin argLevel) := .none
+  -- Type vars scope: level of TypeArgs argument for polymorphic function declarations
+  -- When set, identifiers from TypeArgs are added as .tvar bindings
+  typeVarsScope : Option (Fin argLevel) := .none
   -- Whether to unwrap this argument
   unwrap : Bool := false
 deriving Inhabited, Repr
@@ -65,6 +68,7 @@ private def push (as : ArgElaborators)
     argLevel := argLevel.val
     contextLevel := argDecls.argScopeLevel argLevel
     datatypeScope := argDecls.argScopeDatatypeLevel argLevel
+    typeVarsScope := argDecls.argScopeTypeVarsLevel argLevel
   }
   have scp : sc < sc + 1 := by grind
   { as with argElaborators := as.argElaborators.push ⟨newElab, scp⟩ }
@@ -81,6 +85,7 @@ private def pushWithUnwrap
     argLevel := argLevel.val
     contextLevel := argDecls.argScopeLevel argLevel
     datatypeScope := argDecls.argScopeDatatypeLevel argLevel
+    typeVarsScope := argDecls.argScopeTypeVarsLevel argLevel
     unwrap := unwrap
   }
   have scp : sc < sc + 1 := by grind
diff --git a/Strata/DDM/Elab/Tree.lean b/Strata/DDM/Elab/Tree.lean
index be2a17e8..12f4782a 100644
--- a/Strata/DDM/Elab/Tree.lean
+++ b/Strata/DDM/Elab/Tree.lean
@@ -32,6 +32,11 @@ over the parameters.
 Variable belongs to the particular category below.
 -/
 | cat (k : SyntaxCat)
+/--
+Variable is a polymorphic type variable (for function type parameters).
+These are passed through to the dialect's typechecker for inference.
+-/
+| tvar (ann : SourceRange) (name : String)
 deriving Inhabited, Repr
 
 namespace BindingKind
@@ -48,6 +53,7 @@ def ofCat (c : SyntaxCat) : BindingKind :=
 def categoryOf : BindingKind → SyntaxCat
 | .expr tp => .atom tp.ann q`Init.Expr
 | .type loc _ _ => .atom loc q`Init.Type
+| .tvar loc _ => .atom loc q`Init.Type
 | .cat c => c
 
 instance : ToStrataFormat BindingKind where
@@ -55,6 +61,7 @@ instance : ToStrataFormat BindingKind where
     match bk with
     | .expr tp => mformat tp
     | .type _ params _ => mformat (params.foldr (init := f!"Type") (fun a f => f!"({a} : Type) -> {f}"))
+    | .tvar _ name => mformat f!"tvar({name})"
     | .cat c => mformat c
 
 end BindingKind
diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean
index 03b761c7..47012bca 100644
--- a/Strata/DDM/Format.lean
+++ b/Strata/DDM/Format.lean
@@ -275,6 +275,7 @@ private protected def mformat : TypeExprF α → StrataFormat
 | .ident _ tp a => a.attach.foldl (init := mformat tp) fun m ⟨e, _⟩ =>
   mf!"{m} {e.mformat.ensurePrec (appPrec + 1)}".setPrec appPrec
 | .bvar _ idx => .bvar idx
+| .tvar _ name => mf!"tvar!{name}"
 | .fvar _ idx a => a.attach.foldl (init := .fvar idx) fun m ⟨e, _⟩ =>
   mf!"{m} {e.mformat.ensurePrec (appPrec + 1)}".setPrec appPrec
 | .arrow _ a r => mf!"{a.mformat.ensurePrec (arrowPrec+1)} -> {r.mformat.ensurePrec arrowPrec}"
@@ -289,6 +290,7 @@ namespace PreType
 private protected def mformat : PreType → StrataFormat
 | .ident _ tp a => a.attach.foldl (init := mformat tp) (fun m ⟨e, _⟩ => mf!"{m} {e.mformat}")
 | .bvar _ idx => .bvar idx
+| .tvar _ name => mf!"tvar!{name}"
 | .fvar _ idx a => a.attach.foldl (init := .fvar idx) (fun m ⟨e, _⟩ => mf!"{m} {e.mformat}")
 | .arrow _ a r => mf!"{a.mformat} -> {r.mformat}"
 | .funMacro _ idx r => mf!"fnOf({StrataFormat.bvar idx}, {r.mformat})"
diff --git a/Strata/DDM/Integration/Lean/ToExpr.lean b/Strata/DDM/Integration/Lean/ToExpr.lean
index 02d74f65..981c15e9 100644
--- a/Strata/DDM/Integration/Lean/ToExpr.lean
+++ b/Strata/DDM/Integration/Lean/ToExpr.lean
@@ -131,6 +131,8 @@ private protected def toExpr {α} [ToExpr α] : TypeExprF α → Lean.Expr
   astAnnExpr! ident ann (toExpr nm) ae
 | .bvar ann idx =>
   astAnnExpr! bvar ann (toExpr idx)
+| .tvar ann name =>
+  astAnnExpr! tvar ann (toExpr name)
 | .fvar ann idx a =>
   let ae := arrayToExpr levelZero (TypeExprF.typeExpr (toTypeExpr α)) (a.map (·.toExpr))
   astAnnExpr! fvar ann (toExpr idx) ae
@@ -223,6 +225,7 @@ private protected def toExpr : PreType → Lean.Expr
   let args := arrayToExpr .zero PreType.typeExpr (a.map (·.toExpr))
   astExpr! ident (toExpr loc) (toExpr nm) args
 | .bvar loc idx => astExpr! bvar (toExpr loc) (toExpr idx)
+| .tvar loc name => astExpr! tvar (toExpr loc) (toExpr name)
 | .fvar loc idx a =>
     let args := arrayToExpr .zero PreType.typeExpr (a.map (·.toExpr))
     astExpr! fvar (toExpr loc) (toExpr idx) args
diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean
index 160367da..459db1df 100644
--- a/Strata/DDM/Ion.lean
+++ b/Strata/DDM/Ion.lean
@@ -385,6 +385,9 @@ private protected def toIon {α} [ToIon α] (refs : SymbolIdCache) (tpe : TypeEx
     -- A bound type variable with the given index.
     | .bvar ann vidx =>
       return Ion.sexp #[ionSymbol! "bvar", ← toIon ann, .int vidx]
+    -- A polymorphic type variable with the given name.
+    | .tvar ann name =>
+      return Ion.sexp #[ionSymbol! "tvar", ← toIon ann, .string name]
     | .fvar ann idx a => do
       let s : Array (Ion SymbolId) := #[ionSymbol! "fvar", ← toIon ann, .int idx]
       let s ← a.attach.mapM_off (init := s) fun ⟨e, _⟩ =>
@@ -416,6 +419,11 @@ private protected def fromIon {α} [FromIon α] (v : Ion SymbolId) : FromIonM (T
     return .bvar
       (← FromIon.fromIon args[1])
       (← .asNat "Type expression bvar" args[2])
+  | "tvar" =>
+    let ⟨p⟩ ← .checkArgCount "Type expression tvar" args 3
+    return .tvar
+      (← FromIon.fromIon args[1])
+      (← .asString "Type expression tvar name" args[2])
   | "fvar" =>
     let ⟨p⟩ ← .checkArgMin "Type expression free variable" args 3
     let ann ← FromIon.fromIon args[1]
@@ -931,6 +939,9 @@ private protected def toIon (refs : SymbolIdCache) (tpe : PreType) : InternM (Io
     -- A bound type variable with the given index.
     | .bvar loc vidx =>
       return Ion.sexp #[ionSymbol! "bvar", ← toIon loc, .int vidx]
+    -- A polymorphic type variable with the given name.
+    | .tvar loc name =>
+      return Ion.sexp #[ionSymbol! "tvar", ← toIon loc, .string name]
     | .fvar loc idx a => do
       let s : Array (Ion SymbolId) := #[ionSymbol! "fvar", ← toIon loc, .int idx]
       let s ← a.attach.mapM_off (init := s) fun ⟨e, _⟩ => e.toIon refs
@@ -958,6 +969,11 @@ private protected def fromIon (v : Ion SymbolId) : FromIonM PreType := do
     return PreType.bvar
       (← fromIon args[1])
       (← .asNat "TypeExpr bvar" args[2])
+  | "tvar" =>
+    let ⟨p⟩ ← .checkArgCount "PreType tvar" args 3
+    return PreType.tvar
+      (← fromIon args[1])
+      (← .asString "PreType tvar name" args[2])
   | "fvar" =>
     let ⟨p⟩ ← .checkArgMin "fvar" args 3
     let ann ← fromIon args[1]
diff --git a/Strata/Languages/Boogie/DDMTransform/Parse.lean b/Strata/Languages/Boogie/DDMTransform/Parse.lean
index d4e8494e..55525b3c 100644
--- a/Strata/Languages/Boogie/DDMTransform/Parse.lean
+++ b/Strata/Languages/Boogie/DDMTransform/Parse.lean
@@ -265,8 +265,8 @@ op command_constdecl (name : Ident,
 @[declareFn(name, b, r)]
 op command_fndecl (name : Ident,
                    typeArgs : Option TypeArgs,
-                   @[scope(typeArgs)] b : Bindings,
-                   @[scope (typeArgs)] r : Type) : Command =>
+                   @[scopeTypeVars(typeArgs)] b : Bindings,
+                   @[scopeTypeVars(typeArgs)] r : Type) : Command =>
   "function " name typeArgs b ":" r ";\n";
 
 category Inline;
@@ -275,8 +275,8 @@ op inline () : Inline => "inline";
 @[declareFn(name, b, r)]
 op command_fndef (name : Ident,
                   typeArgs : Option TypeArgs,
-                  @[scope (typeArgs)] b : Bindings,
-                  @[scope (typeArgs)] r : Type,
+                  @[scopeTypeVars(typeArgs)] b : Bindings,
+                  @[scopeTypeVars(typeArgs)] r : Type,
                   @[scope(b)] c : r,
                   // Prefer adding the inline attribute here so
                   // that the order of the arguments in the fndecl and fndef
diff --git a/Strata/Languages/Boogie/DDMTransform/Translate.lean b/Strata/Languages/Boogie/DDMTransform/Translate.lean
index 0c563dbb..174ccd7f 100644
--- a/Strata/Languages/Boogie/DDMTransform/Translate.lean
+++ b/Strata/Languages/Boogie/DDMTransform/Translate.lean
@@ -272,7 +272,12 @@ partial def translateLMonoTy (bindings : TransBindings) (arg : Arg) :
     assert! i < bindings.boundTypeVars.size
     let var := bindings.boundTypeVars[bindings.boundTypeVars.size - (i+1)]!
     return (.ftvar var)
-  | _ => TransM.error s!"translateLMonoTy not yet implemented {repr tp}"
+  | .tvar _ name =>
+    return (.ftvar name)
+  | .arrow _ argTp resTp =>
+     let argTy ← translateLMonoTy bindings (.type argTp)
+     let resTy ← translateLMonoTy bindings (.type resTp)
+     return (.arrow argTy resTy)
 
 partial def translateLMonoTys (bindings : TransBindings) (args : Array Arg) :
   TransM (Array LMonoTy) :=
diff --git a/Strata/Languages/C_Simp/DDMTransform/Translate.lean b/Strata/Languages/C_Simp/DDMTransform/Translate.lean
index b7df8b3b..5e8db806 100644
--- a/Strata/Languages/C_Simp/DDMTransform/Translate.lean
+++ b/Strata/Languages/C_Simp/DDMTransform/Translate.lean
@@ -151,6 +151,8 @@ partial def translateLMonoTy (bindings : TransBindings) (arg : Arg) :
     assert! i < bindings.boundTypeVars.size
     let var := bindings.boundTypeVars[bindings.boundTypeVars.size - (i+1)]!
     return (.ftvar var)
+  | .tvar _ name =>
+    return (.ftvar name)
   | _ => TransM.error s!"translateLMonoTy not yet implemented {repr tp}"
 
 partial def translateLMonoTys (bindings : TransBindings) (args : Array Arg) :
diff --git a/Strata/Languages/Python/BoogiePrelude.lean b/Strata/Languages/Python/BoogiePrelude.lean
index 7eb7cd3d..abc2ed51 100644
--- a/Strata/Languages/Python/BoogiePrelude.lean
+++ b/Strata/Languages/Python/BoogiePrelude.lean
@@ -46,38 +46,13 @@ datatype Error () {
 // /////////////////////////////////////////////////////////////////////////////////////
 // Regular Expressions
 
-type Except (err : Type, ok : Type);
-
-// FIXME:
-// Once DDM support polymorphic functions (and not just type declarations),
-// we will be able to define the following generic functions and axioms. For now,
-// we manually define appropriate instantiations.
-// Also: when ADT support is lifted up to Boogie, all these
-// constructors, testers, destructors, and axioms will be auto-generated.
-// How will the DDM keep track of them?
-
-// // Constructors
-// function Except_mkOK(err : Type, ok : Type, val : ok) : Except err ok;
-// function Except_mkErr(err : Type, ok : Type, val : err) : Except err ok;
-// // Testers
-// function Except_isOK(err : Type, ok : Type, x : Except err ok) : bool;
-// function Except_isErr(err : Type, ok : Type, x : Except err ok) : bool;
-// // Destructors
-// function Except_getOK(err : Type, ok : Type, x : Except err ok) : ok;
-// function Except_getErr(err : Type, ok : Type, x : Except err ok) : err;
-// // Axioms
-// // Testers of Constructors
-// axiom [Except_isOK_mkOK]: (forall x : ok :: Except_isOK(Except_mkOK x));
-// axiom [Except_isErr_mkErr]: (forall x : err :: Except_isErr(Except_mkErr x));
-// // Destructors of Constructors
-// axiom [Except_getOK_mkOK]: (forall x : ok :: Except_getOK(Except_mkOK x) == x);
-// axiom [Except_getErr_mkErr]: (forall x : err :: Except_isErr(Except_mkErr x));
-
-datatype ExceptErrorRegex () {
-  ExceptErrorRegex_mkOK(ExceptErrorRegex_getOK: regex),
-  ExceptErrorRegex_mkErr(ExceptErrorRegex_getErr: Error)
+datatype Except (err : Type, ok : Type) {
+  Except_mkOK(Except_getOK: ok),
+  Except_mkErr(Except_getErr: err)
 };
 
+type ExceptErrorRegex := Except Error regex;
+
 // NOTE: `re.match` returns a `Re.Match` object, but for now, we are interested
 // only in match/nomatch, which is why we return `bool` here.
 function PyReMatchRegex(pattern : regex, str : string, flags : int) : bool;
diff --git a/StrataTest/Languages/B3/DDMFormatTests.lean b/StrataTest/Languages/B3/DDMFormatTests.lean
index e28b3942..be25b503 100644
--- a/StrataTest/Languages/B3/DDMFormatTests.lean
+++ b/StrataTest/Languages/B3/DDMFormatTests.lean
@@ -119,6 +119,7 @@ mutual
   partial def typeExprFUnitToSourceRange : TypeExprF Unit → TypeExprF SourceRange
     | .ident () tp a => .ident default tp (a.map typeExprFUnitToSourceRange)
     | .bvar () idx => .bvar default idx
+    | .tvar () name => .tvar default name
     | .fvar () idx a => .fvar default idx (a.map typeExprFUnitToSourceRange)
     | .arrow () a r => .arrow default (typeExprFUnitToSourceRange a) (typeExprFUnitToSourceRange r)
 
diff --git a/StrataTest/Languages/Boogie/PolymorphicDatatypeTest.lean b/StrataTest/Languages/Boogie/PolymorphicDatatypeTest.lean
new file mode 100644
index 00000000..6c2651f7
--- /dev/null
+++ b/StrataTest/Languages/Boogie/PolymorphicDatatypeTest.lean
@@ -0,0 +1,319 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Boogie.Verifier
+
+/-!
+# Polymorphic Datatype Integration Tests
+
+Tests polymorphic datatype declarations in Boogie syntax, including function
+generation (constructor, accessor, etc) and SMT verification for concrete
+instantiations.
+-/
+
+namespace Strata.PolymorphicDatatypeTest
+
+---------------------------------------------------------------------
+-- Test 1: Option Datatype Declaration
+---------------------------------------------------------------------
+
+def optionDeclPgm : Program :=
+#strata
+program Boogie;
+
+datatype Option (a : Type) { None(), Some(value: a) };
+
+#end
+
+/-- info: ok: type:
+Option
+Type Arguments:
+[a]
+Constructors:
+[Name: None Args: [] Tester: Option..isNone , Name: Some Args: [(value, a)] Tester: Option..isSome ]-/
+#guard_msgs in
+#eval Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram optionDeclPgm)).fst
+
+---------------------------------------------------------------------
+-- Test 2: Option Used with Concrete Type (int)
+---------------------------------------------------------------------
+
+def optionIntPgm : Program :=
+#strata
+program Boogie;
+
+datatype Option (a : Type) { None(), Some(value: a) };
+
+procedure TestOptionInt() returns ()
+spec {
+  ensures true;
+}
+{
+  var x : Option int;
+  var y : Option int;
+  var v : int;
+
+  x := None();
+  y := Some(42);
+  v := value(y);
+  assert [valIs42]: v == 42;
+};
+#end
+
+/-- info: ok: type:
+Option
+Type Arguments:
+[a]
+Constructors:
+[Name: None Args: [] Tester: Option..isNone , Name: Some Args: [(value, a)] Tester: Option..isSome ]
+
+(procedure TestOptionInt :  () → ())
+modifies: []
+preconditions: 
+postconditions: (TestOptionInt_ensures_0, #true)
+body: init (x : (Option int)) := (init_x_0 : (Option int))
+init (y : (Option int)) := (init_y_1 : (Option int))
+init (v : int) := (init_v_2 : int)
+x := (~None : (Option int))
+y := ((~Some : (arrow int (Option int))) #42)
+v := ((~value : (arrow (Option int) int)) (y : (Option int)))
+assert [valIs42] ((v : int) == #42)-/
+#guard_msgs in
+#eval Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram optionIntPgm)).fst
+
+---------------------------------------------------------------------
+-- Test 3: List Used with Concrete Type (int)
+---------------------------------------------------------------------
+
+def listIntPgm : Program :=
+#strata
+program Boogie;
+
+datatype List (a : Type) { Nil(), Cons(head: a, tail: List a) };
+
+procedure TestListInt() returns ()
+spec {
+  ensures true;
+}
+{
+  var xs : List int;
+  var h : int;
+
+  xs := Cons(1, Cons(2, Nil()));
+  h := head(xs);
+  assert [headIs1]: h == 1;
+};
+#end
+
+/-- info: ok: type:
+List
+Type Arguments:
+[a]
+Constructors:
+[Name: Nil Args: [] Tester: List..isNil , Name: Cons Args: [(head, a), (tail, (List a))] Tester: List..isCons ]
+
+(procedure TestListInt :  () → ())
+modifies: []
+preconditions: 
+postconditions: (TestListInt_ensures_0, #true)
+body: init (xs : (List int)) := (init_xs_0 : (List int))
+init (h : int) := (init_h_1 : int)
+xs := (((~Cons : (arrow int (arrow (List int) (List int)))) #1) (((~Cons : (arrow int (arrow (List int) (List int)))) #2) (~Nil : (List int))))
+h := ((~head : (arrow (List int) int)) (xs : (List int)))
+assert [headIs1] ((h : int) == #1)-/
+#guard_msgs in
+#eval Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram listIntPgm)).fst
+
+---------------------------------------------------------------------
+-- Test 4: Type with Multiple Parameters (Either)
+---------------------------------------------------------------------
+
+def eitherUsePgm : Program :=
+#strata
+program Boogie;
+
+datatype Either (a : Type, b : Type) { Left(l: a), Right(r: b) };
+
+procedure TestEither() returns ()
+spec {
+  ensures true;
+}
+{
+  var x : Either int bool;
+  var y : Either int bool;
+
+  x := Left(42);
+  y := Right(true);
+
+  assert [xIsLeft]: Either..isLeft(x);
+  assert [yIsRight]: Either..isRight(y);
+  assert [lValue]: l(x) == 42;
+};
+#end
+
+/-- info: ok: type:
+Either
+Type Arguments:
+[a, b]
+Constructors:
+[Name: Left Args: [(l, a)] Tester: Either..isLeft , Name: Right Args: [(r, b)] Tester: Either..isRight ]
+
+(procedure TestEither :  () → ())
+modifies: []
+preconditions: 
+postconditions: (TestEither_ensures_0, #true)
+body: init (x : (Either int bool)) := (init_x_0 : (Either int bool))
+init (y : (Either int bool)) := (init_y_1 : (Either int bool))
+x := ((~Left : (arrow int (Either int bool))) #42)
+y := ((~Right : (arrow bool (Either int bool))) #true)
+assert [xIsLeft] ((~Either..isLeft : (arrow (Either int bool) bool)) (x : (Either int bool)))
+assert [yIsRight] ((~Either..isRight : (arrow (Either int bool) bool)) (y : (Either int bool)))
+assert [lValue] (((~l : (arrow (Either int bool) int)) (x : (Either int bool))) == #42)-/
+#guard_msgs in
+#eval Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram eitherUsePgm)).fst
+
+---------------------------------------------------------------------
+-- Test 9: Nested Polymorphic Types (Option of List)
+---------------------------------------------------------------------
+
+def nestedPolyPgm : Program :=
+#strata
+program Boogie;
+
+datatype Option (a : Type) { None(), Some(value: a) };
+datatype List (a : Type) { Nil(), Cons(head: a, tail: List a) };
+
+procedure TestNestedPoly() returns ()
+spec {
+  ensures true;
+}
+{
+  var x : Option (List int);
+
+  x := Some(Cons(1, Nil()));
+  assert [isSome]: Option..isSome(x);
+};
+#end
+
+/-- info: ok: type:
+Option
+Type Arguments:
+[a]
+Constructors:
+[Name: None Args: [] Tester: Option..isNone , Name: Some Args: [(value, a)] Tester: Option..isSome ]
+
+type:
+List
+Type Arguments:
+[a]
+Constructors:
+[Name: Nil Args: [] Tester: List..isNil , Name: Cons Args: [(head, a), (tail, (List a))] Tester: List..isCons ]
+
+(procedure TestNestedPoly :  () → ())
+modifies: []
+preconditions: 
+postconditions: (TestNestedPoly_ensures_0, #true)
+body: init (x : (Option (List int))) := (init_x_0 : (Option (List int)))
+x := ((~Some : (arrow (List int) (Option (List int)))) (((~Cons : (arrow int (arrow (List int) (List int)))) #1) (~Nil : (List int))))
+assert [isSome] ((~Option..isSome : (arrow (Option (List int)) bool)) (x : (Option (List int))))-/
+#guard_msgs in
+#eval Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram nestedPolyPgm)).fst
+
+---------------------------------------------------------------------
+-- Test 6: Polymorphic List Destructor with Havoc (SMT verification)
+---------------------------------------------------------------------
+
+def polyListHavocPgm : Program :=
+#strata
+program Boogie;
+
+datatype List (a : Type) { Nil(), Cons(head: a, tail: List a) };
+
+procedure TestPolyListHavoc() returns ()
+spec {
+  ensures true;
+}
+{
+  var xs : List int;
+  var h : int;
+
+  xs := Nil();
+  havoc xs;
+
+  assume xs == Cons(100, Nil());
+
+  h := head(xs);
+
+  assert [headIs100]: h == 100;
+};
+#end
+
+/-- info: true -/
+#guard_msgs in
+#eval TransM.run Inhabited.default (translateProgram polyListHavocPgm) |>.snd |>.isEmpty
+
+/--
+info:
+Obligation: headIs100
+Property: assert
+Result: ✅ pass
+
+Obligation: TestPolyListHavoc_ensures_0
+Property: assert
+Result: ✅ pass
+-/
+#guard_msgs in
+#eval verify "cvc5" polyListHavocPgm Inhabited.default Options.quiet
+
+---------------------------------------------------------------------
+-- Test 7: Multiple Instantiations with SMT Verification
+---------------------------------------------------------------------
+
+/-- Test SMT verification with List int and List bool in same procedure -/
+def multiInstSMTPgm : Program :=
+#strata
+program Boogie;
+
+datatype List (a : Type) { Nil(), Cons(head: a, tail: List a) };
+
+procedure TestMultiInstSMT() returns ()
+spec {
+  ensures true;
+}
+{
+  var xs : List int;
+  var ys : List bool;
+
+  xs := Nil();
+  ys := Nil();
+  havoc xs;
+  havoc ys;
+
+  assume List..isCons(xs);
+  assume List..isCons(ys);
+
+  assert [bothCons]: List..isCons(xs) == List..isCons(ys);
+};
+#end
+
+/-- info: true -/
+#guard_msgs in
+#eval TransM.run Inhabited.default (translateProgram multiInstSMTPgm) |>.snd |>.isEmpty
+
+/--
+info:
+Obligation: bothCons
+Property: assert
+Result: ✅ pass
+
+Obligation: TestMultiInstSMT_ensures_0
+Property: assert
+Result: ✅ pass
+-/
+#guard_msgs in
+#eval verify "cvc5" multiInstSMTPgm Inhabited.default Options.quiet
+
+end Strata.PolymorphicDatatypeTest
diff --git a/StrataTest/Languages/Boogie/PolymorphicFunctionTest.lean b/StrataTest/Languages/Boogie/PolymorphicFunctionTest.lean
new file mode 100644
index 00000000..dcd8836e
--- /dev/null
+++ b/StrataTest/Languages/Boogie/PolymorphicFunctionTest.lean
@@ -0,0 +1,189 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Boogie.Verifier
+
+/-!
+# Polymorphic Function Integration Tests
+
+Tests polymorphic function declarations in Boogie syntax, including parsing,
+typechecking, and type inference.
+-/
+
+namespace Strata.PolymorphicFunctionTest
+
+---------------------------------------------------------------------
+-- Test 1: Single Type Parameter Function Declaration
+---------------------------------------------------------------------
+
+def singleTypeParamDeclPgm : Program :=
+#strata
+program Boogie;
+
+function identity<a>(x : a) : a;
+
+#end
+
+/--
+info: ok: func identity : ∀[$__ty0]. ((x : $__ty0)) → $__ty0;
+-/
+#guard_msgs in
+#eval Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram singleTypeParamDeclPgm)).fst
+
+---------------------------------------------------------------------
+-- Test 2: Single Type Parameter Function Concrete Instantiation
+---------------------------------------------------------------------
+
+def singleTypeParamIntPgm : Program :=
+#strata
+program Boogie;
+
+function identity<a>(x : a) : a;
+
+procedure TestIdentityInt() returns ()
+spec {
+  ensures true;
+}
+{
+  var x : int;
+  var y : int;
+  x := 42;
+  y := identity(x);
+};
+#end
+
+/-- info: ok: func identity : ∀[$__ty0]. ((x : $__ty0)) → $__ty0;
+(procedure TestIdentityInt :  () → ())
+modifies: []
+preconditions: 
+postconditions: (TestIdentityInt_ensures_0, #true)
+body: init (x : int) := (init_x_0 : int)
+init (y : int) := (init_y_1 : int)
+x := #42
+y := ((~identity : (arrow int int)) (x : int))-/
+#guard_msgs in
+#eval (Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram singleTypeParamIntPgm)).fst)
+
+---------------------------------------------------------------------
+-- Test 3: Multiple Type Parameter Function Used in Expression
+---------------------------------------------------------------------
+
+def multiTypeParamUsePgm : Program :=
+#strata
+program Boogie;
+
+function makePair<a, b>(x : a, y : b) : Map a b;
+
+procedure TestMakePair() returns ()
+spec {
+  ensures true;
+}
+{
+  var m : Map int bool;
+  m := makePair(42, true);
+};
+#end
+
+/-- info: ok: func makePair : ∀[$__ty0, $__ty1]. ((x : $__ty0) (y : $__ty1)) → (Map $__ty0 $__ty1);
+(procedure TestMakePair :  () → ())
+modifies: []
+preconditions: 
+postconditions: (TestMakePair_ensures_0, #true)
+body: init (m : (Map int bool)) := (init_m_0 : (Map int bool))
+m := (((~makePair : (arrow int (arrow bool (Map int bool)))) #42) #true)-/
+#guard_msgs in
+#eval (Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram multiTypeParamUsePgm)).fst)
+
+---------------------------------------------------------------------
+-- Test 4: Polymorphic Function with Arrow Types Used in Expression
+---------------------------------------------------------------------
+
+def arrowTypeParamUsePgm : Program :=
+#strata
+program Boogie;
+
+function apply<a, b>(f : a -> b, x : a) : b;
+function intToBool(x : int) : bool;
+
+procedure TestApply() returns ()
+spec {
+  ensures true;
+}
+{
+  var result : bool;
+  result := apply(intToBool, 42);
+};
+#end
+
+/-- info: ok: func apply : ∀[$__ty0, $__ty1]. ((f : (arrow $__ty0 $__ty1)) (x : $__ty0)) → $__ty1;
+func intToBool :  ((x : int)) → bool;
+(procedure TestApply :  () → ())
+modifies: []
+preconditions: 
+postconditions: (TestApply_ensures_0, #true)
+body: init (result : bool) := (init_result_0 : bool)
+result := (((~apply : (arrow (arrow int bool) (arrow int bool))) (~intToBool : (arrow int bool))) #42)-/
+#guard_msgs in
+#eval (Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram arrowTypeParamUsePgm)).fst)
+
+---------------------------------------------------------------------
+-- Test 5: Different Instantiations in a Single Term
+---------------------------------------------------------------------
+
+def differentInstantiationsPgm : Program :=
+#strata
+program Boogie;
+
+function identity<a>(x : a) : a;
+function makePair<a, b>(x : a, y : b) : Map a b;
+
+procedure TestDifferentInstantiations() returns ()
+spec {
+  ensures true;
+}
+{
+  var m : Map int bool;
+  m := makePair(identity(42), identity(true));
+};
+#end
+
+/-- info: ok: func identity : ∀[$__ty0]. ((x : $__ty0)) → $__ty0;
+func makePair : ∀[$__ty1, $__ty2]. ((x : $__ty1) (y : $__ty2)) → (Map $__ty1 $__ty2);
+(procedure TestDifferentInstantiations :  () → ())
+modifies: []
+preconditions: 
+postconditions: (TestDifferentInstantiations_ensures_0, #true)
+body: init (m : (Map int bool)) := (init_m_0 : (Map int bool))
+m := (((~makePair : (arrow int (arrow bool (Map int bool)))) ((~identity : (arrow int int)) #42)) ((~identity : (arrow bool bool)) #true))-/
+#guard_msgs in
+#eval (Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram differentInstantiationsPgm)).fst)
+
+---------------------------------------------------------------------
+-- Test 6: Negative Test - Type Unification Failure (eq with different types)
+---------------------------------------------------------------------
+
+def eqTypeMismatchPgm : Program :=
+#strata
+program Boogie;
+
+function eq<a>(x : a, y : a) : bool;
+
+procedure TestEqTypeMismatch() returns ()
+spec {
+  ensures true;
+}
+{
+  var result : bool;
+  result := eq(42, true);
+};
+#end
+
+/-- info: error: (0, 0) Impossible to unify (arrow int bool) with (arrow bool $__ty6).
+First mismatch: int with bool.-/
+#guard_msgs in
+#eval (Boogie.typeCheck Options.quiet (TransM.run Inhabited.default (translateProgram eqTypeMismatchPgm)).fst)
+
+end Strata.PolymorphicFunctionTest
diff --git a/docs/verso/DDMDoc.lean b/docs/verso/DDMDoc.lean
index 477cf933..494c00b2 100644
--- a/docs/verso/DDMDoc.lean
+++ b/docs/verso/DDMDoc.lean
@@ -397,6 +397,28 @@ category Statement;
 op varStatement (dl : DeclList) : Statement => "var " dl ";";
 ```
 
+### Polymorphic Type Variables
+
+The `@[scopeTypeVars]` annotation allows polymorphic function declarations
+where type parameters (like `<a, b>`)
+need to be in scope when parsing parameter types and return types.
+For example, function declarations in Strata.Boogie are defined as 
+the following:
+
+```
+category TypeArgs;
+op type_args (args : CommaSepBy Ident) : TypeArgs => "<" args ">";
+
+@[declareFn(name, b, r)]
+op command_fndecl (name : Ident,
+                   typeArgs : Option TypeArgs,
+                   @[scopeTypeVars(typeArgs)] b : Bindings,
+                   @[scopeTypeVars(typeArgs)] r : Type) : Command =>
+  "function " name typeArgs b ":" r ";";
+```
+
+This allows parsing declarations like `function identity<a>(x: a): a`.
+
 ## The `Init` dialect
 %%%
 tag := "init"