• Plan des 4 prochains cours

Partie: I
Les principes du typage

• Plan
• Introduction I
  • Le typage
  • Intérêts du typage statique
• Introduction II
  • Remarque
  • Qu'est qu'un type?
  • Typer une expression
• Introduction III
  • Vérification des types
  • Synthèse des types
• Introduction IV
  • Vérification
  • Synthèse
  • Intérêts de la synthèse
• Quelques exemples I
  • Typer une expression:
  • Exemple:
• Quelques exemples II
• Quelques exemples III
  • Typer:
  • Question:
• Notations, définitions I
  • L'environnement de typage
  • Notre langage des types
• Le typage de CAML I
  • Constantes
  • Identificateurs
  • Conditionnelle
• Le typage de CAML II
  • Application de fonction
  • Exemples:
  • Remarque:
• Le typage de CAML III
  • Fonctions: function x -> corps
• Le typage de CAML IV
  • Déclarations globales
• Le typage de CAML V
  • Déclarations locales
• Le typage de CAML VI
  • Fonctions récursives
  • Typage dans Env
• Le typage de CAML VII
  • Polymorphisme
  • Intérêt du polymorphisme
• Le typage de CAML VIII
  • Schéma de type:
  • Type:
  • Type monomorphe:
  • Type polymorphe:
  • Instancier un schéma de type:
  • Généraliser un type dans Env:
• Le typage de CAML IX
  • Typage d'une expression ne contenant que des identificateurs connus
• Le typage de CAML X
  • Exemple
• Le typage de CAML XI
  • Quand et comment généraliser ?
  • Expression expansive:
• Le typage de CAML XII
  • La généralisation
  • Déclarations globales:
  • Exemple
• Modularité I
  • Un exemple
• Modularité II
• Modularité III
• Modularité IV
  • Structure d'un environnement complet
• Environnement initial EInit
• Modularité V
  • Construire un environnement par importation
• A FAIRE
• Traits impératifs I
• Traits impératifs II
  • Référence
  • Affectation
  • Séquence
  • Exceptions
• Un algorithme d'unification entre types
  • Un langage de types:
  • Substitution:
  • Unification:
• Un algorithme d'unification entre types
• Conclusion
  • Extensions

Partie: II
Les types de données

• Plan
• Introduction
• Types de base
• Produit Cartésien I
  • Produit cartésien d'ensembles:
  • Projections:
  • Produit cartésien de deux types:
  • Produit cartésien de n types:
  • Attention:
  • Projections à définir par l'utilisateur
• Produit cartésien II
  • Paires
  • N-uplets
  • Définitions par cas: filtrage
• Type Enregistrement I
  • Constructeur de type
  • Constructeur de valeur
  • Notation pointée
• Enregistrements III
  • Masquage
  • Règle de typage
• Types somme I
  • Union disjointe d'ensembles:
  • Injection canonique
• Types somme II
  • Syntaxe:
  • Convention:
  • Prise en compte de la définition
  • Règle de typage
• Types somme III
  • Filtrage - Somme
• Types somme IV
• Types somme IV
  • Typage des fonction définies par filtrage
  • Un cas
  • Plusieurs cas
• Types récursifs II
• Conclusion
  • Questions

Ce document a été traduit de L^AT_EX par H^EV^EA et H^AC^HA.