From Event-B to Lambdapi
Résumé
B, Event-B and TLA+ are modelling notations based on set theory. Dedukti/Lambdapi is a logical framework based on the λΠcalculus modulo rewriting in which many theories and logics can be expressed. In the context of ICSPA (ANR project), Lambdapi will be used to exchange models and proofs between the set theory-based formal methods B, Event-B and TLA+. They will rely on the encoding of the respective set theories in Lambdapi. Our current work focuses on translating the mathematical language of Event-B and proof trees obtained with the Rodin platform for Event-B.
| Origine | Fichiers produits par l'(les) auteur(s) |
|---|