Speaker: Jean-Pierre Talpin
Abstract: An era of ubiquitous computing arises under the novel paradigm of mobile cyber-physical networks which intertwines continuous dynamics in physical spaces to intermittent discrete computations and communications in digital and social spaces.
The semantics hybrid pi-calculus packs capacities to express the complexity of such networks using a lean and simple proof system. Here be dragons! however, as this simplicity comes at the cost of uncharted challenges to formal verification.
This talk will share key process algebraic concepts to put the HPC in motion, and hint the steep and arduous path ahead to type, analyse, verify, and implement it with the help of vast literatures on bisimulation, session type and contract theory.
Bio: Jean-Pierre Talpin is a senior scientist with INRIA. He received a Master degree in Theoretical Computer Science from University Paris VI and was awarded a Ph.D. Thesis by Ecole des Mines de Paris under the supervision of Pierre Jouvelot. He then joined the European Computer-Industry Research Centre in Munich for three years before being hired by INRIA in 1995, where he led Inria project-teams ESPRESSO and TEA from 2000 to 2023.
His early career works on effect inference and on region-based memory management were awarded the 2004 ACM Award for the most influential POPL paper (for 1994) with Mads Tofte and the 2012 ACM/IEEE LICS Test of Time Award (for 1992) with Pierre Jouvelot.
After joining Inria, he consecutively served and lead two project-teams: ESPRESSO, on synchronous programming, and TEA, on architecture ad scheduling analysis.
Since these career-long studies frol logic, type, concurrency theory and experiences in program analysis and verification, and cybernetic system design, his late research interests focus on novel and challenging topics such as end-to-end mechanized program verification, the design of advanced process calculi to model the logic of mobile, dynamic cyber-physical system networks and compositional contract-algebraic methodologies to verify them.