Positionnement vis-à-vis des autres projets issus de CROAP

Des membres de l'ex-équipe CROAP font partie d'autres propositions de projets. Il est important de positionner les activités de Lemme par rapport à la thématique de ces projets :

• OASIS : la thématique d'OASIS qui se rapproche le plus de nos centres d'intérêt est la certification de programmes Java. L'approche d'OASIS est inverse de la nôtre. Il s'agit, avec des outils et méthodes héritées de Centaur, d'étudier la sémantique de programmes Java et d'en prouver des propriétés.

• TROPICS : La différentiation automatique est un candidat naturel pour l'application de nos techniques de certification. Cependant l'investissement nécessaire pour espérer s'attaquer aux problèmes que se propose de résoudre TROPICS est pour le moment trop important. Mais l'analyse réelle progressant dans sa formalisation en théorie des types, on peut raisonnablement penser qu'il sera possible dans un futur proche de s'attaquer à des algorithmes simples. C'est une voie possible de collaboration future de notre projet avec TROPICS, et aussi avec le projet Coq qui commence une étude de la certification d'Odyssée (Gilles Dowek et Micaela Mayero).

• CERTILAB : la thématique du projet CERTILAB se concentre autour de la sémantique des langages de programmation. Ce domaine est éloigné des préoccupations premières de Lemme. Cependant certaines collaborations en cours (Génie et Types) continueront.