Notes du cours de DEA : Typage et programmation

Notes du cours de DEA\Typage et programmation"Xavier LeroyXavier.Leroy@inria.frVersion du December 13, 2001http://pauillac.inria.fr/~xleroy/dea/Contents1 Mini-ML: evaluation et typage 41.1 Syntaxe de mini-ML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41.2 Evaluation de mini-ML: semantique operationnelle a\ grands pas" . . . . . . . . . . 51.2.1 Les valeurs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51.2.2 Rappels sur les regles d’inferences . . . . . . . . . . . . . . . . . . . . . . . . 61.2.3 Les regles d’evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71.2.4 Determinisme de l’evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . 81.3 Typage de mini-ML . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101.3.1 L’algebre de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101.3.2 Les regles de typage { typage monomorphe . . . . . . . . . . . . . . . . . . . 111.3.3 Schemas de types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 121.3.4 Les regles de typage { typage polymorphe a la ML . . . . . . . . . . . . . . . 131.3.5 Quelques proprietes des regles de typage . . . . . . . . . . . . . . . . . . . . . 142 Suret^ e du typage et semantique a reduction 162.1 Distinguer erreurs d’execution et non-terminaison . . . . . . . . . . . . . . . . . . . . 162.1.1 Tout programme ...