1   Introduction

2   Rappels fondamentaux, I

Induction
mathématique et complète

Relations bien fondées
définitions et exemples

Principe d'induction bien fondée
et preuve

Composition de relations bien fondées
lexicographique, produit etc.

3   Rappels fondamentaux, II

Réécriture
notion de relation de Réécriture abstraite,

Propriétés des systèmes de réécriture abstraits
confluence faible, confluence, confluence forte, normalisation faible et normalisation forte.

Propositions
Lemme de Newman (confluence faible + normalisation forte implique confluence), prouvé par induction bien fondée

Egalite engendree par une relation de réécriture
propriété de Church-Rosser, et équivalence avec la confluence.

Introduction au lambda calcul
lamda termes, substitution, notion de reduction b et d'égalité b

4   Lamda calcul non typé

Confluence du lambda calcul
preuve par le biais de la technique des reductions parallèles

5   Lambda calcul typé

Définitions de base
type, jugement de typage, derivation de typage

Propriétés
unicité de la derivation de typage, decidabilité de la typabilité,

Subject Reduction
preuve par induction sur la derivation de typage

Inférence de type
esquisse de la methode de reconstruction de type par resolution d'équations engendrées sur les noeuds de la squelette de l'arbre de derivation

6   Réductibilité, Relations logiques

Normalisation forte du lambda calcul simplement typé
par la méthode dite de réductibilité, qui utilise des relations logiques.

7   Sémantique Opérationnelle

Généralités
sur la Sémantique operationnelle structurée (SOS, ou à la Plotkin, ou des petits pas, ou small steps), et sur la Sémantique opérationnelle naturelle (à la Khan, big steps ou des grands pas)

Exemple
évaluation des nombres binaires

Sémantique du lambda calcul
appel par nom et par valeur, en style SOS et naturel, avec définition de la notion de valeur (les abstractions)

Propriétés
determinisme, correspondence entre SOS et naturelle, heritage des propriétés de subject reduction et de normalisation forte de la version typée

8   Machines à environnement pour l'appel par nom

evaluateur simple
critique de l'opération de substitution

machine de Krivine
: notion de fermeture (Closure), environnement et pile; définition d'état (c,e,s) et de la table de transition

propriétés
: définition de depliage d'une fermeture et de relecture d'un état.

théorème
si (c,e,s) transite sur (c',e',s'), alors les relectures sont b équivalentes.

raffinement du théorème
si (c,e,s) transite sur (c',e',s'), alors soit les relectures sont identiques, soit la prémière reduit en une étape b sur la deuxième

raffinement ultérieure
l'eventuelle étape b est bien une étape de reduction en appel par nom. Ceci donne enfin une partie de la correction de la machine.

This document was translated from LATEX by HEVEA.