Résumé
Le premier séminaire a consisté en une défense et illustration de la programmation avec types dépendants dans le langage Agda. Le conférencier est parti d’un problème classique : la sémantique d’un langage d’expressions arithmétiques et sa compilation vers le code d’une machine à pile. Il a montré que de nombreux cas d’erreurs sont à traiter si on n’emploie que des types simples, mais disparaissent si on indexe les expressions et les instructions de la machine par les types des valeurs produites. Cela garantit par construction que le compilateur préserve les types. Les instructions peuvent aussi être indexées par leur sémantique opérationnelle, ce qui garantit par construction que le compilateur est correct (préserve la sémantique), atteignant ainsi un point extrême de la programmation à types dépendants.
