diff --git a/src/CPS.ml b/src/CPS.ml
index 3ec1577..bab67e6 100644
--- a/src/CPS.ml
+++ b/src/CPS.ml
@@ -69,9 +69,13 @@ let rec cps_term_inner (t: S.term) (cont: T.variable) (nameHint: string option)
         let curCont = freshBlockVar () in
         letCont curCont var (cps_term_inner next cont None) @@
         cps_term_inner value curCont (Some (Atom.hint var))
-| S.IfZero _ ->
-        (* TODO ifzero *)
-        assert false
+| S.IfZero (expr, tIf, tElse) ->
+        let curCont = freshBlockVar ()
+        and exprVal = freshVar () in
+        letCont curCont exprVal (T.IfZero(T.vvar exprVal,
+                cps_term_inner tIf cont None,
+                cps_term_inner tElse cont None)) @@
+            cps_term_inner expr curCont None
 
 let cps_term (t: S.term): T.term =
     (** Entry point. Transforms a [Lambda] term into a [Tail] term, applying a
diff --git a/src/Defun.ml b/src/Defun.ml
index bb00d15..13484fb 100644
--- a/src/Defun.ml
+++ b/src/Defun.ml
@@ -86,9 +86,10 @@ let rec walk_term fs t =
                 T.Branch(thisTag, freeVars, nBody) in
             let fs = add_func fs arity thisFunc in
             fs, T.LetBlo (var, T.Con(thisTag, T.vvars freeVars), nNext)
-    | S.IfZero _ ->
-            (* TODO ifzero *)
-            assert false
+    | S.IfZero (value, tIf, tElse) ->
+            let fs, tIf = walk_term fs tIf in
+            let fs, tElse = walk_term fs tElse in
+            fs, T.IfZero(value, tIf, tElse)
 
 
 let apply_of_arity name args branches =
diff --git a/src/Finish.ml b/src/Finish.ml
index ecf4b17..9bd6ff5 100644
--- a/src/Finish.ml
+++ b/src/Finish.ml
@@ -228,9 +228,11 @@ let rec finish_term (t : S.term) : C.stmt =
         init_block x b1 @
         [ finish_term t2 ]
       )
-  | S.IfZero _ ->
-      (* TODO ifzero *)
-      assert false
+  | S.IfZero (expr, tIf, tElse) ->
+      T.IfElse (
+        finish_value expr,
+        finish_term tIf,
+        finish_term tElse)
   | S.Swi (v, bs) ->
       T.Switch (
         read_tag v,
diff --git a/src/Tail.ml b/src/Tail.ml
index 789023e..eb2e8f9 100644
--- a/src/Tail.ml
+++ b/src/Tail.ml
@@ -131,6 +131,7 @@ and fv_term (t : term) =
       union
         (fv_block b1)
         (remove x (fv_term t2))
-  | IfZero _ ->
-      (* TODO ifzero *)
-      assert false
+  | IfZero (cond, tIf, tElse) ->
+      union
+        (fv_value cond)
+        (union (fv_term tIf) (fv_term tElse))
diff --git a/src/prettify/PrettyTail.ml b/src/prettify/PrettyTail.ml
index 92ebf66..bcc3011 100644
--- a/src/prettify/PrettyTail.ml
+++ b/src/prettify/PrettyTail.ml
@@ -21,9 +21,11 @@ and fmt_term fmt (t: S.term) = match t with
 | S.LetBlo (var, block, next) ->
         Format.fprintf fmt "@[<v 4>let %a = %a@] in@ %a"
             fmt_var var fmt_block block fmt_term next
-| S.IfZero _ ->
-        (* TODO ifzero *)
-        assert false
+| S.IfZero (cond, tIf, tElse) ->
+        Format.fprintf fmt "@[<v 4>ifzero %a then@ %a@]@ @[<v 4>else@ %a@]@ "
+            fmt_val cond
+            fmt_term tIf
+            fmt_term tElse
 
 let show term =
     Format.asprintf "@[<v 0>%a@]" fmt_term term
diff --git a/src/prettify/PrettyTop.ml b/src/prettify/PrettyTop.ml
index 4975e43..9844ec0 100644
--- a/src/prettify/PrettyTop.ml
+++ b/src/prettify/PrettyTop.ml
@@ -28,9 +28,11 @@ let rec fmt_term fmt (term: S.term) = match term with
             fmt_var name
             fmt_block block
             fmt_term next
-| S.IfZero _ ->
-        (* TODO ifzero *)
-        assert false
+| S.IfZero (cond, tIf, tElse) ->
+        Format.fprintf fmt "@[<v 4>ifzero %a then@ %a@]@ @[<v 4>else@ %a@]"
+            fmt_val cond
+            fmt_term tIf
+            fmt_term tElse
 | S.Swi (value, branches) ->
         Format.fprintf fmt "@[<v 4>switch(%a)" fmt_val value ;
         List.iter