Résumé
Dans le premier séminaire, le conférencier a partagé son expérience d’utilisation d’assistants à la démonstration pour enseigner les fondations des langages de programmation. Initialement, il a utilisé Software Foundations, le cours interactif en Coq de Benjamin Pierce et coauteurs. Insatisfait par la présentation des démonstrations, il a développé son propre cours, Programming Language Foundations in Agda, qui formalise le lambda-calcul simplement typé avec une syntaxe intrinsèquement typée et des démonstrations explicites sous forme de fonctions exécutables. Ainsi, la démonstration de la propriété de progression donne directement un évaluateur pour le langage. Une extension de l’approche au système F est en cours de développement dans le cadre du langage Plutus de smart contracts.
