En sémantique des langages, l'équivalence contextuelle de programmes est une notion clef, mais sa définition se prête mal à la manipulation, on cherche donc des modèles corrects et complets lui donnant une expression plus pratique. Les jeux et la sémantique interactive sont de tels modèles, applicables à beaucoup de langages et donnant une équivalence coïnductivement définie. Dans cette présentation je vais esquisser visuellement et de manière intuitive un formalisme de jeux général qui se prête bien à la formalisation dans un assistant de preuve. Je vais également décrire différents genres d'arbres inductifs et coïnductifs ainsi qu'une manière pratique de construire des jeux à partir de composants plus élémentaires.