Sahlqvist Correspondence for Intuitionistic Modal Mu-Calculus Yves Fomatati Abstract: The motivation of this thesis is the idea of extending the results in [13] to the case of logics with fixpoints and with a non-classical base. We focus in particular on the intuitionistic modal mu-calculus. We enhance the ALBA algorithm [26] for the elimination of monadic second order variables so that mu-formulas can be treated in which all the variables occur inside the scope of fixpoint binders. We prove that this enhancement is sound thanks to the order-theoretic properties of the interpretation of fixpoint binders in the algebraic semantics for intuitionistic mu-calculus. We define the class of recursive inequalities and informally justify that the enhanced ALBA is successful on this class.