Département 2 : Méthodes formelles

Responsable de l’équipe : Didier Galmiche
Tél. : +33 3 83 59 20 15
Mail : didier.galmiche@loria.fr

Site de l’équipe

Présentation

Le projet scientifique de TYPES s’inscrit dans le cadre général de la conception de systèmes informatiques sûrs en considérant les liens entre logique et programmation sûre. On considérera comme fondamentale la relation entre calcul, programmation et logique telle qu’elle apparaît au travers de paradigmes comme proofs-as-programs (isomorphisme de Curry-Howard, programmation fonctionnelle), proofs-as-computations (programmation logique) et proofs-as-processes (programmation concurrente). Ainsi la modélisation de concepts, de mécanismes et les calculs sont abordés au travers de la logique (théorie de la démonstration, sémantique) avec des méthodes qui reposent sur la construction (ou recherche) automatisée de preuves et l’analyse structurelle des preuves dans des logiques sous-structurelles et constructives.

Axes thématiques

• modèles, sémantique et expressivité
• structures de preuves, réfutations et décidabilité

Logiciels

• LC
• Bi-instutionistic

Collaborations

• Stéphane Demri (ENS Cachan)
• équipe LILAC de l’IRIT de Toulouse
• Université de Bath
• Roy Dyckhoff de l’Université de St Andrew (Écosse)

Mots-clés

Logique, sémantiques, modèles, preuves, réfutations, programmes, ressources