~~NOCACHE~~ ---- datatemplateentry ---- template : en:templates:pole type : Pole nom : Proofs, programs and systems nomcourt : pps responsable : gmanzone ---- \\
[[poles:pps:intranet:]]
\\ === Research themes === The pole Proofs, programs and systems (PPS) aims at advancing the state of the art in the fields of theoretical foundations of programming languages, of interactive proof assistants, and more generally of computational formalisms. We investigate these subjects by combining three different approaches: * {{icon>circle?lg&color=#c77fff}} a //syntactic// approach, developing theoretical languages based on logical formalisms, * {{icon>circle?lg&color=#ffbf7f}} an //algebraic// approach, studying the mathematical structures underlying computation, * {{icon>circle?lg&color=#ade09a}} a //practical// approach, modeling and analyzing actual computational systems. The pole is structured into three thematic teams, according to the three different approaches. These teams use their specific methods to contribute to the common scientific goals: {{page>patates}} /* {{ potatoes.svg?750 |Research activities}} */ The PPS pole hosts the project-team $\pi r^2$ which is joined between INRIA, CNRS and Université Paris-Diderot — Paris 7. We also host several members of IRILL, the Center for Research and Innovation on Free Software which is a joined structure of INRIA, Université Paris-Diderot — Paris 7 and Université Pierre-et-Marie-Curie — Paris 6. /* 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. */ \\ === Events === * Seminar [[::en:seminaires:pps:]] * Online seminar [[::en:seminaires:greta:]] * Working groups * [[::en:seminaires:acs:]] * [[::en:seminaires:cat:]] * [[::en:seminaires:semantique:]] * [[::en:seminaires:programmation:]]\\ * [[::en:seminaires:types:]] * Meetings [[::en:rencontres:pps:]] /* \\ === Members === {{page>.:db:annuaire_en}} */ \\ === Permanent members === {{page>.:db:annuaire_perm_en}} \\ === Non-permanent members === {{page>.:db:annuaire_noperm_en}}