Nubo
Nubo
La bibliothèque universelle des preuves formelles
Nubo améliore et facilite la sûreté de fonctionnement et la vérification des systèmes informatiques en répondant au problème de disparité des preuves formelles, engendré par l’absence de standard et le manque d’interopérabilité des systèmes de preuves existants.
Cette base de données de preuves, traduites dans un formalisme commun facilement vérifiable*, permet aux informaticiens et aux mathématiciens de réutiliser une théorie dans un autre système, sans redémontrer toutes les preuves.
*Cette suite logicielle nommée Dedukti est également développée par l’équipe DEDUCTEAM.
L’absence de dysfonctionnements doit être garanti dans de nombreux domaines tels que les systèmes de transport, la production d’énergie, les chaînes de production de médicaments, les systèmes financiers, la robotique chirurgicale, les applications militaires…
Points forts :
- Nubo contient des démonstrations dans les 7 systèmes les plus utilisés dans le monde : Isabelle, Zenon, Iprover, VeriT, Focalize, Matita, Hol Light.
- Nubo a pour vocation de devenir une bibliothèque universelle de preuve formelle, en rassemblant une large communauté de contributeurs industriels et académiques, ainsi que d’organismes certificateurs.
Pour aller plus loin :
- Raphaël Cauderlier, Catherine Dubois. ML Pattern-Matching, Recursion, and Rewriting: From FoCaLiZe to Dedukti. ICTAC 2016 – 13th International Colloquium on Theoretical Aspects of Computing, Oct 2016, Taipei, Taiwan. pp.459-468, ⟨10.1007/978-3-319-46750-4_26⟩
- François Thiré. Sharing a Library between Proof Assistants: Reaching out to the HOL Family *. Electronic Proceedings in Theoretical Computer Science, EPTCS, 2018, 274, pp.57 – 71.
- Ali Assaf, Guillaume Burel, Raphaël Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti: a Logical Framework based on theλΠ-Calculus Modulo Theory. 2016
L'équipe Deducteam
L’équipe Deducteam explore les applications de la théorie de la démonstration à la conception de cadres logiques, à l’interopérabilité entre systèmes de preuves et à la construction de bibliothèques mathématiques universelles.
En savoir plus sur l'équipe