Types, Spécifications et Preuves

Informations

Langue d'enseignement : Anglais
Crédits ECTS: 3

Programme

  • Heures d'enseignement dispensées à l'étudiant : 24 heures
  • Temps de travail personnel : 51 heures

Objectifs et compétences

Objectifs :
Les systèmes de types suffisamment puissants permettent d'exprimer la spécification de programmes. La preuve de correction de ces programmes s'apparente alors à une vérification de types. Ces techniques seront illustrées dans le cadre de la programmation fonctionnelle.

----

Type systems, when they are powerful enough, can express precise program specifications. As a result, correctness proofs of these programs can be implemented by type checking. These techniques will be illustrated within the functional programming framework.

Compétences :
  • Comprendre et mettre en oeuvre l'intérêt et les principes de la démarche de recherche fondamentale et/ou appliquée
  • Savoir se remettre en question, faire preuve d'esprit critique
  • Construire et développer une argumentation.

  • Connaître et mettre en application les principaux modèles mathématiques intervenant dans les différentes disciplines connexes du domaine Sciences et Technologies mais aussi des autres domaines
  • Maîtriser les bases de la logique et organiser un raisonnement mathématique.
  • Construire et rédiger une démonstration mathématique synthétique et rigoureuse.
  • Être capable de traduire un problème simple en langage mathématique.
  • Connaître les principaux paradigmes de programmation et sélectionner un langage adapté à une situation donnée
  • Modéliser une situation concrète en un énoncé formel au moyen d'outils (e.g., automates, langages, grammaires, graphes)
  • Comprendre une preuve de correction d'algorithme (e.g., variants/invariants, induction, convergence)
  • Ecrire une preuve de correction d'algorithme

Organisation pédagogique

le mode de fonctionnement de l'UE est présenté au début des enseignements

Contrôle des connaissances

Évaluation par projet : développement, rapport et soutenance orale (controle continu integral), coeff. 1

Pas de session 2

Lectures recommandées

l'ensemble des références bibliographiques est communiqué au début des enseignements

Responsable de l'unité d'enseignement

Pierre Casteran

Enseignants

la composition de l'ensemble de l'équipe pédagogique est communiquée au début des enseignements