Métaprogrammation en Lean4 : expérimentation pour Event-B

Objectif

Lean4 est un environnement de programmation fonctionnelle à types dépendants qui possède des fonctionnalités étendues de méta-programmation. A titre d’exemple, Lean4 est également un assistant de preuve interactif, et cette fonctionnalité est intégralement implémentée au dessus du langage de base en exploitant ces outils de méta-programmation. Dans le cadre d’un cours de Master, nous avons développé une bibliothèque pour Lean4 permettant de modéliser des systèmes logiciels ou logiciels/matériels selon les concepts de la méthode Event-B. Pour l’instant, les constructions syntaxiques utilisées par cette librairie sont les constructions proposées nativement par Lean4. Dans le cadre de ce stage, nous souhaitons développer des constructions syntaxiques plus proches des constructions originales de Event-B, par exemple celles utilisées dans le cadre des plateformes Rodin et Atelier-B.

Tâches à réaliser

Dans un premier temps, il s’agira de prendre en main l’environnement Lean4 qui s’apparente à un langage de programmation fonctionnel typé comme Ocaml ou Haskell, avec un système de type beaucoup plus “riche” (mais que nous n’exploiterons pas directement dans le cadre du stage). On s’intéressera bien sûr en priorité aux fonctionnalités de méta-programmation, avec par ordre de “technicité” : les notations, les macros hygiéniques et l’élaborateur programmable. Pour prendre en main ces fonctionnalités, on commencera par implémenter des structures syntaxiques très simples, puis, graduellement, nous essaierons de développer des structures plus complexes associées à notre bibliothèque “Event-B” : spécifications de machines, d’événements et d’étapes de raffinement.

Prérequis

• un intérêt pour la programmation fonctionnelle typée (Ocaml, Haskell, Scala, …)
• un intérêt pour les langages de programmation en général : la compilation (plutôt frontend/middlend que backend) et les expérimentations “linguistiques”

Références

• Lean4 programming language and proof assistant : https://lean-lang.org/
• Functional programmin in Lean4 : https://lean-lang.org/functional_programming_in_lean/
• Lean4 metaprogramming : https://leanprover-community.github.io/lean4-metaprogramming-book/
• Event B / Rodin : https://www.event-b.org/index.html
• Atelier B : https://www.clearsy.com/outils/atelier-b/

Le stagiaire devra être d'accord pour que ses contributions soient distribuées sous licence libre.

Contacts : Frédéric Peschanski (équipe APR - LIP6 - Sorbonne Université)