Outil dédié à la génération automatique de parseurs et générateurs de code à partir de grammaires définies. Il simplifie la création d'analyses syntaxiques pour des langages spécifiques, réduisant ainsi le temps de développement des compilateurs et outils d'analyse. Idéal pour les développeurs et équipes travaillant sur des projets nécessitant une manipulation avancée de langages formels.

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.

Ce projet propose une sémantique formelle pour le langage de programmation Erlang, axée sur l'ordre des messages et la gestion des signaux. Il vise à simplifier la représentation du parallélisme et de la concurrence, tout en offrant une modélisation des comportements de surveillance et de gestion des exceptions. Les fonctionnalités telles que la création dynamique de processus, la représentation du temps continu ou la mise à jour dynamique du code ne sont pas prises en charge.

SYNTAX est un générateur de parseurs syntaxiques permettant d'analyser du code source et de générer du code à partir de grammaires formelles. Il facilite la création de langages de programmation dédiés et spécialisés.