MobilityReadingGroup

π-calculus, Session Types research at Imperial College

People

Prof Nobuko Yoshida
Professor of Computing
Publications

Nobuko Yoshida is Professor of Computing at Imperial College London. Last 10 years, her main research interests are theories and applications of protocols specifications and verifications. She introduced multiparty session types [ POPL’08, JACM ] which received Most Influential POPL Paper Award in 2018 (judged by its influence over the last decade). This work enlarged the community and widened the scope of applications of session types, e.g. runtime monitoring based on Scribble (co-developed with Red Hat) has been deployed to other projects such as cyberinfrastructure in the US Ocean Observatories Initiative (OOI); and widened the scope of her research areas. She was awarded CNRS and JSSP visiting fellowships and visiting professorships at Paris VI and Paris VII. She is an editor of ACM Transactions on Programming Languages and Systems, Mathematical Structures in Computer Science, Journal of Logical Algebraic Methods in Programming, and the chief editor of The Computer-aided Verification and Concurrency Column for EATCS Bulletin. Her current industry partners include: Cognizant, Estafet, J.P. Morgan, Red Hat, Weaveworks, November Group, ABB, EDF Energy, Xilinx, EPCC Ltd, Codeplay Software Ltd and Mexeler.

Dr Simon Castellan
Research Associate
Publications

I am a RA in the Department of Computing at Imperial College London. Previously, I was a PhD Student at ENS Lyon under the supervision of Pierre Clairambault and Olivier Laurent, working on true concurrent approaches to concurrent games semantics of programming languages. I am interested in semantics of concurrent programming languages, causal models, game semantics, type theory and their applications to static analysis of concurrent programs.

Dr David Castro
Research Associate
Publications

I am an RA in the Department of Computing at the Imperial College London. I did my PhD at the University of St Andrews, under the supervision of Kevin Hammond. My research interests are focused on high-level models of parallel computing (algorithmic skeletons), functional programming and typing systems. Specifically, I am interested in using the behavioural types approach for mapping high-level specifications programs to efficient low-level parallel programs.

Dr Francisco Ferreira
Research Associate
Publications

I am an RA at Imperial College. My research interests are proof assistants, programming language theory and design, and reactive systems. Previously, I did a PhD at McGill University under the supervision of Brigitte Pientka. My PhD thesis is about using contextual types to simplify writing programs and proofs with potentially open terms. Currently, I am working on simplifying the mechanization of session based type systems.

Dr Raymond Hu
Research Associate
Publications

I am an RA at Imperial College London working primarily on the design and application of session types to practice. My recent and current work includes a graphical integration of multiparty session types and Petri nets, and the Scribble framework for multiparty session types verification in existing mainstream languages such as Java and Python. I have also recently worked on deadlock verification for advanced barrier-based concurrent programs. I completed my PhD at Imperial College London in 2011.

Dr Nicholas Ng
Research Associate
Publications

I am an RA in the Department of Computing at Imperial College London, previously completed a PhD degree under the supervision of Nobuko Yoshida and Wayne Luk. My research centres around a typing system for the Pi-calculus (session types) and its applications on high performance parallel computing systems. My recent research focuses on verification of concurrency in the Go programming language using using process calculi/behavioural types approach.

Dr Domenico Ruoppolo
Research Associate
Publications

I am an RA in the Department of Computing at Imperial College London. Previously I was an assistant professor (ATER) at the University Paris 13, where I also completed a PhD in 2016 under the supervision of Giulio Manzonetto and Stefano Guerrini. My research lies at the interface of logic, theoretical computer science and category theory provided by the Curry-Howard correspondence. Specifically, I am interested in the study of proofs and programs through the lens of denotational semantics. In this context, sometimes I explore abstract categorical axiomatizations, sometimes I study more concrete models of lambda-calculi, especially those related to linear logic and intersection type theory.

Dr Alceste Scalas
Research Associate
Publications
Assel Altayeva
PhD Student
Publications

Assel is a PhD student under the supervision of Professor Nobuko Yoshida. Her background is in Applied Logic and Constructive Type Theory. Assel holds a Master degree from Novosibirsk State University where she worked on computability of higher-order type functionals and precomplete arithmetical equivalences. Her current research concerns optimisation and data provenance problems arising in the architecture of complex distributed component based systems through application of session type theory.

Julien Gabet
PhD Student
Publications

Juju is a PhD student under supervision of Professor Nobuko Yoshida. They have a master’s degree from Université d’Aix-Marseille, where they worked primarily on linear type systems over π-calculus under supervision of Pr. Emmanuel Beffara. Current research interests are focused on shared memory races and session types.

Eva Graversen
PhD Student
Publications

Eva Graversen is a PhD student working under the supervision of Professor Nobuko Yoshida and Dr Iain Phillips. She has a masters degree from Aalborg University, where she worked primarily on type inference for session types and generic type systems for psi-calculi. Her current research focuses on reversibility, session types, and event structures.