---- datatemplateentry ----
template    : templates:equipe
type        : Équipe thématique
nom         : Preuves et programmes
nomcourt    : preuves
responsable : saurin
pole        : pps
---- 

\\ === Thèmes de recherche ===

Notre méthodologie repose principalement sur la correspondance de Curry-Howard entre preuves et programmes, dans laquelle la réécriture joue un rôle essentiel, représentant à la fois l'élimination des coupures des preuves et la sémantique opérationnelle des programmes. L'objet de base est le lambda-calcul, une théorie très pure de la programmation fonctionnelle, et ses extensions : par des systèmes de types, par des raffinements linéaires ou différentiels, par des mécanismes de pattern-matching et par différentes sortes d'effets non purement fonctionnels (choix non déterministe ou probabiliste, continuations, états internes, locaux ou non, etc.). On obtient alors des formalismes intéressants pour leurs propriétés logiques, donnant par exemple un sens calculatoire à des concepts standard de la logique (tels que le choix ou le raisonnement par l'absurde). On obtient aussi des représentations abstraites des langages de programmation réels, dans un cadre rendu aussi indépendant que possible des implémentations, et permettant d’en analyser la sémantique. Parmi ces extensions, le calcul des constructions inductives est à la fois une logique et un langage de programmation, sur laquelle est fondé l’assistant de preuve Coq.

/*
{{ patates.svg?500 |Activités de recherche }}
*/

\\ === Séminaire et groupes de travail ===

[[::seminaires:pps:]] \\
[[::seminaires:semantique:]] \\
[[::seminaires:types:]]

\\ === Permanents  ===

{{page>.:db:annuaire_perm}}

\\ === Non-permanents ===

{{page>.:db:annuaire_noperm}}