Le langage de programmation Fortress est un langage généraliste, typé statiquement, basé sur la programmation par composants et est conçu pour le développement de logiciel robuste haute-performance. Il est développé dans le Programming Language Research Group de Sun microsystems. Il pourrait être un successeur de Java.
La spécification du langage est informelle et en partie formalisée. Pour raisonner sur les programmes Fortress et pour obtenir un évaluateur à partir d'une sémantique formelle, cette spécification doit être étendue. Pour plus de sûreté, la sémantique pourrait être modélisée dans un assistant de preuve et les preuves associées réalisées à l'aide d'un prouveur interactif tel que l'assistant de preuve Coq.
Le stage consistera dans un premier temps à établir un état de l'art sur la sémantique des langages de programmation apparentés à Fortress et aux techniques de modélisation et de preuves associées.
Dans un second temps, la sémantique formelle telle que décrite dans le document de spécification de Fortress, devra être modélisée en Coq et ses propriétés prouvées à l'aide de cet assistant de preuve.
Enfin dans une troisième partie, ce noyau formalisé de Fortress devra être étendu pour prendre en compte un sous-ensemble plus large du langage.