Depuis l'an dernier, Xavier Leroy est le nouveau titulaire de la chaire « sciences du logiciel » au Collège de France. J'en avais fait un journal pour présenter le thème de sa première année de cours où il abordait la correspondance entre programmes et démonstrations mathématiques, connue sous le nom de correspondance de Curry-Howard.
Cette année, il a décidé d'aborder la formalisation de la sémantique des langages de programmation avec l'aide de la machine (en utilisant l'assistant de (…)