STAGE Implémentation, optimisation et tests d'une traduction de programme

Contexte :

Le système T est un langage de programmation abstrait muni de types fonctionnels de tout ordre, basés sur le
type des entiers. Le système F [1] est une extension du système T par des types polymorphes paramétriques.
La récursion barrée [2] est une autre extension du système T par un opérateur de récursion sur des arbres
implicitement bien fondés.
D'un point de vue logique, le système T permet d'interpréter l'arithmétique du premier ordre, alors que
ses extensions que sont le système F et la récursion barrée permettent toutes deux d'interpréter l'arithmétique
du second ordre.
Bien que ces deux interprétations calculatoires de l'arithmétique du second ordre fournissent des programmes
au comportement fondamentalement différent, j'ai pu définir en 2017 une traduction du système F
vers la récursion barrée. Cette traduction remplace donc les types polymorphes par des appels à un opérateur
de récursion.
Afin de mieux comparer les comportements calculatoires des programmes source et cible de cette traduction,
il est nécessaire d'implémenter celle-ci.