Normal view MARC view ISBD view

Compilation des langages fonctionnels dans les combinateurs catégoriques [Texte imprimé] : application au langage ML / Michel Mauny

Auteur principal : Mauny, Michel, AuteurAuteur secondaire collectivité : Université Paris Diderot - Paris 7, 1970-2019, Organisme de soutenancePublication :[S.l.] : [s.n.], 1985Description : 1 vol. (132 p.) ; 30 cmRésumé : Cette thèse décrit une technique de compilation des langages fonctionnels qui repose sur une machine abstraite d'un type nouveau, appelée Machine Abstraite Catégorique, définie en collaboration avec G. Cousineau et P-L. Curien. Le code de cette machine est principalement constitué des termes du 1er ordre construits à partir des combinateurs catégoriques de Berry et Curien. Le processus de compilation peut donc être en partie assimilé au processus de traduction du lambda-calcul dans les termes catégoriques. Cette caractéristique permet de faire lde façon simple la preuve de correction des différents types de compilation proposés. Ces preuves de correction constituent l'essentiel de cette thèse. Des spécifications d'appel par valeur et d'évaluation paresseuse dans le lambda-calcul ainsi que dans le calcul catégorique sont données, utilisant le formalisme de Plotkin : des systèmes d'inférence donnent à chaque fois la sémantique opérationnelle du langage considéré. On décrit formellement la compilation dans la CAM du noyau purement fonctionnel du langage ML soumis tant à un appel par valeur qu'à une évaluation paresseuse. De plus, la CAM est montrée aisément extensible par l'adjonction d'un mécanisme de gestion d'échappements.Bibliographie: Bibliogr. p. 115-117.Thèse : .Sujet - Nom d'actualité : Lambda-calcul -- Thèses et écrits académiques ;Réécriture, Systèmes de (informatique) -- Thèses et écrits académiques ;Langages de programmation fonctionnelle -- Thèses et écrits académiques Sujet : LANGAGE ML ;COMPILATION
Current location Call number Status Date due Barcode
Centre de recherche en informatique
1985 MAU Sur demande CRI04382D

Bibliogr. p. 115-117

Thèse de 3e cycle Mathématiques Paris 7 1985

Cette thèse décrit une technique de compilation des langages fonctionnels qui repose sur une machine abstraite d'un type nouveau, appelée Machine Abstraite Catégorique, définie en collaboration avec G. Cousineau et P-L. Curien. Le code de cette machine est principalement constitué des termes du 1er ordre construits à partir des combinateurs catégoriques de Berry et Curien. Le processus de compilation peut donc être en partie assimilé au processus de traduction du lambda-calcul dans les termes catégoriques. Cette caractéristique permet de faire lde façon simple la preuve de correction des différents types de compilation proposés. Ces preuves de correction constituent l'essentiel de cette thèse. Des spécifications d'appel par valeur et d'évaluation paresseuse dans le lambda-calcul ainsi que dans le calcul catégorique sont données, utilisant le formalisme de Plotkin : des systèmes d'inférence donnent à chaque fois la sémantique opérationnelle du langage considéré. On décrit formellement la compilation dans la CAM du noyau purement fonctionnel du langage ML soumis tant à un appel par valeur qu'à une évaluation paresseuse. De plus, la CAM est montrée aisément extensible par l'adjonction d'un mécanisme de gestion d'échappements

Powered by Koha