Dans ce cours, nous apprenons les bases du raisonnement formel sur les programmes avec l’assistant de preuve Rocq. Nous spécifions formellement les langages de programmation, c’est-à-dire leur syntaxe et leur sémantique opérationnelle. Nous formulons également des spécifications de programmes et prouvons que les programmes donnés satisfont à ces spécifications.
Ce cours s'appuie sur la série Software Foundations.
