Ce cours présente les principales méthodes formelles sur lesquelles est basée la certification de code. Syntaxe et sémantiques des langages à travers le lambda-calcul et ses extensions. Logiques classique et intuitionniste. Logique de Hoare et logique d'ordre supérieur. Correspondance entre calcul et logique. Assistant de preuves Coq.
Ce cours présente les principales méthodes formelles sur lesquelles est basée la certification de code. Syntaxe et sémantiques des langages à travers le lambda-calcul et ses extensions. Logiques classique et intuitionniste. Logique de Hoare et logique d'ordre supérieur. Correspondance entre calcul et logique. Assistant de preuves Coq.
