π-calculus, Session Types research at the University of Oxford
Nobuko Yoshida is Christopher Strachey Chair of Computer Science in University of Oxford. She is an EPSRC Established Career Fellow and an Honorary Fellow at Glasgow University. Last 15 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 received the third Suffrage Science Awards for Mathematics and Computing from MRC for her STEM activity. Her current grants include: EPSRC Morella-HAT, AppControl, Border Control (Hardware), POST (Fellowship), Stardust (Distributed systems) and Turtles (Multi agent systems). She is an editor of ACM Transactions on Programming Languages and Systems, ACM Formal Aspects of Computing, 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: Actyx, Barclays, Cognizant, Google, Red Hat, Weaveworks and EDF Energy.
I am an RA at the University of Oxford. I earned my PhD from Queen Mary, University of London, in mathematical physics. Before joining the University of Oxford, I worked in various industry roles, including at Secondmind and Honu AI, with an emphasis on in AI. Right now, my focus is on realising multiparty session types with dependent types.
I am an RA at the University of Oxford. I earned my PhD from Université Grenoble Alpes in France. Previously, I worked as a postdoc at the University of Iowa, USA and at the University of Innsbruck, Austria. Right now, my focus is on formalizing various aspects of asynchronous multiparty session types in the Coq proof assistant.
I am an RA at the University of Oxford. My research interests are formal analysis and verification of programming languages and complex systems. Previously, I was a research fellow at the University of Innsbruck. I did my PhD at Katholieke Universiteit Leuven. Currently, I am focusing on the specification and verification of multiparty session type systems.
I am Atalay Mert Ileri, a Senior Research Associate (Postdoctoral Fellow in US terms) on Concurrent, Distributed and Quantum Programming at University of Oxford. My work focuses on formal verification of software systems’ security properties using interactive proof assistants. I am currently working with Prof. Nobuko Yoshida on adapting session types to quantum processes as a part of Mobility Reading Group. Before joining University of Oxford, I worked at Kansas State University as a Postdoctoral Fellow with Prof. Hande McGinty as a member of Koncordant Lab. My work in Kansas State University investigated applications of formal verification on deductive reasoning using knowledge graphs. Prior to that, I obtained my Ph.D. from MIT under the supervision of Prof. Nickolai Zeldovich and Prof. M. Frans Kaashoek in PDOS group. My PhD work involved formal verification of crash-safe storage systems with nondeterministic behaviors’ confidentiality properties.
I am a Research Assistant at the University of Oxford. I have an MMathCompSci degree from Oxford. I am working on multiparty sessions types.
I am currently a Senior Research Associate at the University of Oxford. Previously, I was a postdoc at Reykjavik University, and before that, I earned my PhD from the University of Cambridge. I work primarily on denotational semantics for graded computational effects, including multiparty session types from the computational effects perspective. I am also interested in notions of algebraic theory, especially from the perspective of formal category theory.
I am a Research Associate in Theoretical Computer Science at the University of Oxford. I obtained my PhD from the University of Groningen. My research focuses on probabilistic multi-party session type systems and the model checking of probabilistic multi-party systems. I adopt a bottom-up approach, ensuring correct interactions between sessions through safety properties and exploring probabilistic behavioural equivalences.
I am an RA at the University of Oxford. I earned my PhD from University of Milano-Bicocca, Italy. Previously, I worked as a postdoc at Inria-Rennes (France), as a research engineer at the telecom firm Orange (France) and then again as a postdoc at the Bernoulli Institute, Uni. of Groningen (Netherlands). My expertise involves different models of concurrency such as Petri nets, their formal verification and applications to choregraphic programming languages. I am currently working on the relations between Markov processes, probabilistic temporal logics and distributed systems.
Ari Hernawan is a PhD student under supervision of Professor Nobuko Yoshida. He has a master’s degree (M.Sc) from the Department Computer Science and Information Engineering at National Central University, Taiwan. He studied Bayesian inference in Hidden Markov Model for 3D depth video. Current research interests are focused on distributed machine.
I am a DPhil Student at the University of Oxford. I graduated in Computing from Imperial College London. Previously I worked as a Research Student at Imperial College London, and a Software Engineering Intern at Ghyston.
Kai Pischke is 1st year PhD student under the supervision of Nobuko Yoshida. His interests are in lightweight verification using type systems. He is currently working on a processes calculus integrating refinement types and session types. Before his PhD, he obtained a MCompSci at Oxford and his dissertation with Sam Staton was on categorical semantics for hardware description languages, and he previously worked on probabilistic programming.
I am a PhD student at the University of Oxford. Previously I completed an MMathCompSci at Oxford, with a master’s dissertation on denotational semantics of lambda calculi. Currently I am working on security of cryptographic protocols and denotational semantics for concurrency.
I am a DPhil student at the University of Oxford. I previously completed a MSc in Advanced Computer Science at Oxford, with a dissertation on probabilistic session types with expected cost analysis. Currently I am working on the theory and application of probabilistic session types in concurrent systems.