Je présente un lambda calcul codant une logique intuitionniste du second ordre et permettant de programmer un ou-parallèle''. Ce calcul a les propriétés suivantes :préservation de type'', forte normalisation'' etunicité de représentation des données''. Il permet aussi d'écrire des programmes avec une sorte d'exception. Il est inspire du lambda-mu-{++}-calcul que j'ai introduit en 2002.