Research on humanoid robots has made significant progress in recent years, and Model Predictive Control (MPC) has seen great applicability as a technique for gait generation. The main advantages of MPC are the possibility of enforcing constraints on state and inputs, and the constant replanning which grants a degree of robustness. This thesis describes a framework based on MPC for humanoid gait generation, and analyzes some theoretical aspects which have often been neglected. In particular, the stability of the controller is proved. Due to the presence of constraints, this requires proving recursive feasibility, i.e., that the algorithm is able to recursively guarantee that a solution satisfying the constraints is found. The scheme is referred to as Intrinsically Stable MPC (IS-MPC). A basic scheme is presented, and its stability and feasibility guarantees are discussed. Then, several extensions are introduced. The guarantees of the basic scheme are carried over to a robust version of IS-MPC. Furthermore, extension to uneven ground and to a more accurate multi-mass model are discussed. Experiments on two robotic platforms (the humanoid robots HRP-4 and NAO) are presented in the concluding section.