Les calculs de substitutions explicites comme fondement des implantations des langages fonctionnels - Université de Lorraine Accéder directement au contenu
Thèse Année : 1997

Explicit substitution calculi as a foundation of functional programming languages implementations

Les calculs de substitutions explicites comme fondement des implantations des langages fonctionnels

Résumé

Non disponible / Not available
Les langages de programmation fonctionnels font partie des langages de très haut niveau. Ils peuvent être vus comme des extensions ou des variantes du lambda-calcul, un formalisme mathématique puissant qui a donné lieu à d'innombrables travaux durant les vingt dernières années. Ils bénéficient de ce fait assez directement, pour la définition de leur sémantique, du riche corps de doctrine qui a été constitué autour de celui-ci. Si ce formalisme, au départ simple, donne lieu à tant de variations, c'est en particulier à des fins d'implantation. Notamment, au travers de la béta-réduction (une opération fondamentale du lambda-calcul) différentes stratégies d'évaluation peuvent être définies : elles constituent autant de spécifications possibles pour les implantations de ces langages. La béta-réduction est une opération complexe comparée aux instructions machines utilisées pour la mettre en oeuvre et, de ce fait, il existe un fossé assez important entre la spécification d'une stratégie d'évaluation et sa réalisation. En conséquence, les preuves de corrections des implantations de langages fonctionnels restent limitées, rendant difficile les comparaisons formelles entre les différentes implantations. Les calculs de substitutions explicites, introduits par Curien, remplacent l'opération de substitution intervenant dans la béta-réduction par des opérations plus élémentaires. Ces calculs décomposent la béta-réduction en une règle de déclenchement de la substitution et un ensemble de règles de propagation de cette substitution. Ces règles de propagation ont un grain fin qui rapprochent la béta-réduction des instructions qui l'implantent. L'introduction de ces calculs a ouvert une voie nouvelle de recherche d'un formalisme mieux adapté à la description unifiée de sémantique, de stratégie d'évaluation et d'implantations associées. [...]
Fichier non déposé

Dates et versions

tel-01747439 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01747439 , version 1

Accès intranet

Citer

Zine-Ei-Abidine Benaissa. Les calculs de substitutions explicites comme fondement des implantations des langages fonctionnels. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 1997. Français. ⟨NNT : 1997NAN10173⟩. ⟨tel-01747439⟩
16 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More