From Event-B to Lambdapi

Anne Grieu
Digital Printed Abstract View Cite
Type
Conference paper
Publication
10th International Conference on Rigorous State Based Methods (ABZ'24)

Abstract

B, Event-B and TLA+ are modelling notations based on set theory. Dedukti/Lambdapi is a logical framework based on the (\lambda \Pi )-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.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{Grieu24,
  author       = {Anne Grieu},
  editor       = {Silvia Bonfanti and
                  Angelo Gargantini and
                  Michael Leuschel and
                  Elvinia Riccobene and
                  Patrizia Scandurra},
  title        = {From Event-B to Lambdapi},
  booktitle    = {Rigorous State-Based Methods - 10th International Conference, {ABZ}
                  2024, Bergamo, Italy, June 25-28, 2024, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {14759},
  pages        = {387--391},
  publisher    = {Springer},
  year         = {2024},
  url          = {https://doi.org/10.1007/978-3-031-63790-2\_29},
  doi          = {10.1007/978-3-031-63790-2\_29},
  timestamp    = {Thu, 04 Jul 2024 22:05:23 +0200},
  biburl       = {https://dblp.org/rec/conf/zum/Grieu24.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
ABZ'24

Related