Nous examinons les propriétés de sécurité du lambda-calcul au travers du prisme du lambda-calcul étiqueté. Les étiquettes expriment dynamiquement la dépendance des termes présents vis-à-vis des réductions passées. Nous montrons que le lambda-calcul étiqueté vérifie la propriété d'irréversibilité des contextes: une fois qu'un contexte est intervenu dans une réduction, il disparaît irréversiblement dans la suite de cette réduction. Nous examinons les propriétés fondamentales de variantes du lambda-calcul étiqueté. Pour cela, nous introduisons une preuve élégante du théorème des développements finis dans la cadre du lambda-calcul par valeur étiqueté. Puis nous prouvons que les étiquettes du lambda-calcul faible expriment le partage. Les étiquettes du lam! bda-calcul permettent d'exprimer des politiques de sécurité telles que l'inspection de pile et la Muraille de Chine. Nous définissons la notion de réduction indépendante de deux principaux A et B: une telle réduction peut se décomposer en deux réductions: une réduction qui ignore A et une réduction qui ignore B. Nous prouvons que la Muraille de Chine garantit cette propriété d'indépendance. Les étiquettes du lambda-calcul permettent aussi d'exprimer la propriété d'interférence: il s'agit ici d'identifier les sous-termes d'un terme M qui influencent le résultat de la réduction de M. Dans le lambda-calcul muni de références, en plus de l'interférence fonctionnelle déjà présente dans le lambda-calcul pur, on identifie l'interférence de mémoire due à l'utilisation des référe! nces. Les étiquettes permettent d'identifier les int! ervalles de temps pendant lesquels une référence influence le résultat d'une réduction.
| Identifer | oai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00002090 |
| Date | 07 November 2006 |
| Creators | Blanc, Tomasz |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0019 seconds