Stages M2 langages de programmation

November 30, 2009 § 1 Comment

Mise-à-jour:

Merci pour toutes les (très bonnes) candidatures aux stages que nous avons proposé. Tous les stages ont été pris.

À bientôt pour la prochaine version d’OPA.

L’entreprise MLstate développe OPA, une plate-forme de développement web fondée sur l’état de l’art de la Recherche en langages de programmation, parallélisme, distribution, sécurité et bases de données. Pour l’année 2009-2010, MLstate propose autour d’OPA plusieurs stages de Master 2 informatique dans les domaines suivants :

  • langages de programmation ;
  • systèmes de types ;
  • analyse statique ;
  • preuve de programmes ;
  • politiques de sécurité de haut niveau ;
  • programmation parallèle ;
  • programmation distribuée ;
  • bases de données ;
  • génération d’interfaces graphiques.

Ces stages, dont la durée est à négocier, sont prévus a priori pour le deuxième semestre 2009-2010, seront rémunérés 800€ bruts/mois + primes et pourront déboucher sur un doctorat avec bourse CIFRE ou/et sur une embauche en CDI.

Compétences et parcours

Le candidat doit être étudiant de Master 2 (professionnel ou recherche) en Informatique et doit s’intéresser à la notion de programmation sûre par construction. De plus, le candidat devra avoir des connaissances dans au moins l’un des domaines suivants :

  • programmation fonctionnelle, si possible à l’aide de OCaml, F#, SML, Haskell, Scala ou un autre langage proche de ML ;
  • programmation web ;
  • programmation parallèle ou/et distribuée ;
  • modèles à base de messages ;
  • compilation ;
  • systèmes de types ;
  • sémantique du parallélisme ;
  • preuve de programmes, si possible à l’aide de Coq, Focal, Pangolin, Why, Ynot, Who ou d’autres outils de preuve formelle ;
  • bases de données, y compris et en particulier les bases de données non-relationnelles  ;
  • sécurité des programmes.

Le candidat doit avoir le droit de travailler en France et sera affecté sur le site de R&D de MLstate, à Paris, dans le quartier Bibliothèque François Mitterand, dans une équipe dynamique, multilingue, composée de chercheurs et d’ingénieurs de recherche.

Sujet : compilation

Le développement de compilateurs optimisateurs pour des langages de haut niveau se heurte fréquemment à des problèmes inhérents aux processeurs et aux machines virtuelles modernes, conçus pour améliorer la performance de langages impératifs de bas niveau. De nombreuses techniques fondées sur le lambda-lifting ou les transformations par passage de continuation, ont été conçues pour compiler efficacement des langages fonctionnels d’ordre supérieur vers un modèle impératif. Ces techniques interviennent aussi lors de la compilation de code parallèle ou/et distribué.

Le langage OPA est un langage de haut niveau, doté de plusieurs compilateurs visant plusieurs cibles, natives et interprétées, séquentielles et parallèles. Dans le cadre de ce travail, l’étudiant prendra part au développement d’une branche expérimentale du compilateur parallélisateur natif OPA. Le stagiaire devra concevoir et implanter des techniques de compilation, d’optimisation et d’analyse statique, ainsi que mesurer et améliorer les performances du compilateur lui-même.

Ce travail sera dirigé par Mikolaj Konarski et François-Régis Sinot et impliquera des recherches bibliographiques, la conception de phases de compilation et d’optimisation, la programmation en OCaml, la conception et l’implantation d’expériences, l’analyse et l’exploitation des résultats. Un éventuel doctorat ou CDI pourra continuer ce stage sous la forme du développement complet d’une nouvelle génération de compilateur OPA.

Sujet : système de types

Dans les langages de programmation statiquement typés, la première protection contre les failles de sécurité passe par le système de types, qui vérifie la cohérence entre un certain nombre d’hypothèses faites implicitement ou explicitement par le programmeur. Malgré la souplesse que permettent les langages de programmation avec inférence de types, aucun système de types n’acceptera tout programme correct et tout programmeur se retrouvera un jour confronté aux limitations du système de types qu’il emploie.

Le langage OPA est statiquement typé. Au cours de son existence, ce langage a déjà connu deux générations majeures de systèmes de types, qui lui ont permis de gagner en souplesse, en puissance et en fiabilité. Dans le cadre de ce travail, l’étudiant prendra part au développement d’une troisième génération de système de types d’OPA. Le stagiaire devra proposer des techniques d’inférence et de vérification de types pour des types récursifs implicites (y compris des types récursifs ouverts), des techniques de correction interactive d’erreurs de types introduites par l’utilisateur, ainsi que des techniques pour faire interagir le typage statique d’OPA et des utilisations qui pourront nécessiter une forme de typage dynamique.

Ce travail sera dirigé par Mikolaj Konarski et François-Régis Sinot et impliquera des recherches bibliographiques, la conception d’algorithmes et de contraintes de typage, la programmation en OCaml, la conception et l’implantation d’expériences, l’analyse et l’exploitation des résultats. Un éventuel doctorat ou CDI pourra continuer ce stage sous la forme du développement complet d’une nouvelle génération de système de types OPA.

Sujet : métaprogrammation statique et manipulation statique de programmes

La métaprogrammation est une technique de programmation qui consiste à écrire des programmes ou des sous-programmes qui seront évalués durant la compilation ou l’interprétation et produiront un nouveau programme ou sous-programme, qui pourra à son tour être évalué ou compilé, etc. Cette technique, très puissante, pose de nombreuses difficultés de gestion des dépendances, de typage, de performance et de traçabilité.

La chaîne de compilation OPA emploie en interne des techniques de métaprogrammation qui ne sont pas, à l’heure actuelle, manipulables directement par l’utilisateur. Dans le cadre de ce travail, l’étudiant prendra part à l’expérimentation sur la possibilité de développer des techniques de métaprogrammation sûres et simples pour OPA. En parallèle, l’étudiant prendra part au développement d’outils de manipulation statique de programmes pour refactoring, analyse de propriétés et mesures de qualité, etc.

Ce travail sera dirigé par Rudy Sicard et François-Régis Sinot et impliquera la conception et l’implantation d’algorithmes de manipulation de programme durant la compilation et hors-compilation, d’algorithme pour remonter les erreurs de typage apparaissant durant durant la compilation suite à la manipulation de programme par métaprogrammation, ainsi que l’implantation d’utilitaires pour OPA.

Sujet : programmation distribuée

Par nature, les applications web sont distribuées entre un serveur et de nombreux clients. Généralement, le côté serveur est lui-même distribué entre plusieurs serveurs web, plusieurs serveurs de stockage et parfois des serveurs additionnels de calcul. Si cette distribution est fréquemment nécessaire pour des raisons de performances, de capacité de stockage ou tout simplement de fonctionnalités, les mécanismes sous-jacents sont généralement de grandes sources de lenteur, de gaspillage d’espace et de failles de sécurité.

Le compilateur OPA produit des applications distribuées entre toutes ces cibles. Dans le cadre de ce travail, l’étudiant prendra part à l’amélioration de l’environnement d’exécution distribué d’OPA, notamment à l’optimisation du ramasse-miettes distribué, des protocoles de communication et de migration entre serveurs et du routage entre serveurs. L’objectif de ce stage est d’améliorer les performances de l’exécution distribuée de code OPA sans diminuer la sécurité existante.

Ce travail sera dirigé par David Rajchenbach-Teller et Rudy Sicard et impliquera de la théorie de la distribution, de la bibliographie, la conception et l’implantation d’algorithmes de ramasse-miettes en OCaml ou/et en OPA, ainsi que l’expérimentation et l’exploitation des résultats d’expériences. Un éventuel doctorat ou CDI pourra continuer ce stage par l’implantation d’une deuxième génération d’environnement d’exécution distribuée pour OPA.

Sujet : Preuve de programmes

Pour être totalement certain qu’un programme correspond à ses spécifications, il est nécessaire de prouver ce programme formellement, sous la forme d’un ensemble de théorèmes vérifiables par un outil tel que Coq. Si Coq dispose de nombreux modules et de nombreuses bibliothèques, le champ d’action de cet outil reste encore limité par rapport à l’ensemble des propriétés nécessaire pour garantir le fonctionnement d’une application complète, en particulier d’une application web.

Dans le cadre de ce travail, l’étudiant prendra part à l’effort en cours de MLstate pour définir une plateforme formellement prouvée pour le développement Web. En particulier, le stagiaire s’intéressera à la manipulation de texte dans Coq, manipulation qu’il étendra de manière à introduire les encodages internationaux. En particulier, l’objectif de ce travail est de permettre à Coq de représenter et de prouver des propriétés sur les encodages internationaux, les conversions de chaînes de caractères, les structures de cordes de caractères, …

Ce travail sera dirigé par Adam Koprowski et impliquera essentiellement de la spécification et de la programmation en Coq.

Sujet : Bases de données

Toute application web dépend d’une base de données pour le stockage des informations à long terme. Si la fiabilité du stockage lui-même, est un problème largement étudié, la fiabilité des entrées-sorties soulève de nombreuses questions qui restent à explorer. En particulier, que faut-il faire si des données manquent, si le format des données a changé, si les données ont été (re)réparties selon des critères différents des critères attendus.

Dans le cadre de ce travail, l’étudiant prendra part à la recherche et au développement de MLstate sur les questions d’interaction entre stockage et application web, notamment les notions de partage de données entre applications web et de mise-à-jour du format des données.

Ce travail sera dirigé par Louis Gesbert et impliquera de la programmation en OCaml et en OPA.

Sujet : Interaction entre bases de données relationnelles et bases de données structurées

Toute application web dépend d’une base de données pour le stockage des informations à long terme. Le paradigme de stockage employé par la majorité des applications à ce jour est une extension du modèle relationnel, au sens où les informations sont stockées dans des tables (ou “relations”), tables prévues pour être manipulées par un être humain et liées par des clés explicites. À l’inverse, un autre paradigme de bases de données, parfois appelé “structuré”, “algébrique” ou “objet”, stocke les informations sous la forme de structures de données, prévues pour être manipulées par un programme et liées par des références implicites.

Dans le cadre de ce travail, l’étudiant prendra part à la recherche et au développement de MLstate sur l’unification des modèles relationnels et structurés. En particulier, l’étudiant devra concevoir et implanter des techniques permettant d’exploiter des bases de données relationnelles et des données préexistantes dans le cadre d’un paradigme structuré, ainsi que de porter au modèle structuré les outils de consultation traditionnellement exploités dans le modèle relationnel.

Ce travail sera dirigé par Louis Gesbert et impliquera de la programmation en OCaml, en OPA et dans divers dialectes de SQL.

Pour candidater

Pour candidater, nous vous invitons à envoyer un CV et une lettre de motivation, par courrier physique ou électronique, à Henri Binsztok et David Teller. Si possible, joignez un échantillon de vos travaux scientifiques ou/et techniques.

À propos de MLState

Fondée à Paris en 2007 par Henri Binsztok, enseignant aux Universités Paris 6 & 7, MLState développe un nouveau langage pour la création d’applications web. Ce langage, fondé sur les avancées les plus récentes en termes de recherche, ouvre des perspectives nouvelles en termes de prouvabilité, de calcul distribué et d’intégration aux bases de données. MLstate a été récompensée de nombreuses fois pour cette technologie, remportant notamment le Prix du Concours national d’aide à la création de technologies innovantes. À côté de développements pour des clients, MLstate fournit un effort important de recherche pour enrichir son offre technologique intégrée.

Dans le cadre de ses recherches, MLstate travaille avec l’ENS Ulm, le CNAM, l’ENSIIE, les universités Paris 6 et Paris 12, l’INRIA Rhône-Alpes, l’Université d’Edinburgh, l’Imperial College of London, l’Université de Cambridge, l’Université de Saint-Andrews, l’Université Heriot-Watt, l’Université de Bologne …

About these ads

Tagged: , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , , ,

§ One Response to Stages M2 langages de programmation

  • [...] Publié dans En français / In French, Informatique / Computer science, Recherche / Research, Stage, Sûreté / Security, offre d'emploi tagged applications web, bytecode, canaux, candidat, certification, compilation, entreprise, informatique, langages de programmation, lifo, m2, machine virtuelle, mastère, mastère 2, master, master 2, mlstate, mpi, OCaml, parallélisme, pi-calcul, programmation, Programmation Fonctionnelle, sémantique, sds, stage, start-up, systèmes d'exploitation à 1:29 par yoric Note De nouveaux stages sont proposés pour l’année 2009-2010. [...]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

What’s this?

You are currently reading Stages M2 langages de programmation at Il y a du thé renversé au bord de la table.

meta

Follow

Get every new post delivered to your Inbox.

Join 32 other followers

%d bloggers like this: