Les langages applicatifs, de par la facilité de prototypage et l'expressivité qu'ils apportent, jouent un rôle croissant dans la programmation des logiciels dont la sûreté est prépondérante. La chaîne de développement de ces logiciels sûrs s'appuie sur un ensemble d'outils, de la conception en amont à la phase de validation en aval : spécification formelle, test, vérification de propriétés, démonstration automatique ou assistée par ordinateur.

Les thèmes abordés dans Langages applicatifs portent aussi bien sur la sémantique et la compilation des langages fonctionnels ou la combinaison avec d'autres paradigmes de programmation, que sur la spécification et la validation formelles du logiciel.

On s'intéresse à la théorie ainsi qu'aux applications pratiques, allant de l'implémentation à l'utilisation à l'échelle industrielle, en passant par l'enseignement de ces thématiques et les développements à forte composante méthodologique.

• Interopérabilité avec Objective Caml
• Typage des collections topologiques hétérogènes et des transformations
• Formalisation en Coq et visualisation d'un cours de géométrie pour le lycée
• Coq, un outil pour l'enseignement. Une expérience avec les étudiants du DESS Développement de logiciels sûrs
• Vérification formelle d'extractions de racines entières
• Typage, sûreté et sécurité