Résumé
Ce séminaire a approfondi la technique de forcing de Cohen et l’analyse de son contenu calculatoire abordées dans le septième cours. Le conférencier a ensuite expliqué la théorie de la réalisabilité, une méthode de construction de modèles de la logique formalisant et étendant l’interprétation BHK, et montré ses liens formels avec le forcing : la réalisabilité peut être vue comme un forcing non commutatif. Poursuivant cette unification, il a introduit la notion d’algèbre implicative, une structure qui représente uniformément programmes et types, réalisateurs et formules logiques.
