On propose une notion de modèle pour la logique intuitionniste, qui étend celle fondée sur les algèbre de Heyting. Cette notion de modèle permet de distinguer l'équivalence logique (si A est démontrable, alors B aussi, et vice-versa) de l'équivalence calculatoire (toute démonstration de A est une démonstration de B, et vice-versa), ce que ne permettaient pas de faire les algèbres de Heyting. On montre ensuite que cette notion de modèle peut être utilisée pour démontrer la normalisation des démonstrations dans de nombreuses théories comme l'arithmétique de Peano ou la logique d'ordre supérieur.