J'exposerai mes idées pour une nouvelle sorte de théorème prouveur, basé sur les idées suivantes: - on crée le langage de programmation avec un système de typage statique fort le plus fort possible - on étend ce langage pour en faire une logique (on n'ajoute pas la logique au dessus du langage) Le but de ce séminaire sera de démarrer un éventuel groupe de travail ...