Projet de recherche en informatique théorique axé sur la vérification formelle de preuves mathématiques et le développement de tactiques dépendantes dans le langage Meta Dedukti. Il permet d'assurer la correction et la fiabilité des démonstrations logiques et mathématiques à l'aide de méthodes formelles avancées.

Ce projet est la bibliothèque standard du Rocq Prover, un assistant de preuve interactif. Il propose un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, accompagnés d'un environnement pour développer des preuves vérifiées par machine. La bibliothèque standardise et organise les modules essentiels pour les utilisateurs et développeurs, favorisant ainsi la rigueur et la réutilisabilité dans les travaux de preuve formelle.

Ce projet propose une traduction automatique d'une partie de la bibliothèque HOL-Light vers le système Rocq. Il permet d'aligner des types et fonctions mathématiques entre ces deux environnements de preuve formelle, facilitant ainsi l'utilisation de théorèmes HOL-Light dans Rocq. L'objectif est d'accélérer le développement de preuves formelles en exploitant des résultats déjà établis dans HOL-Light, tout en garantissant leur compatibilité avec Rocq.

Ce projet propose une collection de modules et de fonctionnalités destinées à enrichir la bibliothèque standard de Rocq, un assistant de preuve formelle. Il vise à faciliter le développement de preuves mathématiques et logiques en fournissant des outils réutilisables et des abstractions supplémentaires.

Ce projet fournit une traduction en Coq de la définition des nombres réels dans HOL-Light, en utilisant le type nat de Coq. Il permet de formaliser des concepts mathématiques avancés et de vérifier des preuves automatiquement. La bibliothèque est générée à partir de HOL-Light et peut être utilisée pour des développements formels en mathématiques ou en informatique théorique.

Kôika-SUSHI est un langage de conception matérielle basé sur des règles, intégré dans Rocq. Il permet de développer et de vérifier formellement des circuits électroniques, notamment des processeurs. Ce projet facilite la création de matériel fiable et optimisé grâce à des preuves mathématiques intégrées, en s'appuyant sur des approches de réécriture progressive et des outils SMT pour renforcer la robustesse des designs.

VsRocq est une extension pour Visual Studio Code et VSCodium qui fournit un support avancé pour le prouveur interactif Rocq (anciennement Coq). Il permet aux utilisateurs de vérifier des preuves mathématiques, de développer des logiciels certifiés et d'enseigner la logique formelle grâce à une intégration fluide avec l'éditeur. L'outil offre des fonctionnalités comme la vérification continue des preuves, une interface interactive pour explorer les objectifs de preuve et un panneau dédié aux requêtes.

Coq est un système de gestion de preuves formelles. Il fournit un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves formelles vérifiables par machine.

Coq est un système de gestion de preuves formelles. Il offre un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves machine-checkées.

Coq est un système de gestion de preuves formelles. Il fournit un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, ainsi qu'un environnement pour le développement semi-interactif de preuves vérifiées par ordinateur.