Les grammaires catégorielles sont des formalismes très généraux basés sur des systèmes d'inférence logiques et dédiés à l'analyse des langues naturelles. Elles ont l'avantage de garantir une interface syntaxe/ sémantique aisée. Plusieurs modèles logiques enrichis ont été récemment définis pour rendre compte de différents phénomènes linguistiques assez complexes. Toutefois, l'adéquation de ces formalismes vient au détriment de leur simplicité et leur complexité d'analyse. Nous réalisons un outil destiné à la recherche et l'enseignement de la linguistique computationnelle, permettant d'appréhender ces modèles, en construisant des analyses syntaxiques de phrases et leur interprétation sémantique, mais aussi en établissant des propriétés de classes entières de langages et en étudiant les relations entre divers formalismes. Cet outil : l'atelier ICHARAT E, est composé de bibliothèques pour l'assistant à la démonstration Coq. Nous décrivons dans cet article les principales fonctionnalités de cet atelier, en montrant comment il répond aux besoins exprimés ci-dessus.