B, Event-B et TLA sont des méthodes formelles basées sur la théorie des ensembles. Dedukti/Lambdapi est un framework logique basé sur le λΠ-calcul modulo dans lequel de nombreuses théories peuvent être exprimées. Dans le projet ANR ICSPA, Lambdapi a été choisi pour échanger les méthodes formelles basées sur la théorie des ensemble B, Event-B et TLA.

Nous allons présenter plus particulièrement certains choix et questionnements concernant l'encodage du langage mathématique d'Event-B et des preuves produites par la plate-forme Rodin, en nous appuyant sur la construction du langage mathématique d'Event-B et sa représentation en Lambdapi. Nous présenterons aussi la représentation des preuves dans Rodin et les propositions de transcription dans Lambdapi.