From Event-B to Lambdapi (Journées FAC 2024)
Résumé
We will here focus on Event-B with the Rodin Platform, an Eclipse-based IDE and logical framework (Java-based) for Event-B. In this first work, our aim is to check the proof trees generated by Rodin. For this purpose, we use the Lambdapi framework. We present the translation of Event-B constructs based on the set theory (first order equational classic logic, set based-logic) and some deduction rules. We also discuss how the specific rules of Event-B related to set theory are translated.
Domaines
Théorie et langage formel [cs.FL]Origine | Fichiers produits par l'(les) auteur(s) |
---|