diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs
index e2060bc..21037d5 100644
--- a/crates/ailang-check/src/builtins.rs
+++ b/crates/ailang-check/src/builtins.rs
@@ -149,6 +149,68 @@ pub fn install(env: &mut crate::Env) {
         },
     );
 
+    // Iter 22-floats.3: Float-conversion and inspection builtins.
+    // Codegen lowering lands in iter 4; iter 3 only registers types.
+    // `neg` is polymorphic (`forall a. (a) -> a`) for the same reason
+    // the widened `+` is — Int and Float negation share one symbol;
+    // the spec section A3 also notes that `(- 0.0 x)` desugar is
+    // wrong for `-0.0` (returns `+0.0` per IEEE rounding), so Float
+    // negation needs its own builtin name.
+    env.globals.insert(
+        "neg".into(),
+        Type::Forall {
+            vars: vec!["a".into()],
+            constraints: vec![],
+            body: Box::new(Type::Fn {
+                params: vec![Type::Var { name: "a".into() }],
+                ret: Box::new(Type::Var { name: "a".into() }),
+                effects: vec![],
+                param_modes: vec![],
+                ret_mode: ailang_core::ast::ParamMode::Implicit,
+            }),
+        },
+    );
+    env.globals.insert(
+        "int_to_float".into(),
+        Type::Fn {
+            params: vec![Type::int()],
+            ret: Box::new(Type::float()),
+            effects: vec![],
+            param_modes: vec![],
+            ret_mode: ailang_core::ast::ParamMode::Implicit,
+        },
+    );
+    env.globals.insert(
+        "float_to_int_truncate".into(),
+        Type::Fn {
+            params: vec![Type::float()],
+            ret: Box::new(Type::int()),
+            effects: vec![],
+            param_modes: vec![],
+            ret_mode: ailang_core::ast::ParamMode::Implicit,
+        },
+    );
+    env.globals.insert(
+        "float_to_str".into(),
+        Type::Fn {
+            params: vec![Type::float()],
+            ret: Box::new(Type::str_()),
+            effects: vec![],
+            param_modes: vec![],
+            ret_mode: ailang_core::ast::ParamMode::Implicit,
+        },
+    );
+    env.globals.insert(
+        "is_nan".into(),
+        Type::Fn {
+            params: vec![Type::float()],
+            ret: Box::new(Type::bool_()),
+            effects: vec![],
+            param_modes: vec![],
+            ret_mode: ailang_core::ast::ParamMode::Implicit,
+        },
+    );
+
     env.effect_ops.insert(
         "io/print_int".into(),
         EffectOpSig {
@@ -207,6 +269,11 @@ pub fn list() -> Vec<(&'static str, &'static str)> {
         (">=", "forall a. (a, a) -> Bool"),
         ("not", "(Bool) -> Bool"),
         ("__unreachable__", "forall a. a"),
+        ("neg", "forall a. (a) -> a"),
+        ("int_to_float", "(Int) -> Float"),
+        ("float_to_int_truncate", "(Float) -> Int"),
+        ("float_to_str", "(Float) -> Str"),
+        ("is_nan", "(Float) -> Bool"),
         ("io/print_int", "(Int) -> Unit !IO  [effect op]"),
         ("io/print_bool", "(Bool) -> Unit !IO  [effect op]"),
         ("io/print_str", "(Str) -> Unit !IO  [effect op]"),
@@ -309,4 +376,57 @@ mod tests {
         let ty = synth_in_builtins_env(&app("<", vec![lit_float(bits_a), lit_float(bits_b)]));
         assert_eq!(ty, Type::bool_(), "(< 1.5 2.5) must type as Bool");
     }
+
+    /// Iter 22-floats.3: `neg` is polymorphic — `forall a. (a) -> a`.
+    /// Both `(neg 5) : Int` and `(neg 1.5) : Float` typecheck. The
+    /// polymorphic shape is the same as the widened arithmetic ops, so
+    /// Int and Float negation share one symbol; codegen dispatches on
+    /// the resolved arg type at the call site (iter 4).
+    #[test]
+    fn install_neg_is_polymorphic() {
+        let ty_int = synth_in_builtins_env(&app("neg", vec![lit_int(5)]));
+        assert_eq!(ty_int, Type::int(), "(neg 5) must type as Int");
+        let bits = 1.5_f64.to_bits();
+        let ty_float = synth_in_builtins_env(&app("neg", vec![lit_float(bits)]));
+        assert_eq!(ty_float, Type::float(), "(neg 1.5) must type as Float");
+    }
+
+    /// Iter 22-floats.3: `int_to_float : (Int) -> Float`. The
+    /// monomorphic conversion builtin — codegen lowers via `sitofp` in
+    /// iter 4. Typecheck only validates the signature here.
+    #[test]
+    fn install_int_to_float_signature() {
+        let ty = synth_in_builtins_env(&app("int_to_float", vec![lit_int(5)]));
+        assert_eq!(ty, Type::float(), "(int_to_float 5) must type as Float");
+    }
+
+    /// Iter 22-floats.3: `float_to_int_truncate : (Float) -> Int`.
+    /// Saturating truncation toward zero per spec A4 — typecheck only
+    /// validates the signature; semantics is iter 4's codegen lowering
+    /// via `@llvm.fptosi.sat.i64.f64`.
+    #[test]
+    fn install_float_to_int_truncate_signature() {
+        let bits = 1.5_f64.to_bits();
+        let ty = synth_in_builtins_env(&app("float_to_int_truncate", vec![lit_float(bits)]));
+        assert_eq!(ty, Type::int(), "(float_to_int_truncate 1.5) must type as Int");
+    }
+
+    /// Iter 22-floats.3: `float_to_str : (Float) -> Str`. Codegen lowers
+    /// via runtime C glue in iter 4; typecheck only validates the signature.
+    #[test]
+    fn install_float_to_str_signature() {
+        let bits = 1.5_f64.to_bits();
+        let ty = synth_in_builtins_env(&app("float_to_str", vec![lit_float(bits)]));
+        assert_eq!(ty, Type::str_(), "(float_to_str 1.5) must type as Str");
+    }
+
+    /// Iter 22-floats.3: `is_nan : (Float) -> Bool`. Codegen lowers to
+    /// `fcmp uno double %x, %x` in iter 4 — typecheck only validates
+    /// the signature here.
+    #[test]
+    fn install_is_nan_signature() {
+        let bits = 1.5_f64.to_bits();
+        let ty = synth_in_builtins_env(&app("is_nan", vec![lit_float(bits)]));
+        assert_eq!(ty, Type::bool_(), "(is_nan 1.5) must type as Bool");
+    }
 }
diff --git a/crates/ailang-codegen/src/synth.rs b/crates/ailang-codegen/src/synth.rs
index ad0c092..ef338a5 100644
--- a/crates/ailang-codegen/src/synth.rs
+++ b/crates/ailang-codegen/src/synth.rs
@@ -136,6 +136,47 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
             constraints: vec![],
             body: Box::new(Type::Var { name: "a".into() }),
         },
+        // Iter 22-floats.3: Float-conversion and inspection builtins.
+        // Same lockstep with `crates/ailang-check/src/builtins.rs`.
+        "neg" => Type::Forall {
+            vars: vec!["a".into()],
+            constraints: vec![],
+            body: Box::new(Type::Fn {
+                params: vec![Type::Var { name: "a".into() }],
+                ret: Box::new(Type::Var { name: "a".into() }),
+                effects: vec![],
+                param_modes: vec![],
+                ret_mode: ParamMode::Implicit,
+            }),
+        },
+        "int_to_float" => Type::Fn {
+            params: vec![Type::int()],
+            ret: Box::new(Type::float()),
+            effects: vec![],
+            param_modes: vec![],
+            ret_mode: ParamMode::Implicit,
+        },
+        "float_to_int_truncate" => Type::Fn {
+            params: vec![Type::float()],
+            ret: Box::new(Type::int()),
+            effects: vec![],
+            param_modes: vec![],
+            ret_mode: ParamMode::Implicit,
+        },
+        "float_to_str" => Type::Fn {
+            params: vec![Type::float()],
+            ret: Box::new(Type::str_()),
+            effects: vec![],
+            param_modes: vec![],
+            ret_mode: ParamMode::Implicit,
+        },
+        "is_nan" => Type::Fn {
+            params: vec![Type::float()],
+            ret: Box::new(Type::bool_()),
+            effects: vec![],
+            param_modes: vec![],
+            ret_mode: ParamMode::Implicit,
+        },
         _ => return None,
     })
 }