Partagez sur
STAGE Implémentation, optimisation et tests d'une traduction de programme
Date de mise à jour de l’offre
Etablissement public à caractère scientifique, culturel et professionnel :
École Normale supérieur paris-saclay - DIM RFSI
Description de la mission
Contexte :
Le système T est un langage de programmation abstrait muni de types fonctionnels de tout ordre, basés sur le
type des entiers. Le système F [1] est une extension du système T par des types polymorphes paramétriques.
La récursion barrée [2] est une autre extension du système T par un opérateur de récursion sur des arbres
implicitement bien fondés.
D'un point de vue logique, le système T permet d'interpréter l'arithmétique du premier ordre, alors que
ses extensions que sont le système F et la récursion barrée permettent toutes deux d'interpréter l'arithmétique
du second ordre.
Bien que ces deux interprétations calculatoires de l'arithmétique du second ordre fournissent des programmes
au comportement fondamentalement différent, j'ai pu définir en 2017 une traduction du système F
vers la récursion barrée. Cette traduction remplace donc les types polymorphes par des appels à un opérateur
de récursion.
Afin de mieux comparer les comportements calculatoires des programmes source et cible de cette traduction,
il est nécessaire d'implémenter celle-ci.
Le système T est un langage de programmation abstrait muni de types fonctionnels de tout ordre, basés sur le
type des entiers. Le système F [1] est une extension du système T par des types polymorphes paramétriques.
La récursion barrée [2] est une autre extension du système T par un opérateur de récursion sur des arbres
implicitement bien fondés.
D'un point de vue logique, le système T permet d'interpréter l'arithmétique du premier ordre, alors que
ses extensions que sont le système F et la récursion barrée permettent toutes deux d'interpréter l'arithmétique
du second ordre.
Bien que ces deux interprétations calculatoires de l'arithmétique du second ordre fournissent des programmes
au comportement fondamentalement différent, j'ai pu définir en 2017 une traduction du système F
vers la récursion barrée. Cette traduction remplace donc les types polymorphes par des appels à un opérateur
de récursion.
Afin de mieux comparer les comportements calculatoires des programmes source et cible de cette traduction,
il est nécessaire d'implémenter celle-ci.
Profil recherché
Objectifs du stage :
L'objectif de ce stage est d'implémenter cette traduction à partir d'une définition sur papier déjà existante.
Une fois cette implémentation effectuée, il faudra la tester sur des programmes simples du système F. Afin
de pousser plus loin ces tests, il pourra être nécessaire d'optimiser la traduction.
Prérequis du stage :
Le stagiaire devra avoir une bonne expérience de la programmation fonctionnelle et un intérêt pour la logique
mathématique et l'informatique théorique.
L'objectif de ce stage est d'implémenter cette traduction à partir d'une définition sur papier déjà existante.
Une fois cette implémentation effectuée, il faudra la tester sur des programmes simples du système F. Afin
de pousser plus loin ces tests, il pourra être nécessaire d'optimiser la traduction.
Prérequis du stage :
Le stagiaire devra avoir une bonne expérience de la programmation fonctionnelle et un intérêt pour la logique
mathématique et l'informatique théorique.
Niveau de qualification requis
Bac + 4/5 et +
Les offres de stage ou de contrat sont définies par les recruteurs eux-mêmes.
En sa qualité d’hébergeur dans le cadre du dispositif des « 100 000 stages », la Région Île-de-France est soumise à un régime de responsabilité atténuée prévu aux articles 6.I.2 et suivants de la loi n°2204-575 du 21 juin 2004 sur la confiance dans l’économie numérique.
La Région Île-de-France ne saurait être tenue responsable du contenu des offres.
Néanmoins, si vous détectez une offre frauduleuse, abusive ou discriminatoire vous pouvez la signaler
en cliquant sur ce lien.
-
EmployeurEtablissement public à caractère scientifique, culturel et professionnel
-
Secteur d’activité de la structureEnseignement - Formation - Recherche
-
Effectif de la structurePlus de 250 salariés
-
Site internet de la structurehttps://ens-paris-saclay.fr
-
Type de stage ou contratStage pour lycéens et étudiants en formation initiale
-
Date prévisionnelle de démarrage
-
Durée du stage ou contrat2 mois
-
Le stage est-il rémunéré ?Non
-
Niveau de qualification requis
Bac + 4/5 et + -
Lieu du stageEcole Normale Superieure Paris-Saclay
4 Avenue des Sciences
91190 GIF SUR YVETTE -
Accès et transportsRER B : Arrêt Bagneux