Find Academic Supervisors

• Category Theory
• Programming Semantics
• Theoretical Computer Science
• +3 more

James Robin Bernard Cockett is a Professor in the Department of Computer Science at the University of Calgary, Faculty of Science. His research focuses on foundational topics in category theory and its applications, including distributive categories, restriction categories, differential categories, and semantics of computation. He teaches advanced courses such as Category Theory for Computer Science and Foundations of Functional Programming. Education: B.A. Mathematics, University of Warwick, 1974 Doctor of Philosophy (Mathematics), University of Leeds, 1979 Research Interests: Dr. Cockett explores categorical proof theory, semantics of concurrency, and quantum programming. His work bridges abstract mathematics with computational models, emphasizing structured programming paradigms and logical frameworks. Awards & Recognition: 2019: Visiting Professor, Macquarie University 2018: Distinguished Visiting Researcher, SICSA 2013: Chercheur Invite, CNRS (France) 2011: Volunteer Family Award (Calgary) Teaching & Service: In addition to academic roles, he has contributed to community service, including volunteer work recognized by the 2011 Volunteer Family Award. His courses emphasize foundational concepts in computer science and category theory.

Mateus De Oliveira OliveiraView profile

Associate Professor

• Theoretical Computer Science
• Automated Theorem Proving
• Parameterized Complexity
• +3 more

Mateus De Oliveira Oliveira is an Associate Professor in the Department of Informatics at the University of Bergen. His research focuses on theoretical computer science, automated theorem proving, parameterized complexity, formal verification, graph theory, and computational logic. His work spans algorithm design for constraint satisfaction problems, automated reasoning systems, and formal verification techniques. Notable contributions include advancements in width-based automated theorem proving, Petri net synthesis, and parameterized complexity analysis for graph algorithms. He leads the Autoproving project funded by the Research Council of Norway, exploring automated theorem proving through parameterized complexity theory. Recent publications highlight developments in symbolic functional decomposition, state canonization for theorem proving, and optimal dynamic programming algorithms. His research bridges foundational theory with practical applications in automated systems and formal methods.

Roberta GoriView profile

Associate Professor

• Modelling and Simulation of Biological Systems
• Formal Verification
• Floating-Point Arithmetic Analysis
• +4 more

Roberta Gori is an Associate Professor at the Dipartimento di Informatica of the University of Pisa. Her research focuses on formal verification techniques for biological systems and floating-point intensive programs, leveraging abstract interpretation and coinductive methods. She collaborates with BUGSENG Srl on safety-critical systems verification and has led multiple projects including 'Metodi Informatici Integrati per la Biomedica' (UniPi 2020-2021) and PRIN initiatives since 2000. Her work bridges theoretical computer science with practical biomedical applications, addressing challenges in program obfuscation, numerical analysis, and systems biology. Education: Background in Computer Science with focus on formal methods Key research interests include: Verification of floating-point computations Modeling biological systems using reaction networks Formal program analysis and abstract interpretation Development of verification tools like FPSE and ECLAIR Notable collaborations include work with Simula Research Laboratory (Norway) and the University of Parma. Her contributions span over 60 publications, emphasizing both foundational theory and industrial applications in safety-critical domains.

• Theoretical Computer Science
• Formal Methods
• Coalgebra
• +3 more

Clemens Kupke is a Senior Lecturer in the Department of Computer and Information Sciences at the University of Strathclyde, part of the Faculty of Science. His research focuses on theoretical computer science, formal methods, and coalgebraic systems. He leads projects such as Cover: Coalgebraic Foundations for Quantitative Verification and contributed to the Maths DTP 2021/22 grant. Kupke has organized events like the Scottish Programming Languages and Verification Summer School (2024, 2019) and presented at conferences including TYPES 2024. His work emphasizes coalgebraic logic, automata theory, and database foundations, with notable contributions to semi-structured data models and query languages. Research Interests: His core areas include coalgebraic modal logic, automata theory, and formal verification. He explores how coalgebra can unify diverse data models and query languages, particularly in semi-structured data contexts. Recent projects address quantitative verification techniques and categorical approaches to fixpoint logics. Awards: He received the APLAS 2023 Best Paper Award for collaborative work. His publications span theoretical aspects of computing, with a focus on foundational methods in programming languages and verification. Grants & Supervision: Principal Investigator on the £1.5M EPSRC-funded Cover project (2020–2025) and co-investigator on KTP projects. He mentors researchers in formal methods and has supervised work on type theory and algebraic structures. Current grants include collaboration with Nordvall Forsberg and Watters on foundational programming languages research.

• Type Theory
• Category Theory
• Programming Languages
• +4 more

Dr. Fredrik Nordvall Forsberg is a Senior Lecturer in the Department of Computer & Information Sciences at the University of Strathclyde and a member of the Mathematically Structured Programming group. His work focuses on the foundations of programming languages, using tools from mathematical logic, type theory, and category theory. He explores semantics of data types, correct-by-construction programming, constructive mathematics, and applications of category theory to systems modeling. Education: While specific academic qualifications are not listed, his research and publications indicate advanced expertise in theoretical computer science and mathematics. Research Interests: His work spans type theory (especially inductive-inductive definitions and quotient inductive types), constructive mathematics (including ordinal theory), categorical models for programming languages, and applications of category theory to economic game theory and business processes. He designs type systems for correct-by-construction software, addressing challenges in decidable type checking and program correctness. Publications & Impact: His recent work includes foundational contributions to homotopy type theory, categorical game semantics, and formal methods for scientific computing. His publications appear in top venues like LICS, POPL, and ACM SIGPLAN conferences, reflecting interdisciplinary impact spanning computer science and mathematics. Awards: APLAS 2023 Best Paper Award ETAPS 2016 EATCS Best Paper Award Distinguished Presentation Award (2021) Grants & Projects: Leads/co-investigator on projects like the £1M 'Correct-by-Construction Approach to Approximate Computation' (2023–2027) and collaborations with Cambridge Quantum Computing (KTP projects 2020–2022). Professional Activities: Organizes conferences (e.g., Types 2025) and serves on program committees for PLDI, ICFP, and FoSSaCS. Recent speaking engagements include the Academia Sinica IIT Seminar (2024). Labs & Collaborations: Active in the Mathematically Structured Programming group, focusing on foundational programming language theory. Collaborates with industry partners like Cambridge Quantum Computing to apply theoretical insights to real-world software systems.

Pablo NogueiraView profile

Lecturer

• Programming Language Theory
• Programming Language Design
• Programming Language Implementation
• +9 more

Pablo Nogueira is a Permanent Lecturer and Researcher at the Technical University of Madrid, Spain. He is affiliated with the School of Computer Engineering (E.T.S.I. Informáticos) and the Department of Computer Languages and Systems and Software Engineering. His research focuses on foundational aspects of computer science, with extensive teaching experience across diverse programming paradigms and technical domains. Research Interests: His work spans programming language theory, design, and implementation, with specialized expertise in logic-based computer science, lambda calculi, operational semantics, and program transformation techniques. Key innovations include full-reducing abstract machines, proof-directed debugging methodologies, variable-free unification using relational algebra, datatype-generic functional programming, and advanced parsing techniques. Technology Transfer: He has led projects developing virtual-reality simulators for education and public safety, with a patent pending for delta-wing hang glider flight simulation technology (WO/2025/032276). Additional contributions include synthetic content generation for neural network training and applications in educational neuroscience.

Delphine DemangeView profile

Associate Professor

• Programming Languages Implementation
• Compiler Verification
• Formal Semantics
• +7 more

Delphine Demange is an Associate Professor in Computer Science at the University of Rennes, affiliated with Inria, CNRS, and IRISA, where she conducts research in the Epicure group. Her work focuses on programming languages, formal semantics, compiler verification, and program verification using interactive theorem provers. Research Interests: Programming Languages Implementation Compiler Verification Formal Semantics Program Verification with Interactive Theorem Provers Static Analysis and Language-Based Security Her recent publications demonstrate a strong trend in mechanized semantics, verified compilation, and correctness of intermediate representations such as SSA forms and dataflow circuits. She frequently employs Coq for formal verification and contributes to foundational aspects of compiler correctness. Scientific Awards: EAPLS Best PhD Dissertation Award 2012 Gilles Kahn PhD Thesis Award 2013 Delphine Demange has held significant service roles, including Program Co-Chair for CC 2021 and General Co-Chair for JFLA 2023 and 2024. She has served on numerous program committees for top conferences such as POPL, PLDI, CPP, ESOP, and OOPSLA, reflecting her active engagement in the programming languages community. She teaches courses in programming, algorithmics, compilation, semantics, and software security at both undergraduate and master's levels. She is part of the Epicure research team at IRISA, focusing on verified systems and programming language foundations.

Philipp G. HaselwarterView profile

Researcher

• Programming Languages
• Logic
• Security
• +7 more

Philipp G. Haselwarter is a researcher at the Department of Computer Science, School of Science and Technology, Aarhus University, Denmark. His work centers on programming languages, logic, and security, with significant contributions to formal verification and probabilistic programming. His research interests include: Programming Languages Logic Security Cryptography Formal Verification Probabilistic Programming His recent publications focus on higher-order separation logic, error bounds in probabilistic programs, and foundational verification of cryptographic systems. The work shows a strong trend toward rigorous, logic-based methods for ensuring correctness and security in complex software systems, particularly in concurrent and probabilistic settings. He has no listed scientific awards in the provided data. There is no information available about student advising or research grants. He is not noted as leading any specific lab or research team, though his publications suggest active collaboration within the formal methods community.

• Theoretical Computer Science
• Formal Methods
• Rewriting Systems
• +4 more

Kiraku Shintani is affiliated with the Japan Advanced Institute of Science and Technology (JAIST), a leading research institution in Japan focused on science and technology. He actively contributes to the field of theoretical computer science, particularly in formal methods and programming language theory, as evidenced by his participation in the POPL 2024 conference and contribution to the CPP workshop. His research centers on foundational aspects of computation, with a focus on confluence and commutation properties in rewriting systems. These are essential for ensuring the correctness and determinism of computational systems, especially in functional programming and proof assistants. His work applies logical frameworks to certify proofs mechanically, enhancing trust in automated reasoning tools. The recent publication demonstrates a method for certifying confluence and commutation using parallel critical pairs, indicating deep engagement with advanced topics in proof theory and automated verification. This reflects a strong trend in formal verification, aiming to increase the reliability of software and logical systems through machine-checked proofs. Certification of Confluence- and Commutation-Proofs via Parallel Critical Pairs (2024) Kiraku Shintani advises no publicly listed students and there is no mention of grants or funding sources in the available material. However, his research likely involves collaboration within formal methods groups at JAIST or through international academic networks associated with conferences like POPL and CPP. He is likely involved in research teams or labs focused on programming languages, formal verification, or logical frameworks at JAIST, though specific lab names or team structures are not mentioned in the provided texts.

Robbert KrebbersView profile

Associate Professor

• Semantics
• Separation logic
• Theorem proving
• +13 more

Robbert Krebbers is an Associate Professor in the Department of Software Science at Radboud University Nijmegen, Netherlands. His research focuses on advancing program verification techniques for complex programming paradigms such as concurrency, higher-order functions, and modular code, with applications to systems languages like C, Rust, and Scala. He develops rigorous mathematical foundations and practical verification tools, primarily using the Coq proof assistant. His most significant research contribution is as co-designer and co-leader of Iris , a highly influential framework for concurrent separation logic in Coq. Iris has been widely adopted in verification projects worldwide. Before returning to Radboud, he served as an Assistant Professor at Delft University of Technology and completed a postdoctoral fellowship at Aarhus University. He earned his PhD cum laude from Radboud University between 2011 and 2015. His research interests include: Semantics Separation logic Theorem proving Coq Program verification Concurrent and higher-order programming His recent publications (2020–2025) show a consistent focus on mechanized verification, linearizability, session types, deadlock freedom, and foundational enhancements to Iris and separation logic. These works appear in top-tier venues like POPL, PLDI, ICFP, and OOPSLA, with several receiving distinguished paper or artifact awards. Notable scientific awards include: POPL 2023 Distinguished Paper Award (DimSum) POPL 2022 Distinguished Paper Award (Simuliris) PLDI 2021 Distinguished Paper and Artifact Awards (RefinedC) CPP 2021 Distinguished Paper Award (Machine-Checked Semantic Session Typing) ECOOP 2017 Distinguished Paper Award 2023 Alonzo Church Award (as part of Iris team) He has advised PhD students such as Ike Mulder and Jules Jacobs. He actively contributes to the academic community as a program committee member, steering committee member, and organizer for major conferences including POPL, PLDI, ICFP, and CPP. His work is supported by major grants such as ERC Consolidator Grant (RustBelt) and Villum Investigator Grant (CPV). He is a core member of the Logic and Semantics Group and the Iris research project, which involves collaborations across institutions globally. His personal website is https://robbertkrebbers.nl .

David MonniauxView profile

Researcher

• programming languages
• static analysis
• model checking
• +2 more

David Monniaux is a senior researcher (directeur de recherche) at CNRS, the largest French national scientific research agency. He works at VERIMAG, a computer science laboratory jointly operated by CNRS and the University of Grenoble. His research focuses on proving software correct, connecting to computability theory, complexity theory, and mathematical logic. Dr. Monniaux holds a PhD in Computer Science (2001, Université Paris Dauphine) and a habilitation in Computer Science (2009, Université Joseph Fourier, Grenoble), as well as an agrégation in mathematics. His research interests span programming languages, static analysis, model checking, compilers, and assisted proof. He has particular expertise in proving strong properties of critical software used in civil aviation, especially regarding numerical overflows and floating-point computations. He has also worked on cryptographic protocols and probabilistic systems. His approach combines abstract interpretation, formal verification, and mathematical logic to address software correctness problems. Dr. Monniaux's recent work shows a strong focus on static analysis techniques, program verification, and formal methods. His publications demonstrate expertise in polyhedral analysis, strategy iteration, and the application of SMT solving to program analysis problems. His research bridges theoretical computer science with practical applications in safety-critical systems. Among his notable scientific contributions are projects like VERASCO (integrating static analysis into the CompCert certified compiler), STATOR (exploring advanced techniques for automatic inference of program invariants), and ASOPT (developing new algorithms for static program analysis). Dr. Monniaux has advised several students who have gone on to successful careers, including Julien Henry (now at Grammatech), Alexis Fouilhé (now in industry), George (Egor) Karpenkov (now at Apple Inc.), and Alexandre Maréchal (post-doctoral researcher at LIP6). He currently advises Hang Yu and Valentin Touzeau. He is actively involved in the programming languages and formal methods research community, serving on program committees for major conferences including POPL, PLDI, and VMCAI.

• Sustainability
• Sustainable Innovation
• Sustainable Entrepreneurship
• +9 more

Dr. Rosina Watson is an Associate Professor of Sustainability and Head of the Sustainable Business Group at Cranfield School of Management, Cranfield University. She is also Co-Course Director of both the MSc in Sustainability and the Sustainability Business Specialist Apprenticeship. Her academic and professional work integrates sustainability, innovation, and strategic management. University: Cranfield University School: Cranfield School of Management Role: Associate Professor of Sustainability, Head of Sustainable Business Group, Co-Course Director Dr. Watson holds a PhD from Cranfield School of Management and a first-class degree in Politics, Philosophy, and Economics (PPE) from Oxford University. Prior to her academic career, she gained extensive industry experience as Head of Corporate Sustainability at Home Retail Group (Argos and Homebase), with earlier roles in finance, M&A, strategy, and commercial functions at Shell, ITV, and Carphone Warehouse. Her research focuses on sustainable innovation , particularly how large corporations and entrepreneurs can drive sustainability through partnerships and collaboration. She investigates how differences between organizational logics can be harnessed to enhance innovation outcomes. Her work spans stakeholder engagement, dynamic capabilities, and policy frameworks for sustainable entrepreneurship. The recent publications of Dr. Watson reveal a strong and consistent trajectory in sustainability research. Her work emphasizes collaborative models for sustainability innovation, including cross-sector partnerships, stakeholder engagement frameworks, and capability-based approaches. She has made significant contributions to understanding how policy can support sustainable entrepreneurship through meso-level ecosystem interventions and crowdsourced co-creation. Her scholarship also extends to sustainability education, particularly in professional and higher education contexts. Dr. Watson has received no explicitly mentioned scientific awards in the provided text. She actively contributes to teaching across executive and general management programs, including the MBA and Executive MBA, and leads specialized sustainability programs. While no PhD or master’s students are listed as advisees, her leadership in academic programs suggests a strong mentoring role. She is involved in initiatives that foster learning communities and inclusive education in sustainability. Dr. Watson is affiliated with the Sustainable Business Group at Cranfield, a research and teaching hub focused on sustainability-driven innovation and strategy. Her collaborative research involves partnerships with academics and practitioners, reflecting her emphasis on co-creation and stakeholder engagement. Her future work likely continues to explore systemic approaches to sustainability transitions, policy innovation, and the educational foundations of sustainable business leadership.

• Type Theory
• Formal Methods
• Functional Programming
• +3 more

Ana Bove is an Associate Professor (Docent) at Chalmers University of Technology and University of Gothenburg, affiliated with the Department of Computer Science and Engineering. She leads the Logic and Types unit in the Computing Science division since 2021. Her research focuses on type theory, formal methods, and programming languages, with contributions to dependent types, interactive theorem provers, and functional programming. Affiliations: Chalmers University, University of Gothenburg Roles: Head of Logic and Types unit, former Director of Studies (CSE), Project Manager (ForMath EU project) Her work emphasizes foundational aspects of programming languages and verified software. Notable projects include the ForMath EU initiative under Prof. Thierry Coquand. She has contributed to Agda and type systems, with over 28 publications in formal methods and theoretical computer science. Research interests include recursion models in type theory, partial functions, and alpha-structural induction. Her lab, the Logic and Types unit, explores advanced type systems and formal verification techniques.

• Concurrent Software
• Memory Consistency Models
• Parallel Processing
• +7 more

Prof Susmit Sarkar is a Professor and Director of Research in the School of Computer Science at the University of St Andrews. He has been at St Andrews since 2013, following postdoctoral work at the University of Cambridge and a PhD from Carnegie Mellon University. He holds honorary fellowships at the University of Edinburgh and is a Fellow of the BCS and Senior Member of the ACM. His research focuses on concurrency, low-level software, and hardware-software interfaces, with contributions to memory consistency models (ARM, IBM POWER, RISC-V), parallel programming languages (C/C++/Java), and formal verification. He has served as an invited expert for RISC-V architecture and reviewed for top conferences/journals like PLDI and POPL. Teaching responsibilities in 2023-24 include CS3050 (Logic), CS4204 (Concurrency), and CS5031 (Software Engineering). Past teaching includes database systems and advanced programming projects. He supervises student research projects at all levels. Key awards include BCS Fellowship (201X), ACM Senior Membership (201X), and Honorary Fellowship at Edinburgh (20XX). Research has been funded by EPSRC/ERC/ANR grants, with projects on cache coherence verification, scalable shared memory, and parallel algorithm patterns. Publications span over 39 peer-reviewed works, including seminal papers on ARMv8 operational models, POWER memory synchronisation, and RISC-V architecture validation. Active in open-source projects like ModRef2018-MCM and community engagement through programming workshops.

Christian UrbanView profile

Lecturer

• Theorem provers
• Programming languages
• Compilers
• +4 more

Dr. Christian Urban is a Lecturer in Computer Science at King's College London's Department of Informatics, part of the Faculty of Natural, Mathematical & Engineering Sciences. He is actively involved in the Security Hub and King's Cybersecurity Centre, an EPSRC-NCSC Academic Centre of Excellence in Cyber Security Research. His research focuses on theorem provers, programming languages, compilers, type systems, and functional programming. He has led and contributed to multiple research projects, including Formal Verification of Practical Nominal Unification Algorithms (Royal Society-funded) and Nominal Techniques for Verification Environments . Research Interests: Formal methods for program correctness Automated reasoning and theorem proving Programming language semantics and compilation Nominal logic and its applications His work bridges theoretical foundations with practical tools, emphasizing verified software systems and formal verification techniques. Recent Projects: Formal Verification of Practical Nominal Unification Algorithms (2025-2027) Nominal Techniques for Verification Environments (2021-2024) Efficient and provably correct schedulers for many-core CPUs (2013-2015) Awards: Skolem Award from CADE (2015) Grants & Collaborations: Dr. Urban has secured funding from the Royal Society, DFG, and other bodies. His collaborations include projects on XML query optimization, schedulers for parallel architectures, and verified parser implementations. Labs/Teams: As part of the Informatics Department and Security Hub, he contributes to interdisciplinary research on software systems security, formal methods, and verified programming tools.