
It is a consequence of existing literature that least and greatest fixedpoints of monotone polynomials on Heyting algebrasthat is, the algebraic models of the Intuitionistic Propositional Calculusalways exist, even when these algebras are not complete as lattices. The reason is that these extremal fixedpoints are definable by formulas of the IPC. Consequently, the $\mu$calculus based on intuitionistic logic is trivial, every $\mu$formula being equivalent to a fixedpoint free formula. We give in this paper an axiomatization of least and greatest fixedpoints of formulas, and an algorithm to compute a fixedpoint free formula equivalent to a given $\mu$formula. The axiomatization of the greatest fixedpoint is simple. The axiomatization of the least fixedpoint is more complex, in particular every monotone formula converges to its least fixedpoint by Kleene's iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. We extract, out of the algorithm, upper bounds for such n, depending on the size of the formula. For some formulas, we show that these upper bounds are polynomial and optimal.