Informations générales

Les stages effectués au Centre de recherche en informatique de MINES ParisTech sont réalisés sous la responsabilité d’un chercheur ou ingénieur permanent du centre.
L’accent est mis sur la qualité du travail réalisé, l’autonomie des stagiaires, voire leur pro-activité, dans un cadre qui favorise les échanges informels.
Les propositions de stage ci-dessous sont disponibles à tout moment.</p>

Liste des offres de stage

Les offres de stage sont classées selon les catégories suivantes :

Offres de stage


Stage « Efficient Data Structures for Points-to Analysis »

Points-to analysis is crucial to analyze, transform. optimize and compile C programs. Many different kinds of points-to analyses have been introduced but they all depend on efficient data structures to minimize their space and time complexities. For the time being, only simple and crude analyses are performed in production compiler because of the potential cost of more accurate analyses.
In her PhD, Amira Mensi has implemented in PIPS an interprocedural bottom-up points-to analysis to reduce the points-to graph size to the locally visible pointers. However, the underlying data structure she uses is correct but not efficient, neither in space nor in time. The goal of the internship is to analyze the deficiencies of the current implementation by obtaining traces for the many test cases accumulated by Amira, to design several alternative data structures, to select the best one and to integrate it in the current implementation using a new API for points-to graphs.
PIPS is programmed in C and managed with SVN. It already contains many program analyses and transformation and is designed to be extensible. This makes adding new transformations pretty easy, once the framework is understood. This internship requires a good C programmer, with an interest in abstract interpretation and code optimization, ready to interact with other PIPS developers over Internet. The subject is extensible and could lead to a PhD position.

Personne à contacter : Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin–at–mines-paristech.fr


Stage « Generation of Distributed Code: a Small Step Approach to Prove Correctness » :

Code distribution is crucial for many embedded systems and large scale scientific applications. Standard techniques are based, in practice, on the MPI library or on ad'hoc development tools. In both cases, programmers must tackle alone all the issues linked to distributed programming: memory consistency, deadlock, efficiency. Several attempts have been made in research to ease distributed programming using either directives or new programming languages, but compiler technology is not used much because the parallel constructs are either macros or syntactic sugar for a run-time library.

In her PhD, Dounia Khaldi has proposed to generate distributed code directly from a mapping of the statement on the target architecture and from a data dependence graph. It turns out that her heuristic is not robust. The goal of the internship is to explore small-step approaches, classical with compilers and their many passes. Instead of looking for a one-shot transformation from shared to distributed memory code, the intern should look for succession of small transformations, i.e. compiler passes, leading from an initial mapped code for a shared memory machine to a final distributed code. Hopefully, many of the necessary transformations are already implemented in our PIPS framework, but new ones will have to be added.

PIPS is programmed in C. It already contains lots of program analyses and transformation and is designed to be extensible. This makes adding new transformations pretty easy, once the framework is understood.

This internship requires a good C programmer, with an interest in computer architecture and code distributionion, ready to interact with other PIPS developers over Internet. The subject is very ambitious and can lead to a PhD position.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr



Stage « Coarse grain loop parallelization » :

Loop parallellization is crucial for GPU's and multicore processors. Standard techniques are based on dependence graphs linking definition and usage of variable values. The graph arcs contain additional information about the relationship between loop iterations creating these arcs. This information is used to decide if the loop can be parallelized and how it should be parallelized.

The coarse grain approach does not use graphs but summaries of the loop body effects on memory. Each loop can be parallelized, regardless of its body control structure and procedure calls. Coarse grain parallelizations has already been implemented in PIPS, our automatic code analysis and transformation framework, but it should be reimplemented in a simpler way, using additional transformer information and integrating, as far as possible, auxiliary transformations such as array section privatization (this includes scalar and array privatization) and invariant code motion.

PIPS is programmed in C. It already contains lots of program analyses and transformation and is designed to be extensible. This makes adding new transformation pretty easy, once the framework is understood.

This internship requires a good C programmer, with an interest in computer architecture and code optimization, ready to interact with other PIPS developers over Internet.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr



Stage « Coarse grain loop fusion » :

Loop fusion is crucial for GPU's and multicore processors with a memory hierarchy because it improves locality, sometimes dramatically. Standard techniques are based on dependence graphs linking definition and usage of variable values. The graph arcs contain additional information about the relationship between loop iterations creating these arcs. This information is used to decide if two loops can be fused and how.

The coarse grain approach does not use graphs but summaries of the loops body effects on memory. Two loops can be fused if the memory areas they write do no impact the memory area they would have read before or written after. Bascially, the Bernstein conditions must be checked for different sets of iterations and this can be performed without building a graph. Loop fusion has already been implemented in PIPS, our automatic code analysis and transformation framework, using the standard graph-based technique, but it should be reimplemented in a simpler way, using additional transformer information, allowing shifting, prologue and epilogue when the iteration sets are different, and integrating, as far as possible, auxiliary transformations such as array section privatization (this includes scalar and array privatization) and invariant code motion. Non adjacent loops should also be tackled.

PIPS is programmed in C. It already contains lots of program analyses and transformation and is designed to be extensible. This makes adding new transformation pretty easy, once the framework is understood.

This internship requires a good C programmer, with an interest in computer architecture and code optimization, ready to interact with other PIPS developers over Internet.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr



Stage « Analyse statique des paramètres fonctionnels et des pointeurs vers des fonctions » :

L'utilisation de paramètres fonctionnels et de pointeurs vers des fonctions permet d'écrire des codes élégants et puissants, mais elle rend les analyses statiques de tels codes plus délicates alors que la multiplicité et la complexification des architectures matérielles les rendent plus nécessaires que jamais: multicore, GPU, multiprocesseur hétérogène, accélérateur FPGA,...

L'objectif du stage est d'abord de faire un tour rapide de la bibliographie et de proposer plusieurs solutions plus ou moins précises. Ensuite, une ou plusieurs de ces solutions seront implantées en C dans le framework de compilation source-a-source PIPS.

Ce stage peut éventuellement se prolonger par une thèse dans le domaine de la compilation.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr



Stage « Coarse grain approach for loop invariant code motion » :

Loop invariant code motion is a standard code optimization technique. We currently use a technique based on dependence graphs linking definition and usage of variable values. The graph arcs contain additional information about the relationship between loop iterations creating these arcs. The Allen & Kennedy algorithm is slightly modified to hoist the invariant code through loop distribution. This is described in Julien Zory's PhD dissertation, available on line, and implemented in PIPS, our automatic code analysis and transformation framework.

The coarse grain approach does not use graphs but summaries of the loop body effects on memory and of each of its components. It is possible to decide independently for each statement if it can be moved out of the loop because its result is iteration independent. It is still unclear how efficient this approach can be in practice. It is simpler but can only move one statement of the loop body, not a set of statements as is possible with the A&K based algorithm. Experiments will be carried out to check the effectiveness of the coarse grain approach.

PIPS is programmed in C. It already contains lots of program analyses and transformation and is designed to be extensible. This makes adding new transformation pretty easy, once the framework is understood.

This internship requires a good C programmer, with an interest in computer architecture and code optimization, ready to interact with other PIPS developers.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr


Stage « Détection des variables non initialisées d'un programme C » :

La rétro-ingénierie, la maintenance et l'optimisation de codes nécessitent l'application de nombreuses analyses statiques ou dynamiques qui permettent de mieux comprendre, vérifier, améliorer et optimiser les instructions.

Parmi ces analyses, la détection des variables non initialisées avant leur utilisation permet d'éviter des erreurs lors de l'exécution du programme. Elle permet également de valider les analyses ultérieures portant sur les accès aux variables du programme, en lecture et écriture, telles que le calcul des dépendances.
La phase d'analyse dynamique de détection des variables non initialisées avant leur utilisation est déjà intégrée dans notre framework de compilation source-a-source PIPS pour des programmes en Fortran.

L'objectif de ce stage est d'implanter cette analyse pour les programmes C.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr


Stage « Détection des débordements de tableaux d'un programme C » :

La rétro-ingénierie et la maintenance de codes nécessitent l'application de nombreuses analyses statiques ou dynamiques qui permettent de mieux comprendre et de vérifier les programmes.

Parmi ces analyses, la détection des débordements de tableaux est essentielle. Elle permet d'éviter des erreurs lors de l'exécution du programme, mais aussi de valider les résultats des analyses qui caractérisent l'ensemble des éléments de tableaux référencés par des instructions. La phase d'analyse dynamique de détection des débordements de tableaux est déjà intégrée dans notre framework de compilation source-a-source PIPS pour des programmes en Fortran.

L'objectif de ce stage est d'implanter cette analyse pour les programmes C.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr

Stage « Linéarisation de tableaux et test de dépendance » :

PIPS est un framework de compilation source-a-source qui intègre de nombreuses transformations de programmes source-a-source ainsi que des analyses statiques et dynamiques et qui permet d'en développer rapidement de nouvelles.

Une des optimisations clés est la parallélisation automatique de boucles. Mais les programmeurs C ainsi que les générateurs automatiques de code C ont tendance à linéariser leurs tableaux, c'est-à-dire à remplacer les tableaux multidimensionnels par des tableaux monodimensionnels. Les expressions d'indices qui en résultent ne sont généralement pas affines et les tests de dépendance échouent. L'objectif de ce stage est de développer un nouveau test de dépendance permettant de linéariser, dans le vrai sens du terme, les polynomes qui résultent d'une linéarisation de tableaux. Un minimum de connaissance en algèbre linéaire permettra d'aborder le sujet plus facilement.

Ce stage est plutôt orienté ingénieur, mais il peut éventuellement se prolonger par une thèse dans le domaine de la compilation.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr


Stage « Régénération de code source C » :

PIPS est un framework de compilation source-a-source qui intègre de nombreuses  transformations de programmes source-a-source ainsi que des analyses statiques et dynamiques et qui permet d'en développer rapidement de nouvelles.

Les analyses et transformations sont appliquées à une représentation interne du programme, mais une fois les analyses ou transformations réalisées, il faut montrer le résultat en respectant au mieux le style initial du code source. L'objectif de ce stage est de raffiner cette phase de restitution pour les programmes C. Au-delà des problèmes d'indentation qui peuvent être traités en interne ou en externe via, par exemple, indent, il faudrait aussi reconnaître les graphes de contrôle qui peuvent être représentés par la construction switch, regénérer les includes, et ajouter des commentaires Doxygen en fonction des résultats d'analyse de PIPS.

Ce stage est plutôt conçu comme un stage ingénieur, mais il peut éventuellement se prolonger par une thèse dans le domaine de la compilation.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr


Stage « Gestion des dépendances de contrôle dans l'élimination de code mort » :

PIPS est un framework de compilation source-a-source qui intègre de nombreuses  transformations de programmes source-a-source ainsi que des analyses statiques et dynamiques et qui permet d'en développer rapidement de nouvelles.

L'élimination de code mort consiste à retirer d'un programme toutes les instructions et les variables qui n'ont pas d'impact sur le résultat. Cette transformation s'appuie sur les use-def chains, mais elle doit aussi prendre en compte les dépendances de contrôle. Elle est particulierement utile pour traiter du code généré automatiquement par un outil ou un compilateur de langage DSL. L'implantation qui est disponible dans PIPS prend correctement en compte les dépendances de données, mais les dépendances de contrôle le sont imparfaitement.

Le but du stage est de compléter cette implantation, voire d'introduire une nouvelle analyse, une analyse de continuation. La continuation consiste à déterminer si un statement peut provoquer un arrêt ou une boucle infinie, ou bien si l'éxecution doit nécessairement passer au statement suivant. L'information de continuation reste à raffiner puisqu'on ne pourra pas toujours déterminer s'il y a continuation nécessaire ou continuation possible.

Ce stage est plutôt conçu comme un stage ingénieur, mais il peut éventuellement se prolonger par une thèse dans le domaine de la compilation.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr


Stage 8 « Parallélisation des réductions par sections critiques » :

PIPS est un framework de compilation source-a-source qui intègre de nombreuses  transformations de programmes source-a-source ainsi que des analyses statiques et dynamiques et qui permet d'en développer rapidement de nouvelles.

La détection des réductions est implantée dans PIPS, mais elle est exploitée en générant les directives OpenMP spécifiques. Dans certains cas, il est plus efficace de ne pas distribuer une grosse boucle de calcul en une boucle de calcul parallèle et une boucle de réduction. Pour des raisons de localités, il vaut mieux éxécuter en parallèle la boucle initiale et protéger par une section critique la mise à jour de la variable de réduction.

L'objet premier de ce stage est de générer les sections critiques nécessaires à l'éxécution parallèle des réductions. L'objectif second est de vérifier que cette technique permet de traiter efficacement les réductions avant ou après une parallèlisation dite CoarseGrain.

Ce stage est plutôt conçu comme un stage ingénieur, mais il peut éventuellement se prolonger par une thèse dans le domaine de la compilation.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr


Stage « Ordonnancement optimal et vectorisation des calculs de l'opérateur de Dirac » :

La Chromodynamique Quantique sur Réseaux (Lattice Quantum ChromoDynamics ou LQCD en anglais) étudie le mécanisme de la formation de la matière à travers l'interaction des particules fondamentales de l'univers sous les contraintes de confinement (naissance de l'univers juste après le Big Bang). Un axe très prépondérant de cette étude repose sur d'intenses simulations (de type Monte Carlo), dont le principal ingrédient est l'opérateur de Dirac. Du point de vue informatique, la mise en œuvre de cet opérateur expose des patterns d'accès mémoire assez spéciaux ainsi qu'un schéma de calcul pouvant contenir des redondances. L’évaluation de l'opérateur de Dirac étant très répétée, sa mise en œuvre optimisée (suivant l'architecture cible) est devenue le principal cheval de bataille dans la recherche en LQCD (voir le projet <a href="https://www.petaqcd.org/" target=_blank>PetaQCD financé par l'Agence Nationale de le Recherche).

L'étude d'une mise en œuvre efficace de l'opérateur de Dirac se fait à deux niveaux. Le niveau macroscopique, dans lequel le réseaux global est subdivisé en sous-réseaux géométriquement identiques, il faut donc trouver le bon partitionnement et gérer efficacement les communications entre les sous-réseaux. Le niveau microscopique, dans lequel on réorganise les calculs de base de l'opérateur proprement dit de manière à réduire les redondances tout en limitant la perte d'efficacité mémoire (défaut de caches). Cette réorganisation peut se faire par des approches algébriques (factorisations et simplifications en algèbre linéaire) et/ou par une réécriture des instructions de manière à utiliser plus efficacement les possibilités de l'architecture cible (pipeline d'instructions, vectorisation).

Le travail ici consistera à transformer le corps de la boucle principale de l'opérateur de Dirac, de manière à réduire au mieux les défauts de cache. On pourra utiliser un modèle analytique (à déterminer) ou un outil approprié pour mesurer l'efficacité mémoire. La vectorisation explicite du code sera ensuite envisagée.

Prérequis :
Un minimum de connaissance en algèbre linéaire et optimisation de code facilitera l'entrée en matière pour ce sujet. De plus, un intérêt pour l'adéquation application/code/architecture sera utile pour entretenir un bon degré de motivation et d'enthousiasme.
Il n'est pas nécessaire d'avoir des connaissances en physique des particules, mais un minimum de culture sur le sujet sera acquis en chemin.
Ce stage, qui pourra être mené aussi bien sous un angle recherche que sous un angle programmation, pourra servir de point de départ pour une thèse en calcul haute performance (pour la QCD).

Personne à contacter :

Envoyer un CV et une lettre de motivation à Claude Tadonki (CRI, MINES ParisTech).
E-mail : claude.tadonki--at--mines-paristech.fr
Web : http://www.omegacomputer.com/staff/tadonki/

Stage « Représentations intermédiaires parallèles pour LLVM et GCC » :

Sujet :
Application de la méthodologie SPIRE, développée au CRI et permettant l'extension des représentations intermédiaires de compilateurs, aux plateformes LLVM et GCC.

Projet :
La plupart des grandes plateformes de compilation comme LLVM, GCC ou PIPS ont été conçues dans l'optique de la génération de code pour des langages impératifs séquentiels. Avec la multiplication des architectures multicoeurs, des langages explicitement parallèles de type X10, Habanero-Java… et des extensions parallèles type OpenMP et MPI, il convient d'envisager d'étendre l'architecture de ces plateformes pour être à même de traiter les spécificités de ces langages.
Afin de pouvoir réutiliser autant que possible l'investissement logiciel lourd auquel correspondent ces compilateurs, la méthodologie SPIRE d'extension "légère" de représentation intermédiaire, une structure de données centrale dans ces systèmes, a été proposée au CRI et validée, en partie, dans le cas de la plateforme de compilation PIPS.

Descriptif :

L'objet du stage de niveau Master 2 Recherche, de quelques mois, est, en partant du système SPIRE développé par le CRI :

  • d'étudier en détail les représentations intermédiaires (RI) des compilateurs LLVM et GCC ;
  • d'analyser les extensions parallèles des RIs déjà introduites dans la littérature ;
  • de tester la capacité de la méthodologie SPIRE à étendre ces RIs séquentielles au monde parallèle ;
  • et d'implémenter dans au moins une de ces plateformes ces RI étendues pour en tester expérimentalement la pertinence.

Exigences :
Une bonne connaissance de la programmation en C, des systèmes de compilation et des méthodes de spécification formelle est nécessaire.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Pierre Jouvelot (CRI, MINES ParisTech).
E-mail : pierre.jouvelot--at--mines-paristech.fr
Web : http://www.cri.mines-paristech.fr/~pj

Stage « Multithreading sous Matlab » :

Sujet :
Multithreading sous Matlab (Stage Master Recherche 2012/2013)

Projet :
Matlab est un environnement de calcul et de programmation scientifique très utilisé pour la puissance de son moteur (noyau de traitement constitué de routines optimisées) et sa très grande flexibilité (prise en main aisée et utilisation assez souple).
Toutefois, dans sa version "langage de programmation", il propose un interpréteur à la place d'un compilateur. Ceci justifie sa souplesse de programmation et d'exécution interactive, mais en contre partie, il y a d'une part le surcoût sur le temps global d'exécution qui est dû au fonctionnement de l'interpréteur, et d'autre part la difficulté (voire l'impossibilité) d'utiliser directement les outils traditionnels d'analyse et d'optimisation de codes (y compris la parallélisation).
Notons toutefois qu'il existe un moyen de se raccrocher à un langage compilé tel que le C (C++ ou Fortran) via le mécanisme des fichiers "mex".
Avec l'avènement des machines multicœurs, il devient indispensable d'offrir la possibilité de paralléliser les applications dans tout environnement de programmation ou de calcul.

Descriptif :
Le but de ce stage sera donc d'étudier ce problème dans le cadre de Matlab.
En résumé, il s'agit d'étudier les mécanismes de programmation ou d'exécution multithreadée sous Matlab, en analyser les avantages et inconvénients, et procéder à des études de cas avec mesures de performances commentées.
Ce sera l'occasion pour le stagiaire, en fonction de ses capacités, de développer aussi sa propre méthodologie, tout au moins en initier une qui pourra être approfondie plus tard et étendue aux environnements similaires.

Exigences :
Le candidat devra avoir un niveau acceptable en C et connaître un peu Matlab (pas indispensable toutefois, à défaut il y aura une phase de familiarisation préalable).
De même, des notions de base de parallélisme sont importantes, surtout le modèle à mémoire partagé. L'occasion sera donnée au candidat de s'initier à la parallélisation automatique.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Claude Tadonki (CRI, MINES ParisTech).
E-mail : claude.tadonki--at--mines-paristech.fr
Web : http://www.omegacomputer.com/staff/tadonki/

Stage « Modélisation de la bibliothèque MPI dans un compilateur source-à-source » :

Contexte :
PIPS est un framework de compilation source-à-source qui intègre de nombreuses transformations de programmes source-à-source ainsi que des analyses statiques et dynamiques et qui permet d'en développer rapidement de nouvelles. Par exemple, PIPS peut réaliser une analyse de préconditions qui permet de déterminer quelles sont les conditions vérifiées avant l'exécution d'une instruction. Il permet également de faire des transformations telles que l'élimination de code mort, qui détecte les instructions inutiles et les supprime, ou encore du déroulage ou de la fusion de boucles. Parmi ces transformations, une génération de code parallèle distribué au moyen de la bibliothèque MPI est en cours de développement. PIPS peut prendre en entrée du code C ou Fortran.
Cependant, le code distribué MPI n'est actuellement pas supporté par PIPS en entrée. Le code MPI généré ne peut donc pas être réanalysé et aucune nouvelle transformation ou optimisation n'est possible sur celui-ci.

Objectif :
L'objectif de ce stage est d'étudier et surtout d'implémenter les différentes possibilités de prise en charge d'une telle bibliothèque. Pour cela, le stagiaire sera amené à étudier le comportement des fonctions MPI.
Puis, il devra les intégrer dans la représentation interne de PIPS. Plusieurs solutions ont déjà été envisagées, mais le candidat est libre d'en proposer de nouvelles. Par exemple, des stubs peuvent être créés pour simuler les fonctions MPI ou des intrinsèques MPI peuvent être ajoutés à ceux déjà présents dans PIPS.
Durée : 3 à 6 mois

Prérequis :
Une bonne connaissance du langage de programmation C est exigée. Une connaissance de la bibliothèque MPI et du langage Fortran est un plus.

Référence:
PIPS : http://www.pips4u.org/
MPI : http://www.mpi-forum.org/

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr

Stage « Distribution automatique de tâches dans une architecture parallèle basée sur des processeurs en mémoire (PIM)» :

Contexte :
Les processeurs en mémoire (PIM) constituent une nouvelle approche matérielle consistant à embarquer des unités de processing (CPU) directement dans la mémoire des ordinateurs. Une machine équipée de tels composants dispose d'un très grand nombre de calculateurs parallèles, proches de la mémoire de travail du processeur.
La société uPmem propose un modèle de processeur en mémoire, pour lequel un premier environnement de développement est disponible.
PIPS est un framework de compilation source à source, capable de générer des programmes de calcul parallèle sur la base d'informations de distribution des données et des opérations.
En particulier, une implémentation permet d'automatiser la parallélisation et la synchronisation de calculs sur de multiples tâches communiquant via MPI.

Objectif :
L'objectif de ce stage est d'adapter PIPS et le code généré pour remplacer les tâches par des processeurs en mémoire. Sur la base d'un cas d'utilisation simplifié, le stagiaire sera amené à porter ou adapter les primitives MPI invoquées par un programme généré par PIPS en des appels aux processeurs en mémoire.
Il devra pour cela modéliser un "bus de communication inter-DPU", utiliser les primitives de l'API fournie par uPmem et modifier le compilateur PIPS pour qu'il génère un code adapté à ce framework.
Le stagiaire exercera son travail sur des cas d'utilisations simples qui permettront d'évaluer le gain en performance apporté par les PIMs.

Prérequis :
- Une bonne connaissance de la programmation C est exigée.
- La connaissance de la programmation parallèle est demandée.
- Une première pratique de MPI est souhaitée.

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr

Stage « Implémentation d'une application de détection de plaques d'immatriculation sur un processeur en mémoire (PIM) » :

Contexte :
Les processeurs en mémoire (PIM) constituent une nouvelle approche matérielle consistant à embarquer des unités de processing (DPU) directement dans la mémoire des ordinateurs. Une machine équipée de tels composants dispose d'un très grand nombre de calculateurs parallèles, proches de la mémoire de travail du processeur.
Cette approche architecturale constitue un enjeu majeur dans le monde du big data, de la recherche médicale, etc.
La société uPmem propose un modèle de processeur en mémoire, pour lequel un premier environnement de développement est disponible.
Le traitement d'images, et particulièrement de flux videos, est très gourmand en puissance de calcul et constitue un domaine potentiel important pour les PIM.

Objectif :
L'objectif du stage est de robustifier une application de détection de plaques d'immatriculation existante en C ou en C++ et de la porter sur une machine constituée d'un hôte et d'un ou plusieurs accélérateurs DPU à l'aide du SDK de la société uPmem, afin d'en déterminer les performances par rapport à une CPU généraliste.

Prérequis :
Des connaissances en traitement d'images, particulièrement en morphologie mathématique, et en programmation C/C++ parallèle.

Lieu :
à déterminer (Fontainebleau, Grenoble, Paris)

Personne à contacter :

Envoyer un CV et une lettre de motivation à François Irigoin (CRI, MINES ParisTech).
E-mail : francois.irigoin--at--mines-paristech.fr

Stage « Conception multithreadée pour un processeur en mémoire (PIM) » :

Contexte :
Les processeurs en mémoire (PIM) constituent une nouvelle approche matérielle consistant à embarquer des unités de processing (CPU) directement dans la mémoire DRAM des ordinateurs. Une machine équipée de tels composants dispose d'un très grand nombre d'unités parallèles, proches de la mémoire de travail du processeur.
La société uPmem propose un modèle de processeur en mémoire, nommé DPU (DRAM Processing Unit), pour lequel un premier environnement de développement est disponible . Toutefois, le modèle parallélisation actuellement supporté est de type centralisé, avec une exécution exclusivement séquentielle. Par analogie au modèle hybride standard combinant parallélisme à mémoire distribuée et parallélisme à mémoire partagée, il serait intéressant d'explorer la possibilité de rendre opérationnelle la mise en œuvre d'un modèle d'exécution similaire sur le DPU.

Objectif :
Afin d'anticiper le besoin d'un usage de type hybride, c'est à dire en considérant une parallélisation interne des nœuds, en ce qui concerne le DPU. Il s'agira de conceptualiser ce modèle d'exécution sur le DPU, d'en fournir une infrastructure de mise en œuvre, et d'étudier les différents mécanismes assurant une interaction correcte et opérationnelle entre les différentes composantes du système global.

Prérequis :
- Fondamentaux de l'architecture des ordinateurs
- Programmation multithreadée (OpenMP ou Pthreads)

Personne à contacter

Envoyer un CV et une lettre de motivation à Claude Tadonki (CRI, MINES ParisTech).
E-mail : claude.tadonki--at--mines-paristech.fr

Stage « Distribution et maintien de la cohérence de données dans un machine parallèle à base de processeurs en mémoire (PIM) » :

Contexte :
Les processeurs en mémoire (PIM) constituent une nouvelle approche matérielle consistant à embarquer des unités de processing (CPU) directement dans la mémoire des ordinateurs. Une machine équipée de tels composants dispose d'un très grand nombre de calculateurs parallèles, proches de la mémoire de travail du processeur.
Ces architectures à mémoire distribuée ne disposent pas en général de système de gestion de cohérence de la mémoire. Cette dernière doit être assurée par le programmeur ou intégrée au code par le compilateur. Il doit générer un code contenant à la fois les calculs et les communications explicites nécessaires à l’exécution des tâches parallèles sur les processeurs.
La mémoire interne des processeurs étant restreinte, il est important d'optimiser l'allocation et le référencement des données utilisées par les tâches. Si les calculs effectués sur un processeur n’adressent qu’une sous-partie d'un tableau, il serait préférable de déclarer et de référencer dans la tâche qu’un tableau restreint à cette sous-partie.

Objectif :
PIPS est un framework de compilation source à source, capable de générer des programmes de calcul parallèle sur la base d'informations de distribution des données et des opérations. En particulier, une implémentation permet d'automatiser la parallélisation et la synchronisation de calculs de multiples threads communiquant via MPI.
La société uPmem propose un processeur en mémoire, nommé DPU, pour lequel un premier environnement est disponible. L’objectif de ce stage est de proposer et d’implémenter dans PIPS les solutions permettant d’optimiser la mémoire de tâches exécutées sur ce type de processeurs.

Il s’agit de définir les conditions d’application des optimisations proposées, puis de traduire les déclarations et les fonctions d'accès aux éléments des tableaux des tâches de manière appropriée. Enfin, les codes de transfert devront être adaptés pour préserver la cohérence mémoire.

Prérequis :
Une bonne connaissance de la programmation C est exigée. La connaissance des fondamentaux de l'architecture des ordinateurs et de la programmation parallèle est également demandée.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Corinne Ancourt (CRI, MINES ParisTech).
E-mail : corinne.ancourt--at--mines-paristech.fr

Stage « Mise en oeuvre efficace d'algorithmes d'inondation sur des grandes images à niveaux de gris » :

Une image à niveaux de gris peut être considérée comme un relief topographique, lorsqu'on attribue à chaque point de l'image une altitude proportionnelle à son intensité de gris. Cette représentation reste valable quel que soit le nombre de dimensions spatiales de l'image ou encore lorsque l'information d'altitude est portée par les poids attribués aux noeuds d'un graphe (éventuellement valué).

Une inondation d'un relief produit un certain nombre de lacs de profondeur quelconque. Un tel relief image représente une nouvelle image à niveaux de gris, plus simple avec moins de vallées que le relief initial. Et bien évidemment, la surface de chaque lac est plate.

L'opération duale de l'inondation consiste à araser les pics. On l'obtient en inondant le négatif d'une image avant de reprendre le négatif du résultat; on arase ainsi les pics. On peut éviter cette double négation et construire directement les opérateurs d'arasement. Ces derniers se déduisent très simplement des algorithmes d'inondation et sont de même complexité. Nous ne nous intéresserons donc ici qu'aux algorithmes d'inondation.

Les deux opérateurs d'inondation et d'arasement sont les ingrédients de base de beaucoup d'opérateurs de filtrage et de segmentation. De nombreuses inondations sont possibles pour un relief donné ; cependant il en existe une seule si on considère la plus haute inondation possible d'une fonction f sous la contrainte d'une fonction plafond g. La fonction g est une fonction quelconque, supérieure ou égale en tout point à la fonction f (comme un seuil d'altitude non nécessairement constant).

L'opérateur d'inondation maximale prend les images f et g en entrée et produit l'image de l'inondation en sortie, laquelle est une image à niveau de gris égale à l'altitude de l'inondation en tout point inondé et au relief f partout ailleurs.

Les algorithmes classiques sont de deux types: les premiers construisent le résultat par balayages itératifs de l'image, tandis que les deuxièmes contrôlent l'inondation au moyen d'une file d'attente hiérarchique. Ces algorithmes sont très lents sur des très grandes images (2D ou 3D), l'objet de stage est donc de les accélérer. On explorera plusieurs voies :

  • Si on a recours à plusieurs coeurs ou processeurs, comment faut-il leur distribuer le travail de la manière la plus efficace ?
  • Etudier le recours à des représentations locales du relief sous forme de flèches entre chaque point et ses voisins plus hauts ou plus bas afin de limiter le nombre d'accès à la mémoire.
  • Réaliser des mises en oeuvre sur processeurs vectoriels ou graphiques. Contacts:

Personnes à contacter :

Envoyer un CV et une lettre de motivation à
Fernand Meyer (fernand.meyer--at--mines-paristech.fr) et
Claude Tadonki (claude.tadonki--at--mines-paristech.fr)

 

Stage « Mise en oeuvre efficace d'un système de localisation de texte enfoui dans des images ordinaires » :

Les OCR (Optical Character Recognition) commerciaux sont de plus en plus performants mais leur utilisation est encore restreinte aux documents numérisés ou aux images prises dans des conditions d'acquisition maîtrisées (support plat, sans effet de perspective, le document occupant la presque totalité de l'image,..). Ils ne sont pas capables de gérer la diversité de styles, les déformations liées à la perspective ou la complexité de l'environnement. La localisation du texte enfoui est une étape nécessaire pour étendre les conditions d'utilisation des OCR existants.

Le CMM (Centre de Morphologie Mathématique) de l'Ecole des Mines de Paris a développé un système de localisation de texte enfoui pour des images tout venant. Ce système a remporté la première place dans la catégorie « localisation de texte » lors de la campagne d'évaluation d'algorithmes de traitement d'images ImagEval. Aucune contrainte temps réel n'était considérée à cette occasion.

Aujourd'hui nous envisageons de porter ces algorithmes sur des dispositifs portables, type smartphone. Pour cela, un travail important de simplification et d'optimisation des algorithmes est nécessaire. Il s'agit de trouver un compromis qualité/performance satisfaisant. En effet, la puissance traitement des systèmes mobiles est modérée, de même que l'approvisionnement en énergie (généralement de modestes batteries). A partir du système mobile, on devrait donc être capable d'acquérir une image avec ses contraintes (résolution et environnement) et d'en extraire les informations textuelles dans un délai acceptable à l'échelle de l'utilisateur. Le texte deviendrait accessible aux personnes malvoyantes ou illettrées (ou ne parlant pas la langue du pays où elles se trouvent) en combinant ce système soit à un module de restitution orale ou à un module de traduction, respectivement. On peut bien sûr imaginer un télétraitement de cette phase dans une approche du type Cloud Computing, mais nous ne l'aborderons pas dans ce stage.

Exigences :
Le candidat retenu pour ce stage aura pour tâche principale d'accélérer un module critique de l'application développée par le CMM, de manière à répondre à l'exigence du compromis qualité/performance mentionné précédemment. Le travail se fera sur des processeurs multi-coeurs standards, très probablement en C. Toutefois, si le candidat a des compétences dans la programmation des systèmes mobiles et si le temps le permet, il pourra étendre sa contribution dans ce contexte-là.

Personnes à contacter :

Envoyer un CV et une lettre de motivation à
Beatriz Marcotegui (beatriz.marcotegui--at--mines-paristech.fr) et
Claude Tadonki (claude.tadonki--at--mines-paristech.fr)

 

Stage « Optimisation et positionnement de sites web sur un sujet à très forte concurrence » :

HEMISPHERE EDUCATION (www.hemisphere-education.com) est un site entièrement dédié à l'accompagnement scolaire à l'aide de supports numériques interactifs, structurés et dynamiques. Son contenu actuel couvre les cycles primaires et secondaires, en plus d'un espace d'initiation réservé aux premiers apprentissages. Aux côtés des cours et des exercices, éditables en ligne par des contributeurs enregistrés, divers outils de travail et d'entraînement sont disponibles. De plus, le site offre un mécanisme de suivi automatique par des tuteurs aux choix.
La concurrence étant très forte dans le domaine de l'éducation numérique, des sites portant sur l'apprentissage scolaire foisonnent sur Internet, ce qui pose un problème de positionnement pour les nouveaux arrivants, même avec un contenu très compétitif et gratuit.

Le but de se stage sera de prendre le cas du site de HEMISPHERE EDUCATION et d'essayer d'en améliorer le positionnement et la visibilité.
Le candidat utilisera les principales techniques proposées dans la littérature (étude statistique et qualitative des mots-clés, échanges de liens, soumission à les moteurs de recherche, annonces ciblées, pour ne citer que ceux-là) et mesurera l'impact de ses actions en analysant diverses métriques issues des statistiques sur le serveurs et ceux fournies par les sites spécialisés.

Exigences :
Bonne connaissance du web et du langage html. Le candidat devra aussi avoir un goût prononcé pour ce type d'activité et une envie de mener une analyse comportementale des internautes.

Personnes à contacter :

Envoyer un CV et une lettre de motivation à
Laurent Daverio (laurent.daverio--at--mines-paristech.fr) et
Claude Tadonki (claude.tadonki--at--mines-paristech.fr)

Stage « Reconstruction d'images à grande échelle sur GPU » :

Description du stage :
Dans le contexte de la simulation de forage, la reconstruction d'une vue principale à partir de vues partielles est une opération importante et récurrente. En plus de la complexité fondamentale de l'algorithme considéré, il faut ajouter celle liée à la résolution des images traités. Comme la plupart des modules de traitement d'images, l'accélération à l'aide de GPUs est devenu un recours naturel. Toutefois, sachant que le principal goulot d'étranglement en ce concerne les GPUs c'est la mémoire et les échanges avec le CPU, la considération des scénaris à grande-échelle (taille et/ou résolution) à performance quasi-constante est un défi technique à étudier. Le but du présent stage est d'explorer les possibilités de mise en oeuvre efficace de la reconstruction d'images à grande échelle sur les GPUs de dernière génération.
Le travail débutera par le déploiement et le profilage du module existant, suivi d'une extension pour la prise en compte des résolutions élevées. La mise au point pourra se faire sur les GPUs disponibles, le passage au GPU Pascal par exemple se fera par la suite.

Exigences :

Le candidat devrait avoir un bon niveau en programmation C et quelques notions de traitement d'images. Des bases en programmation GPU seraient un plus.

Personnes à contacter :

Envoyer un CV et une lettre de motivation à
Claude Tadonki (claude.tadonki--at--mines-paristech.fr) et
Olivier Stab (olivier.stab--at--mines-paristech.fr)

Stage « Maude in Dedukti » :

Context : Dedukti is a type-checker for the lambda-Pi calculus modulo, a type system characterized by two features: dependent types and a conversion rule generated by beta-reduction and rewriting modulo a given set of rewrite rules Preliminary experiments have shown that the reduction algorithm (a modi cation of the virtual machine of Matita that takes into account rewrite rules) behaves well on simple examples coming from Rewriting Logic and has comparable results to Maude.

Subject : The aim of this internship is to go further in this direction, by de ning a transla- tion from Rewriting Logic into Dedukti's format, and by improving the reduction algorithm of Dedukti to become competitive on the whole set of problems with respect to Maude.

Prerequisites : An advanced course on the fundations of computer science such as logic, type theory or rewrite systems. A compiler course would be a plus

Environment : The intern will be hosted by the Deducteam project-team at Inria Paris-Rocquencourt and/or the CRI at MINES ParisTech.

More information in this file.

Personnes à contacter
:

Envoyer un CV et une lettre de motivation à
Olivier Hermant(olivier.hermant--at--mines-paristech.fr)

Stage « Normalization by Completeness » :

Context : Proofs of cut elimination have took two di erent ways for a long time: syntac- tic cut reduction and proofs that this process terminates, and semantic proofs of cut admissiblity.
Recent works tend to show that some unity exist between two methods. The goal of this project is therefore to compare those two approaches, and more speci cally, to force cut admissibility to generate proofs in normal form that are reducts of the original proofs via an adequate reduction relation.
The main framework of interest of this internship will be Deduction Mod- ulo, that provides in particular a uni ed way to study axiomatic theories and axiomatic cuts.

Subject : The internship will rst focus on the study of the pair of theorems soundness/(cut- free) completeness, and on the computational content of such a cut admissibility proof. This can for instance be made through a formalization in a (construc- tive) proof-assistant of the propositional fragment, as did Hugo Herbelin for completeness with respect to Kripke structures.
The next steps will depend on the interests an results of the candidate. That could be for instance:

- carrying the initial proof (in sequent calculus, natural deduction, ...) through soundness and completeness in order to make a formal link between the original proof and the cut-free proof obtained at the very end.
- model transformations that go from Heyting algebras to (extensions of) Kripke structures, in order to compare this work to Normalization by Evaluation. This last step will take us into the world of proof normalization, while we have started by pure semantic proofs of cut admissibility

Prerequisites : At least one advanced course on the fundations of computer science such as logic or type theory. Some notions of category theory would be a plus.

Environment : The intern will be hosted by the Deducteam project-team at Inria Paris-Rocquencourt and/or the CRI at MINES ParisTech.

More information in this file.

Personnes à contacter
:

Envoyer un CV et une lettre de motivation à
Olivier Hermant(olivier.hermant--at--mines-paristech.fr)

Stage « Compilation de Faust en Signal » :

Sujet :
Développement d'un traducteur automatique du langage Faust de traitement du signal audio vers le langage de programmation synchrone Signal.

Projet :
Le langage Faust, développé au Grame (Lyon), permet de spécifier de manière fonctionnelle des opérations de traitement du signal ; il est particulièrement adapté aux applications audio et musicales (http://faust.grame.fr). Le traitement du son se fait, naturellement, de manière synchrone au sein des programmes Faust, et la question de la traduction de ceux-ci vers d'autres formalismes adoptant une approche similaire, tels que Lustre, Signal voire Esterel, se pose. Cette traduction pourrait permettre d'appliquer des analyses et optimisations conçues dans le cadre d'un formalisme synchrone aux programmes Faust.

Ce stage s'insère dans le cadre du projet ANR FEEVER (voir http://feever.fr) qui a pour ambition d'offrir, via Faust, une solution ubiquitaire innovante pour la manipulation multimodale du son. On s'intéressera plus particulièrement aux relations entre Faust et le langage synchrone Signal proposé au sein de l'environnement Polychrony (voir http://www.irisa.fr/espresso/Polychrony) développé par IRISA (Rennes), l'un des partenaires du projet FEEVER.

Descriptif :
L'objet du stage de niveau Master Recherche, de quelques mois, avec prolongation en thèse possible, est, en partant par exemple de l'évaluateur Faustine développé au CRI (voir http://feever.fr/Papers/propFaustine2013.pdf) :

  • d'étudier les spécificités des langages Faust et Signal ;
  • de déterminer un algorithme de traduction du langage Faust, éventuellement dans une version multirate en cours de développement, vers le langage synchrone Signal ;
  • d'étudier les apports de cette traduction, par exemple en termes d'optimisations liées à Signal et son environnement Polychrony.

En fonction du temps disponible, une preuve informatique, en Coq, d'une partie de ce processus pourra être abordée.

Exigences :
Une bonne connaissance de la programmation fonctionnelle (une implémentation du traducteur en OCaml semblerait adéquate) et des techniques de compilation est nécessaire. Un intérêt pour la musique ou les traitements audio est un plus.

Personne à contacter

Envoyer un CV et une lettre de motivation à Pierre Jouvelot (CRI, MINES ParisTech).
E-mail: pierre.jouvelot--at--mines-paristech.fr
Web: http://www.cri.mines-paristech.fr/~pj

Stage « Traitement et mise en ligne des reprographies de La Description de l'Égypte » :

Contexte :
Le fonds historique de la bibliothèque de MINES ParisTech possède un exemplaire complet de l'ouvrage monumental La Description de l'Égypte, réalisé lors de l'expédition d'Egypte organisée par Napoléon Bonaparte.
En 2006, le Centre de recherche en informatique a entamé une opération de mise à disposition sur internet, en accès libre, de l'intégralité des planches d'illustrations de cet ouvrage.
Le travail effectué consiste en la prise de vue et la numérisation des documents (par procédé de reprographie argentique et numérique), la retouche numérique des images et, enfin, le développement de logiciels aptes à pouvoir présenter, en pleine résolution, les fichiers retraités.

La phase du travail nécessitant le plus de moyens humains est la retouche numérique. En outre, ce travail requiert des compétences spécifiques de photographe. Cet état de fait nous a empêché, pour l'instant, de mettre en ligne l'intégralité des images. Nous avons environ un tiers des images effectivement présentées sur le site http://description-egypte.org.

Outre l'attrait historique, scientifique et culturel intrinsèque de cet ouvrage quasi encyclopédique, le temps nous a montré qu'il suscite beaucoup d'intérêt et d'admiration de la part des spécialistes de l'Égypte et aussi du grand public.
Il nous paraît, par conséquent, important d'atteindre le but ultime de l'exhaustivité.

Profil recherché :
Nous sommes à la recherche d'un(e) spécialiste ayant des compétences de photographe et une grande maîtrise de la retouche numérique avec le logiciel Adobe Photoshop pour réaliser ce travail de finition, par exemple dans le cadre d'un stage de quelques mois.

La connaissance de Photoshop Lightroom est également nécessaire.

Un intérêt pour l'histoire en général et/ou pour le sujet en particulier sera un avantage apprécié.

Étant donné le type de travail à effectuer, des aménagements d'horaire et de lieu de travail peuvent être envisagés.

Personnes à contacter

Envoyer un CV et une lettre de motivation à Benoît Pin ou François Irigoin (CRI, MINES ParisTech).
E-mail: benoit.pin--at--mines-paristech.fr (01 64 69 49 83 )
E-mail: francois.irigoin--at--mines-paristech.fr (01 64 69 47 08

Stage « Analyse statique de performance pour le langage audio Faust » :

Sujet :
Développement d'un analyseur automatique automatique WCET (Worst-Case Execution Time) pour le langage Faust de traitement du signal audio et musical.

Projet :
Le langage Faust, développé initialement au Grame (Lyon), permet de spécifier de manière fonctionnelle des opérations de traitement du signal ; il est particulièrement adapté aux applications audio et musicales (http://faust.grame.fr). Le traitement du son se fait, naturellement, de manière synchrone au sein des programmes Faust, et la question de la performance de ce langage se pose. En effet, un langage synchrone se doit d'être conforme à ce qu'on appelle "Hypothèse synchrone", qui stipule que tous les traitements peuvent être exécutés entre les arrivées de deux échantillons sonores successifs. Pour cela, une analyse statique de cout, du genre WCET (Worst-Case Execution Time), de ces traitements est nécessaire au moment de la compilation pour vérifier que cette hypothèse est valide, assurant ainsi la correction du code Faust à exécuter.

Ce stage s'insère dans le cadre du projet ANR FEEVER (voir http://feever.fr) qui a pour ambition d'offrir, via Faust, une solution ubiquitaire innovante pour la manipulation multimodale du son.

Descriptif :
L'objet du stage de niveau Master Recherche, de quelques mois, avec prolongation en thèse possible, est, en partant par exemple de l'évaluateur Faustine développé au CRI (voir http://feever.fr/Papers/propFaustine2013.pdf) :

- d'étudier les techniques actuelles d'analyse WCET;
- de concevoir et d'implanter via Faustine un algorithme d'analyse WCET pour le langage Faust;
- si le temps le permet, d'en faire une version C++ à intégrer dans le compilateur Faust.

Egalement en fonction du temps disponible, une preuve informatique, en Coq, d'une partie de ce processus pourra être abordée.

Exigences :
Une connaissance de la programmation fonctionnelle et des techniques de compilation est nécessaire. Un intérêt pour la musique ou les traitements audio est un plus.

Personnes à contacter

Envoyer un CV et une lettre de motivation à Pierre Jouvelot (CRI, MINES ParisTech).
E-mail: pierre.jouvelot--at--mines-paristech.fr
Web: http://www.cri.mines-paristech.fr/~pj

Stage « Type refinement in λΠ-calculus modulo » :

Context :
Dedukti is an experimental language designed to write proof checkers for logics. It is used to implement independent proof checkers for proof assistants such as Coq and Isabelle and trace checkers for automated deduction tools such as Zenon and iprover modulo.
The logic underlying Dedukti is called λΠ-modulo : it is an extension of λΠ, the simplest form of dependently typed λ-calculus (called λP in), with user-defined rewriting rules for type equality (a.k.a. conversion).

Subject :
Writing a checker in Dedukti can be split in two phases: developing the theory of the target tool, and writing a translator from the tools syntax to Dedukti's. This internship aims at making the former task, which amounts to writing programs in Dedukti, more tractable.
Dedukti is organised in a way which is reminiscent of proof assistants. It is split into a small kernel, which is tasked with verifying that a term with type annotations is well-typed, and a front-end which takes the program as written by the user and elaborates it into a term which the kernel understands. In principle, the user-level language may differ significantly from the kernel-level language. The front-end is, for instance, usually expected to perform some type inference, whereas it is not the rôle of the kernel. In Dedukti, however, the front-end stops just short of being the identity: the programmer essentially uses the kernel language directly.

To remedy this unfortunate situation, Dedukti needs to be outfitted with a type inference engine. Type inference in dependently typed language fuses with unification and proof search. The main inspiration for such a type inference engine is the proof-search engine used by Coq.
This proof-search engine is meant to be a safe and universal abstraction to manipulate terms with holes. The large amount of pre-existing code in Coq meant, however, that only interactive demonstrations use this abstraction, and specifi- cally not the type inference or unification mechanisms. We would like to take advantage of the experimental status of Dedukti and improve on this design by 1actually expressing type inference and unification in terms of the proof-search abstraction.
This line of research contains both theoretical and practical programming aspects. The internship can be geared towards on or the other depending on the student's preferences.
On the programming side, the proof-search abstraction must be integrated with Dedukti's kernel by means of enriching the syntax of terms with so-called existential variables – also known as unification variables or meta-variables. This change must be made with as little disruption as possible on the kernel side. The design should improve on Coq's by providing two kinds of existential variables: the regular ones and existential variables standing for contexts. This new kind of existential variable was introduced by Lengrand for theoretical reason pertaining to unification and saw other successful application in the Matita proof assistant. Another aspect to consider is that Coq's abstraction was done with the knowledge that unification was handled somewhere else, and hence features no abstraction for unification problems, which will have to be developed as part of this work.
On the theoretical side, the λΠ-calculus modulo needs a good theory of unification expanding on the work of Dowek for pure type systems. Higherorder unification is undecidable in the case of simply typed λ-calculus. It is even more so in the very expressive λΠ-calculus modulo. This prevents us from achieving a decision procedure for unification, but we can devise a set of deduction rules which, provided an oracle, solves unification. The addition of rewriting rules in the conversion the λΠ-calculus modulo changes significantly the shape of normal forms with respect to pure type systems. A good understanding of these normal form must be achieved, in order to derive an appropriate set of rules to describe unification strategies in the λΠ-calculus modulo.

Practical information :

The internship will be supervised by Olivier Hermant.
It will be hosted by the Deducteam project-team at Inria Paris-Rocquencourt and the cri at Mines ParisTech.

More information in this file

Personnes à contacter :

Envoyer un CV et une lettre de motivation à
Olivier Hermant(olivier.hermant--at--mines-paristech.fr)

 

Stage « Verified Computation of Fourier Transforms » :

Overview :
The goal of this internship is to investigate the formal computation of Fourier transforms in Coq, using as a base the Mathematical Components library [1] for specification and CoqEAL [2] for computation.

Detailed Description :
The CoqEAL [2] library is a recent Coq library enabling verified, efficient computation of linear algebra programs. CoqEAL provides efficient algorithms, along with proofs of extensional equivalence to their high-level, proof-oriented counterparts.

The goal of the internship is to explore CoqEAL for the verified computation of Fourier transforms of sampled signals. In particular, the Discrete Fourier Transform (DFT) can be expressed as the matrix multiplication Wx of W, the Vandermonde matrix for the roots of unity, and x, the input signal.

In principle, the mathematical components library [1] already provides most of the tools needed to specify the DFT, such as algebraic numbers and constructive linear algebra. Thus, the first phase of this internship is to specify and compute the DFT in a clean, low-effort way, bootstrapping the project.

Once this first phase is completed, an advanced topic could be to implement and verify the FFT algorithm inside the mathcomp/CoqEAL framework.

Other relevant efforts for verified DFT/FFT can be found at [3,4,5].

Desired qualifications and interests :

The student should be familiar with linear algebra, type theory and Coq. Prior knowledge of DSP theory and ssreflect/mathcomp libraries is a plus.

Contact :

E-mail: Emilio Jesús Gallego Arias or Pierre Jouvelot
Web: http://www.cri.mines-paristech.fr/~pj

References :

[1] http://ssr2.msr-inria.inria.fr/
[2] https://github.com/CoqEAL/CoqEAL
[3] http://www.duplavis.com/venanzio/publications/FFT_TPHOLs_2001.pdf
[4] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.2468
[5] http://hvg.ece.concordia.ca/Publications/Conferences/37_FMCAD'04.pdf

Stage « Stream and Window-based Processing in Javascript » :

Overview :
The goal of this internship is to study the base building blocks for efficient spectral audio processing in WebAudio/Javascript.

Detailed Description and Goals :
The WebAudio API[0] enables easy and flexible audio processing in the browser. WebAudio is defined around an audio node model, providing a predefined set of audio processors, and a callback-based facility (AudioWorkerNode) for user-defined processing. See [1] for some thoughts on the matter.

However, we believe that the current specification provides little support for efficient and reusable implementation of spectral processing. Ring buffering, windowing, and sharing are left unspecified, and must be accommodated to the fixed-width AWN window.

The goal of this internship is both to study how existing approaches for stream processing in Javascript perform ([2,3,4,5,6,7,8]), and to develop a new abstraction library on top of AudioWorkerNode if needed. The new library should facilitate efficient frequency-domain programming by taking care of low level, buffering details. In particular, the student is expected to implement two non-trivial spectral processing algorithms (like [9]) and study its performance.

Desired qualifications and interests :

The student should be familiar with Audio DSP, spectral processing and JavaScript. Experience with Faust/Matlab will be a plus.

Contact :

E-mail: Emilio Jesús Gallego Arias or Pierre Jouvelot
Web: http://www.cri.mines-paristech.fr/~pj

References :

[0] http://webaudio.github.io/web-audio-api/
[1] https://github.com/WebAudio/web-audio-api/issues/468
[2] http://streamjs.org/
[3] http://highlandjs.org/
[4] https://github.com/darach/eep-js
[5] https://github.com/dntj/jsfft
[6] http://p5js.org/learn/examples/Sound_Frequency_Spectrum.php
[7] https://www.npmjs.com/package/fft
[8] http://mohayonao.github.io/timbre/documents/fft.html
[9] https://code.soundsoftware.ac.uk/projects/constant-q-cpp

Stage « Efficient Switching for Audio Processing Components » :

Overview :
The topic of this internship is to study formally audio plugin containers (or racks) with efficient runtime switching/routing of components.

Detailed Description :
In digital audio programming, the chaining of several processing components is a common setup. For instance, a guitar effects processor such as guitarix [3] will link dozens of filters/effects in regular operation, with the user enabling and disabling some components as she advances through the performance.

However, when a component is disabled, the software has to pay for its computational cost (maintaining internal state of the component) or risk glitches/noise when the user enables the component in the future (think for instance of a delay processor). Some common remedies introduce additional crossfade/latency at switch-on time, alleviating this situation, but are usually tuned in an informal basis and lack formal support.

We propose to study the problem of dynamic switching of audio components in the language Faust [1]. The goal will be to understand the conditions for safe disabling of particular audio components, such that output is equivalent to simply muting them with an output gain of 0. As an example, we conjecture that n-order FIR filters can be effectively disabled at the cost of introducing a latency of n samples. For IIR filters, an approximate bound could be used, or even numeric reasoning about floating point error could give absolute guarantees.

Some related fields where the intern could get ideas from are incremental/self-adjusting computation and hierarchical controllers in the embedded/synchronous systems literature.

Desired qualifications and interests :

The student should be familiar with audio, floating point and DSP programming. Experience with Faust and synchronous systems will be a plus.

Contact :

E-mail: Emilio Jesús Gallego Arias or Pierre Jouvelot
Web: http://www.cri.mines-paristech.fr/~pj

Joint research with Jean-Pierre Talpin at IRISA, Rennes.

References :

[1] http://faust.grame.fr/
[2] http://kxstudio.sourceforge.net/Applications:Carla
[3] http://guitarix.org/

Stage « Wagner: Formal Models for Sound Processing » :

Overview :
Wagner [1] is a new functional synchronous language (see for instance [2], ask us for many more references) aimed at both efficient audio processing and formal semantics.
Wagner aims to extend other existing frameworks such as Faust or the more recent Audio System Toolbox

Detailed Description :
Wagner Typing and Semantics: Wagner type system is based on co-effects and a simple notion of type polarity, with a straightforward operational semantics, and a more efficient virtual machine related to the original semantics via logical relations.
You will work with us in extending the type system and improving the operational semantics and proofs. Students should be familiar with the theory of type systems for functional programming languages.

Mechanized Semantics: We have developed basic Wagner model mechanized in Coq/MathComp, enough to already prove quite interesting properties. You will extend this model to accommodate some additional features, as well as complete the part pertaining to Wagner’s VM.
Some proficiency in Coq plus a basic understanding of the mathematical components library is recommended. We’d be happy however to take a candidate willing to learn the library.

Type Inference and Compilation: We have develop a preliminary Ocaml-based compiler for Wagner; the compiler is capable of performing some basic type inference and code generation. You will work on improving the type inference strategy by adding bidirectional type checking, and improve the current interpreter for Wagner’s VM.

Desired qualifications and interests :

Familiarity with Ocaml and type inference is recommended.

Contact :

E-mail: Emilio Jesús Gallego Arias or Pierre Jouvelot
Web: http://www.cri.mines-paristech.fr/~pj

References :

[1] E. J. Gallego Arias. Experiments in Certified Digital Audio Processing. 1h Seminar. http://www.cri.ensmp.fr/people/gallego/slides/SpecFun-04-2016/. 2016.

[2] A. Guatto. “A Synchronous Functional Language with Integer Clocks”. PhD thesis.École Normale Supérieure Paris, 2016.

Stage « jsCoq: New Interfaces for Interactive Theorem Proving » :

Overview :
The jsCoq [2] project is a port of the Coq proof assistant to the web browser platform. jsCoq allows to write web pages with embedded proof scripts, opening up significant new possibilities of interaction and distribution.

Detailed Description :
Coq Backend the SerAPI [1] protocol is an new protocol for machine-based interaction with Coq, used in jsCoq, PeaCoq, and experimentally by CoqIDE.
We propose to extend the protocol in two ways:
a) improve the control protocol to better suit document-oriented environments such as Emacs or the Web DOM;
b) improve the query subprotocol, which powers code completion, display, and proof analysis tools.

Web Frontend we propose to integrate the frontend with IPython’s 1 web libraries, to improve integration with documentation generation tools, and to improve search, pattern, type, and goal display.
We are open to other ideas. All our projects are open source and available at github.

Desired qualifications and interests :

Basic familiarity with Coq and proof workflow. Particular requisites for each part are:
Coq Backend Fluency in Ocaml is recommended.
Web Frontend Fluency in JavaScript and UI web libraries is recommended.

Contact :

E-mail: Emilio Jesús Gallego Arias or Pierre Jouvelot
Web: http://www.cri.mines-paristech.fr/~pj

References :

[1] E. J. Gallego Arias. “SerAPI: Machine-Friendly, Data-Centric Serialization for COQ”. Working paper or preprint. Oct. 2016.

[2] E. J. Gallego Arias, B. Pin, and P. Jouvelot. “jsCoq: towards hybrid theorem proving interfaces”. In: Proceedings of the 12th Workshop on User Interfaces for Theorem Provers. 2016.

Stage « Personnalisation d'avatar compagnon pour personnes atteintes de la maladie d'Alzheimer » :

Sujet :
Développement d'un cadre de réflexion pour la personnalisation d'un environnement informatique pour patients atteints de troubles cognitifs apparentés à la maladie d'Alzheimer.

Projet :
Le projet Louise est mené depuis près de trois ans en collaboration par le Centre de recherche en informatique (CRI) de MINES ParisTech et le Centre d'expertise nationale en stimulation cognitive (CEN STIMCO), situé à l'hôpital Broca. Son objectif consiste à étudier l'applicabilité des technologies issues des jeux videos, et plus particulièrement des agents conversationnels humanoïdes (Embodied Conversational Agent), pour l'assistance des personnes âgées souffrant de déficits cognitifs.

Un premier prototype de Louise visant à étudier la gestion de l'attention chez les patients déments a été développé et testé avec des spécialistes du soin, des aidants et des patients dans le cadre du LUSAGE, un « living lab » situé également à l'hopital Broca. Une publication sur le sujet, "Towards Attention Monitoring of Older Adults with Cognitive Impairment During Interaction with an Embodied Conversational Agent", 3rd IEEE VR International Workshop on Virtual and Augmented Assistive Technology (VAAT), pp. 23-28, Arles, France, March 2015, est disponible via
https://hal-mines-paristech.archives-ouvertes.fr/hal-01137307.

Descriptif :

L'objet du stage de recherche-innovation proposé dans le cadre du projet Louise, de quelques mois, avec prolongation en thèse possible le cas échéant, consiste, en partant de l'expérience gagnée par le CRI et le CEN STIMCO :

  • à s'approprier la littérature scientifique, l'outil et les technologies au coeur de l'environnement Louise;
  • à réfléchir, en collaboration avec les médecins, psychologues, anthropologues (CEN STIMCO) et chercheurs en informatique (CRI), à la possibilité d'étendre les fonctionnalités et domaines d'applications de Louise, en particulier en direction de la personnalisation de l'avatar en fonction des spécificités des patients avec lesquels il interagit;
  • à en valider la pertinence par une implémentation dans le prototype Louise, voire via des tests dans le cadre de LUSAGE.

Exigences :

Une connaissance de la programmation, si possible C++, est nécessaire. Un intérêt pour la robotique, l'application des nouvelles technologies au soin ou les jeux vidéo est un plus.

Personne à contacter :

Envoyer un CV et une lettre de motivation à Pierre Jouvelot (CRI, MINES ParisTech).
E-mail: pierre.jouvelot--at--mines-paristech.fr
Web: http://www.cri.mines-paristech.fr/~pj