---- datatemplateentry ---- template : templates:pole type : Pôle nom : Preuves, programmes et systèmes nomcourt : pps responsable : gmanzone ---- \\
[[.:intranet:]]
\\ === Thèmes de recherche === Le programme scientifique du pôle Preuves, programmes et systèmes (PPS) de l'IRIF vise à renforcer les fondements théoriques des langages de programmation, des assistants de preuves et, plus généralement, des formalismes de calcul. Ces problématiques sont abordées en croisant trois points de vue complémentaires : * {{icon>circle?lg&color=#c77fff}} une approche //syntaxique//, qui développe des langages théoriques issus de formalismes logiques, * {{icon>circle?lg&color=#ffbf7f}} une approche //algébrique//, qui étudie les structures mathématiques liées au calcul, * {{icon>circle?lg&color=#ade09a}} une approche //pratique//, qui modélise et analyse des systèmes de calcul réels. Le pôle est constitué de trois équipes thématiques, correspondant à chacun de ces trois points de vue. Elles développent leurs outils propres, et les mettent ensuite au service d'objectifs scientifiques communs : {{page>patates}} /*{{ patates.svg?750 |Activités de recherche}}*/ Le pôle PPS héberge l'équipe-projet $\pi r^2$ commune à l'INRIA, au CNRS et à l'Université Paris-Diderot — Paris 7, ainsi qu'une partie des membres de l'IRILL (Initiative de Recherche et d'Innovation sur le Logiciel Libre), une structure commune à l'INRIA, à l'Université Paris-Diderot — Paris 7 et à l'Université Pierre-et-Marie-Curie — Paris 6. \\ === Evènements === * Séminaire [[::seminaires:pps:]] * Séminaire en ligne [[::seminaires:greta:]] * Groupes de travail * [[::seminaires:acs:]] * [[::seminaires:cat:]] * [[::seminaires:semantique:]] * [[::seminaires:programmation:]]\\ * [[::seminaires:types:]] * Rencontres [[..:..:rencontres:pps:]] /* Le pôle Preuves, Programmes et Systèmes (PPS) de l'IRIF fédère les énergies de chercheurs, enseignants-chercheurs et doctorants issus de cultures différentes (informatique et mathématiques) pour travailler sur les thématiques des langages de programmation et des systèmes distribués, et de leurs fondements logiques et mathématiques. Dans cette perspective, PPS développe la théorie des systèmes de typage, des machines abstraites et des programmes concurrents et s'intéresse à la logique des programmes, à la sémantique des effets et des ressources dans les langages de programmation, etc. Le pôle élabore aussi des méthodes et des outils de modélisation des systèmes biologiques et de nouvelles méthodes de développement et de maintenance des systèmes dans le domaine du logiciel libre. Enfin, PPS est un acteur essentiel dans le domaine du développement des assistants à la preuve. Notre projet de recherche est fondé sur la conviction que la logique (et plus particulièrement la théorie de la démonstration), mais aussi la théorie des catégories, et d'autres théories mathématiques comme l'homologie ou l'homotopie, ou les probabilités, ont un rôle essentiel à jouer pour élucider le sens des programmes, afin de les rendre plus sûrs, et qu'inversement l'informatique, comme la physique a pu l'être et continue de l'être, peut être une source dans laquelle la logique et d'autres domaines des mathématiques peuvent puiser pour se renouveler. Le pôle PPS comporte une équipe-projet de l'INRIA, πr², et a un rôle moteur dans l'Initiative de Recherche sur l'Informatique du Logiciel Libre, structure d'accueil commune à l'INRIA, et aux Universités Paris 6 et 7. */ /* \\ === Annuaire === {{page>.:db:annuaire}} */ \\ === Permanents === {{page>.:db:annuaire_perm}} \\ === Non-permanents === {{page>.:db:annuaire_noperm}}