Thematic team Pole Proofs, programs and systems Programs and Languages (PL) Head Jean Krivine Research themes The thematic team “Programs and Languages” (PL) covers the activities of the PPS pole, primarily focusing on the design of programs, protocols, or programming languages that are based on or modeled by theoretical tools, most of which are studied within the pole. The team's objective is to bridge the gap between engineering practice and fundamental computer science. A non-exhaustive list of our areas of interest and contributions includes: The design of general-purpose or domain-specific programming languages: Functional programming (Ocaml), Concurrent programming (Elixir), Synchronous programming (Heptagon), and Probabilistic programming (ProbZelus) Coq (proof assistant) and its applications to software verification or mathematics education, Cduce (XML-oriented functional language), Kappa (DSL for molecular biology, based on graph rewriting) The study and design of distributed systems and the protocols that implement them: Babel (routing protocol), smart contracts for Blockchain (modeling and verification of distributed systems) Seminar and working groups Proofs, programs and systems Programming Type theory and realisability Permanent members Name@PhoneOfficePositionPoleTeam Baudart Guillaume @ 4026 Research Scientist - INRIA ISFP PPS picube , preuves , programmes Bernardi Giovanni @ 01 57 27 93 38 4021 Associate Professor PPS , ASV preuves , verif , programmes Castagna Giuseppe @ 01 57 27 93 40 3039 Senior Research Scientist - CNRS PPS preuves , programmes Dagand Pierre-Evariste @ 01 57 27 94 29 3012 Research Scientist - CNRS PPS programmes Di Cosmo Roberto @ Professor - (en détachement à l'INRIA) PPS programmes Ehrhard Thomas @ 01 57 27 92 17 4014a Senior Research Scientist - CNRS PPS algebre , programmes , preuves , picube Férée Hugo @ 01 57 27 94 05 4011 Associate Professor PPS programmes , preuves Guatto Adrien @ 01 57 27 94 15 3019 Associate Professor PPS algebre , programmes , preuves Herbelin Hugo @ 01 57 27 90 87 3029 Senior Research Scientist - INRIA PPS algebre , picube , preuves , programmes Krivine Jean @ 4027 Research Scientist - CNRS PPS algebre , programmes Letouzey Pierre @ 01 57 27 93 37 3040 Associate Professor PPS picube , programmes , preuves Lévy Jean-Jacques @ 01 57 27 92 68 4032 Senior Research Scientist Emeritus - INRIA PPS preuves , picube , programmes Narboux Julien @ 01 57 27 92 58 3022 Associate Professor PPS programmes , preuves Ruet Paul @ 01 57 27 92 48 3023 Research Scientist - CNRS PPS algebre , programmes Saurin Alexis @ 01 57 27 93 37 3040 Research Scientist - CNRS PPS algebre , programmes , preuves , picube Scherer Gabriel @ 4032 Research Scientist - INRIA PPS algebre , programmes , preuves , picube Treinen Ralf @ 01 57 27 92 44 3021 Professor PPS , ASV programmes , verif Non-permanent members Name@PhoneOfficePositionPoleTeam Duboc Guillaume @ 3010 PhD Student PPS programmes Gallego Emilio @ 01 57 27 92 24 4030 Starting research position - INRIA PPS picube , algebre , preuves , programmes Gonzalez Colin @ 3044 PhD Student PPS programmes Huang Xuejing @ 3018 Post-Doc PPS programmes , preuves Jafar-Rhamani Farzad @ 01 57 27 92 92 3026 Post-Doc PPS algebre , programmes , preuves , picube Kirst Dominik @ Post-Doc PPS preuves , picube , programmes Laurent Mickael @ 3033 PhD Student PPS programmes , preuves Ndiaye Yves @ PhD Student PPS programmes Nourel Astyax @ 3044 PhD Student PPS programmes Vienot Ada @ 3044 PhD Student PPS algebre , programmes , preuves