Speaker: Jean-Pierre Talpin
Abstract: An era of ubiquitous computing arises under the novel paradigm of mobile cyber-physical networks, where continuous dynamics in physical spaces become deeply coupled to intermittent discrete computations and communications in digital and social spaces. Its “lingua franca” must denote physical and digital mobility, physical and digital distribution and communication, intermittence and openness, creation and deletion, physics and disturbances, time, real and logical. The semantics of hybrid pi-calculus features all these aspects packed in a lean proof system of five discrete and continuous rules. Here be dragons, as the adage says: this simplicity comes at the cost of extraordinary challenges to formal verification.
The aim of this talk is to share the key process algebraic concepts that put the HPC into motion, and to hint the steep path ahead to analyse, verify, and implement it.
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.