Composants et Coalgèbres
Le but du stage est d’amorcer une étude sémantique de la notion de composants logiciels telle que proposée dans le modèle Fractal en utilisant une approche coalgébrique. Le sujet est détaillé ici.
Modélisation de HOCore en Coq
HOCore est un calcul de processus minimal, semblable à un lambda-calcul concurrent, possédant l’étrange propriété d’être Turing puissant (donc la terminaison est indécidable) mais dont la notion d’équivalence naturelle est décidable.
L’objectif de ce stage est de prouver ce résultat dans l’assistant de preuve Coq, en se basant sur les techniques développées dans le cadre du projet ANR PiCoq. Cette modélisation présente de nombreuses opportunités de développement: encodage de machines de Minsky, preuves impliquant différentes formes de bisimulations, ou encodage du problème de correspondance de Post.
Ce stage aura lieu dans l’équipe-projet Celtique, au centre de recherche de l’INRIA Rennes, et sera encadré par Alan Schmitt. Le stage pourra être rémunéré.
HOCore et localités
HOCore est un calcul de processus minimal, semblable à un lambda-calcul concurrent, possédant l’étrange propriété d’être Turing puissant (donc la terminaison est indécidable) mais dont la notion d’équivalence naturelle est décidable.
Un premier objectif de ce stage est d’étendre HOCore avec une notion de localité permettant la capture de processus en cours d’exécution et d’établir si l’équivalence observationnelle reste décidable. Un second objectif consiste à étudier l’expressivité apporté par les localités ainsi que l’interaction entre localités et envoi de messages. Enfin, un étudiant motivé pourra aborder le problème très difficile de l’équivalence faible.
Ce stage aura lieu dans l’équipe-projet Celtique, au centre de recherche de l’INRIA Rennes, et sera encadré par Alan Schmitt. Le stage pourra être rémunéré.