L'objectif de ce stage est de implémenter un système d'effets sur un langage noyau de smart contracts basé sur les PSS que nous avons mis en place au CEA List. Les effets algébriques permettent au programmeur de formaliser le comportement computationnel attendu du programme, qui est encodé dans le type du programme et automatiquement vérifié en temps de compilation par le type checker. Le système d'effets que nous envisageons possède des propriétés avancées telles que la composabilité, les effets d'ordre supérieur et la dépendance de type. Les effets computationnels à prendre en compte comprennent la termination, les exceptions, la consommation de gaz bornée, les changements de l'état des smart contracts, les changements des balances des comptes, etc.

Une spécification de haut niveau du système d'effets sera disponible et remise au stagiaire. Le candidat interagira avec des chercheurs et des ingénieurs spécialisés dans la technologie blockchain et la théorie des langages de programmation.

Le candidat retenu rejoindra le Laboratoire des systèmes d'information fiables, intelligents et auto-organisés (LICIA) du CEA List.

Le stagiaire aura les responsabilités suivantes :

1. Se familiariser avec l'état de l'art en matière de typage statique et des systèmes d'effets algébriques.
2. Se familiariser avec le langage noyau de smart contracts basé sur les PSS mis en place au CEA List, et avec la spécification du système d'effets qui sera remise au stagiaire.
3. Étendre le langage de smart contracts développé au CEA List en mettant en place un système d'effets d'après la spécification remise au stagiaire, et produire une implémentation réaliste du dit langage (telle qu'un interpréteur efficace ou une machine virtuelle).
4. Vérifier l'exactitude de l'implémentation réaliste en effectuant des tests et des benchmarks.
5. Documenter le développement du système d'effets en rédigeant un rapport technique et/ou en collaborant à un article scientifique.